From 8db1af5afcb414b502a58a87f6bdcc1c08cbe3d2 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 27 Jun 2023 18:22:22 +0200
Subject: Finish some proofs in Diverge

---
 backends/lean/Base/Diverge.lean | 119 ++++++++++++++++++++++++++++++++++------
 1 file changed, 102 insertions(+), 17 deletions(-)

diff --git a/backends/lean/Base/Diverge.lean b/backends/lean/Base/Diverge.lean
index 76f0543a..c97674dd 100644
--- a/backends/lean/Base/Diverge.lean
+++ b/backends/lean/Base/Diverge.lean
@@ -544,28 +544,40 @@ namespace FixI
 
   /- Some utilities to define the mutually recursive functions -/
 
-  inductive Funs : List (Type u) → List (Type u) → Type (u + 1) :=
-    | Nil : Funs [] []
+  -- TODO: use more
+  @[simp] def kk_ty (id : Type) (a b : id → Type) := (i:id) → a i → Result (b i)
+  @[simp] def k_ty (id : Type) (a b : id → Type) := kk_ty id a b → kk_ty id a b
+
+  -- Initially, we had left out the parameters id, a and b.
+  -- However, by parameterizing Funs with those parameters, we can state
+  -- and prove lemmas like Funs.is_valid_p_is_valid_p
+  inductive Funs (id : Type) (a b : id → Type) :
+    List (Type u) → List (Type u) → Type (u + 1) :=
+    | Nil : Funs id a b [] []
     | Cons {ity oty : Type u} {itys otys : List (Type u)}
-           (f : ity → Result oty) (tl : Funs itys otys) : Funs (ity :: itys) (oty :: otys)
+           (f : kk_ty id a b → ity → Result oty) (tl : Funs id a b itys otys) :
+           Funs id a b (ity :: itys) (oty :: otys)
 
-  theorem Funs.length_eq {itys otys : List (Type)} (fl : Funs itys otys) :
-    itys.length = otys.length :=
+  theorem Funs.length_eq {itys otys : List (Type)} (fl : Funs id a b itys otys) :
+    otys.length = itys.length :=
     match fl with
     | .Nil => by simp
     | .Cons f tl =>
       have h:= Funs.length_eq tl
       by simp [h]
 
+  def fin_cast {n m : Nat} (h : m = n) (i : Fin n) : Fin m :=
+    ⟨ i.val, by have h1:= i.isLt; simp_all ⟩
+
   @[simp] def Funs.cast_fin {itys otys : List (Type)}
-    (fl : Funs itys otys) (i : Fin itys.length) : Fin otys.length :=
-    ⟨ i.val, by have h:= fl.length_eq; have h1:= i.isLt; simp_all ⟩
+    (fl : Funs id a b itys otys) (i : Fin itys.length) : Fin otys.length :=
+    fin_cast (fl.length_eq) i
 
-  def get_fun {itys otys : List (Type)} (fl : Funs itys otys) :
-    (i : Fin itys.length) → itys.get i → Result (otys.get (fl.cast_fin i)) :=
+  def get_fun {itys otys : List (Type)} (fl : Funs id a b itys otys) :
+    (i : Fin itys.length) → kk_ty id a b → itys.get i → Result (otys.get (fl.cast_fin i)) :=
     match fl with
     | .Nil => λ i => by have h:= i.isLt; simp at h
-    | @Funs.Cons ity oty itys1 otys1 f tl =>
+    | @Funs.Cons id a b ity oty itys1 otys1 f tl =>
       λ i =>
       if h: i.val = 0 then
         Eq.mp (by cases i; simp_all [List.get]) f
@@ -582,10 +594,9 @@ namespace FixI
           (by
             cases Heq: i; rename_i val isLt;
             cases Heq': j; rename_i val' isLt;
-            cases val <;> simp_all [List.get])
+            cases val <;> simp_all [List.get, fin_cast])
           (get_fun tl j)
 
-
   -- TODO: move
   theorem add_one_le_iff_le_ne (n m : Nat) (h1 : m ≤ n) (h2 : m ≠ n) : m + 1 ≤ n := by
     -- Damn, those proofs on natural numbers are hard - I wish Omega was in mathlib4...
@@ -612,7 +623,7 @@ namespace FixI
     := by
     generalize h: (n - m) = k
     revert m
-    induction k
+    induction k -- TODO: induction h rather?
     case zero =>
       simp_all
       intro m h1 h2
@@ -683,6 +694,65 @@ namespace FixI
     . apply Hgvalid
     . apply Hhvalid
 
+  def Funs.is_valid_p
+    (k : k_ty id a b)
+    (fl : Funs id a b itys otys) :
+    Prop :=
+    match fl with
+    | .Nil => True
+    | .Cons f fl => (∀ x, FixI.is_valid_p k (λ k => f k x)) ∧ fl.is_valid_p k
+
+  #check Subtype
+  def Funs.is_valid_p_is_valid_p_aux
+    {k : k_ty id a b}
+    {itys otys : List Type}
+    (Heq : List.length otys = List.length itys)
+    (fl : Funs id a b itys otys) (Hvalid : is_valid_p k fl) :
+    ∀ (i : Fin itys.length) (x : itys.get i), FixI.is_valid_p k (fun k => get_fun fl i k x) := by
+    -- Prepare the induction
+    have ⟨ n, Hn ⟩ : { n : Nat // itys.length = n } := ⟨ itys.length, by rfl ⟩
+    revert itys otys Heq fl Hvalid
+    induction n
+    --
+    case zero =>
+      intro itys otys Heq fl Hvalid Hlen;
+      have Heq: itys = [] := by cases itys <;> simp_all
+      have Heq: otys = [] := by cases otys <;> simp_all
+      intro i x
+      simp_all
+      have Hi := i.isLt
+      simp_all
+    case succ n Hn =>
+      intro itys otys Heq fl Hvalid Hlen i x;
+      cases fl <;> simp at *
+      rename_i ity oty itys otys f fl
+      have ⟨ Hvf, Hvalid ⟩ := Hvalid
+      have Hvf1: is_valid_p k fl := by
+        simp_all [Funs.is_valid_p]
+      have Hn := @Hn itys otys (by simp[*]) fl Hvf1 (by simp [*])
+      -- Case disjunction on i
+      match i with
+      | ⟨ 0, _ ⟩ =>
+        simp at x
+        simp [get_fun]
+        apply (Hvf x)
+      | ⟨ .succ j, HiLt ⟩ =>
+        simp_arith at HiLt
+        simp at x
+        let j : Fin (List.length itys) := ⟨ j, by simp_arith [HiLt] ⟩
+        have Hn := Hn j x
+        apply Hn
+
+  def Funs.is_valid_p_is_valid_p
+    (itys otys : List (Type)) (Heq: otys.length = itys.length := by decide)
+    (k : k_ty (Fin (List.length itys)) (List.get itys) fun i => List.get otys (fin_cast Heq i))
+    (fl : Funs (Fin itys.length) itys.get (λ i => otys.get (fin_cast Heq i)) itys otys) :
+    fl.is_valid_p k  →
+    ∀ (i : Fin itys.length) (x : itys.get i), FixI.is_valid_p k (fun k => get_fun fl i k x)
+    := by
+    intro Hvalid
+    apply is_valid_p_is_valid_p_aux <;> simp [*]
+
 end FixI
 
 namespace Ex1
@@ -909,12 +979,12 @@ namespace Ex4
       let b ← k 0 (i - 1)
       .ret b
 
-  @[simp] def bodies (k : (i : Fin 2) → input_ty i → Result (output_ty i)) :
-    Funs [Int, Int] [Bool, Bool] :=
-    Funs.Cons (is_even_body k) (Funs.Cons (is_odd_body k) Funs.Nil)
+  @[simp] def bodies :
+    Funs (Fin 2) input_ty output_ty [Int, Int] [Bool, Bool] :=
+    Funs.Cons (is_even_body) (Funs.Cons (is_odd_body) Funs.Nil)
 
   def body (k : (i : Fin 2) → input_ty i → Result (output_ty i)) (i: Fin 2) :
-    input_ty i → Result (output_ty i) := get_fun (bodies k) i
+    input_ty i → Result (output_ty i) := get_fun bodies i k
 
   theorem body_is_valid : is_valid body := by
     -- Split the proof into proofs of validity of the individual bodies
@@ -933,6 +1003,21 @@ namespace Ex4
     . split <;> simp
       apply is_valid_p_bind <;> simp
 
+  theorem body_is_valid' : is_valid body := by
+    -- Split the proof into proofs of validity of the individual bodies
+    rw [is_valid]
+    simp [body]
+    intro k
+    apply (Funs.is_valid_p_is_valid_p [Int, Int] [Bool, Bool])
+    simp [Funs.is_valid_p]
+    (repeat (apply And.intro)) <;> intro x <;> simp at x <;>
+    simp [is_even_body, is_odd_body]
+    -- Prove the validity of the individual bodies
+    . split <;> simp
+      apply is_valid_p_bind <;> simp
+    . split <;> simp
+      apply is_valid_p_bind <;> simp
+
   theorem body_fix_eq : fix body = body (fix body) :=
     is_valid_fix_fixed_eq body_is_valid
 
-- 
cgit v1.2.3