fix: add missing lemmas about infinite sequences

LeroyCompilerVerificationCourse/Sequences.lean

@@ -14,7 +14,7 @@ def infseq_fixpoint {α} (R : α → α → Prop) (x : α) :
   rw [infseq]
 
 -- The associated coinduction principle
-theorem infseq.coind {α} (h : α → Prop) (R : α → α → Prop)
+theorem infseq_coinduction_principle {α} (h : α → Prop) (R : α → α → Prop)
     (prem : ∀ (x : α), h x → ∃ y, R x y ∧ h y) : ∀ x, h x → infseq R x := by
   apply infseq.coinduct
   grind
@@ -95,6 +95,9 @@ theorem plus_right :
 def all_seq_inf (R : α → α → Prop) (x : α) : Prop :=
   ∀ y : α, star R x y → ∃ z, R y z
 
+def infseq_with_function (R : α → α → Prop) (a: α) : Prop :=
+  ∃ f : Nat → α, f 0 = a ∧ ∀ i, R (f i) (f (1 + i))
+
 def infseq_if_all_seq_inf (R : α → α → Prop) : ∀ x, all_seq_inf R x → infseq R x := by
   apply infseq.coinduct
   intro x H
@@ -118,4 +121,49 @@ theorem infseq_coinduction_principle_2 :
     case x => grind
     case y => grind [cases plus]
 
+theorem infseq_from_function : ∀ a, infseq_with_function R a → infseq R a := by
+  apply infseq.coinduct
+  intro x hyp
+  unfold infseq_with_function at hyp
+  have ⟨f , ⟨h0, hsucc⟩⟩ := hyp
+  refine ⟨f 1, ?_⟩
+  refine ⟨by grind, ?_⟩
+  unfold infseq_with_function
+  refine ⟨fun n => f (n + 1), ?_⟩
+  refine ⟨by grind, ?_⟩
+  intro i
+  specialize hsucc (i + 1)
+  grind
+
 @[grind] def irred (R : α → α → Prop) (a : α) : Prop := ∀ b, ¬(R a b)
+
+theorem star_star_inv (R_functional : ∀ a b c, R a b -> R a c -> b = c) : ∀ a b, star R a b -> forall c, star R a c → star R b c ∨ star R c b := by
+  intro _ _ sab
+  induction sab <;> grind
+
+theorem finseq_unique (R_functional : ∀ a b c, R a b -> R a c -> b = c) :
+  ∀ a b b', star R a b → irred R b → star R a b' → irred R b' → b = b' := by
+    intro a b b' sab ib sab' ib'
+    apply Or.elim (star_star_inv R_functional a b sab b' sab') <;> grind
+
+@[grind ]theorem infseq_star_inv (R_functional : ∀ a b c, R a b -> R a c -> b = c) : ∀ a b, star R a b → infseq R a → infseq R b := by
+  intro a b sab ia
+  induction sab
+  case star_refl => grind
+  case star_step x y z rxy syz ih =>
+    unfold infseq at ia
+    grind
+
+theorem infseq_finseq_excl (R_functional : ∀ a b c, R a b -> R a c -> b = c): ∀ a b, star R a b → irred R b → infseq R a → False := by
+  intro a b sab irb ia
+  have h : infseq R b := by grind
+  unfold infseq at h
+  grind
+
+theorem infseq_all_seq_inf (R_functional : ∀ a b c, R a b -> R a c -> b = c): ∀ a, infseq R a → all_seq_inf R a := by
+  intro a ia
+  unfold all_seq_inf
+  intro b sab
+  have h : infseq R b := by grind
+  unfold infseq at h
+  grind