summaryrefslogtreecommitdiff
path: root/backends/lean
diff options
context:
space:
mode:
authorSon Ho2023-06-27 10:52:07 +0200
committerSon Ho2023-06-27 10:52:07 +0200
commit0a62cf3f7d58b31c75344172bad1032e14a4082f (patch)
treeb3ff578d80b86408d49478eb158353011ae76e87 /backends/lean
parent7f3604c21bb9f923aecb98917b5c7a33bafd1bcb (diff)
Finish the proofs which use FixI
Diffstat (limited to '')
-rw-r--r--backends/lean/Base/Diverge.lean199
1 files changed, 157 insertions, 42 deletions
diff --git a/backends/lean/Base/Diverge.lean b/backends/lean/Base/Diverge.lean
index f3fa4815..76f0543a 100644
--- a/backends/lean/Base/Diverge.lean
+++ b/backends/lean/Base/Diverge.lean
@@ -542,6 +542,147 @@ namespace FixI
simp [fix]
conv => lhs; rw [Heq]
+ /- Some utilities to define the mutually recursive functions -/
+
+ inductive Funs : List (Type u) → List (Type u) → Type (u + 1) :=
+ | Nil : Funs [] []
+ | Cons {ity oty : Type u} {itys otys : List (Type u)}
+ (f : ity → Result oty) (tl : Funs itys otys) : Funs (ity :: itys) (oty :: otys)
+
+ theorem Funs.length_eq {itys otys : List (Type)} (fl : Funs itys otys) :
+ itys.length = otys.length :=
+ match fl with
+ | .Nil => by simp
+ | .Cons f tl =>
+ have h:= Funs.length_eq tl
+ by simp [h]
+
+ @[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 ⟩
+
+ 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)) :=
+ match fl with
+ | .Nil => λ i => by have h:= i.isLt; simp at h
+ | @Funs.Cons ity oty itys1 otys1 f tl =>
+ λ i =>
+ if h: i.val = 0 then
+ Eq.mp (by cases i; simp_all [List.get]) f
+ else
+ let j := i.val - 1
+ have Hj: j < itys1.length := by
+ have Hi := i.isLt
+ simp at Hi
+ revert Hi
+ cases Heq: i.val <;> simp_all
+ simp_arith
+ let j: Fin itys1.length := ⟨ j, Hj ⟩
+ Eq.mp
+ (by
+ cases Heq: i; rename_i val isLt;
+ cases Heq': j; rename_i val' isLt;
+ cases val <;> simp_all [List.get])
+ (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...
+ simp [Nat.add_one_le_iff]
+ simp [Nat.lt_iff_le_and_ne]
+ simp_all
+
+ def for_all_fin_aux {n : Nat} (f : Fin n → Prop) (m : Nat) (h : m ≤ n) : Prop :=
+ if heq: m = n then True
+ else
+ f ⟨ m, by simp_all [Nat.lt_iff_le_and_ne] ⟩ ∧
+ for_all_fin_aux f (m + 1) (by simp_all [add_one_le_iff_le_ne])
+ termination_by for_all_fin_aux n _ m h => n - m
+ decreasing_by
+ simp_wf
+ apply Nat.sub_add_lt_sub <;> simp_all
+ simp_all [add_one_le_iff_le_ne]
+
+ def for_all_fin {n : Nat} (f : Fin n → Prop) := for_all_fin_aux f 0 (by simp)
+
+ theorem for_all_fin_aux_imp_forall {n : Nat} (f : Fin n → Prop) (m : Nat) :
+ (h : m ≤ n) →
+ for_all_fin_aux f m h → ∀ i, m ≤ i.val → f i
+ := by
+ generalize h: (n - m) = k
+ revert m
+ induction k
+ case zero =>
+ simp_all
+ intro m h1 h2
+ have h: n = m := by
+ linarith
+ unfold for_all_fin_aux; simp_all
+ simp_all
+ -- There is no i s.t. m ≤ i
+ intro i h3; cases i; simp_all
+ linarith
+ case succ k hi =>
+ simp_all
+ intro m hk hmn
+ intro hf i hmi
+ have hne: m ≠ n := by
+ have hineq := Nat.lt_of_sub_eq_succ hk
+ linarith
+ -- m = i?
+ if heq: m = i then
+ -- Yes: simply use the `for_all_fin_aux` hyp
+ unfold for_all_fin_aux at hf
+ simp_all
+ tauto
+ else
+ -- No: use the induction hypothesis
+ have hlt: m < i := by simp_all [Nat.lt_iff_le_and_ne]
+ have hineq: m + 1 ≤ n := by
+ have hineq := Nat.lt_of_sub_eq_succ hk
+ simp [*, Nat.add_one_le_iff]
+ have heq1: n - (m + 1) = k := by
+ -- TODO: very annoying arithmetic proof
+ simp [Nat.sub_eq_iff_eq_add hineq]
+ have hineq1: m ≤ n := by linarith
+ simp [Nat.sub_eq_iff_eq_add hineq1] at hk
+ simp_arith [hk]
+ have hi := hi (m + 1) heq1 hineq
+ apply hi <;> simp_all
+ . unfold for_all_fin_aux at hf
+ simp_all
+ . simp_all [add_one_le_iff_le_ne]
+
+ theorem for_all_fin_imp_forall (n : Nat) (f : Fin n → Prop) :
+ for_all_fin f → ∀ i, f i
+ := by
+ intro Hf i
+ apply for_all_fin_aux_imp_forall <;> try assumption
+ simp
+
+ /- Automating the proofs -/
+ @[simp] theorem is_valid_p_same
+ (k : ((i:id) → a i → Result (b i)) → (i:id) → a i → Result (b i)) (x : Result c) :
+ is_valid_p k (λ _ => x) := by
+ simp [is_valid_p, k_to_gen, e_to_gen]
+
+ @[simp] theorem is_valid_p_rec
+ (k : ((i:id) → a i → Result (b i)) → (i:id) → a i → Result (b i)) (i : id) (x : a i) :
+ is_valid_p k (λ k => k i x) := by
+ simp [is_valid_p, k_to_gen, e_to_gen, kk_to_gen, kk_of_gen]
+
+ theorem is_valid_p_bind
+ {{k : ((i:id) → a i → Result (b i)) → (i:id) → a i → Result (b i)}}
+ {{g : ((i:id) → a i → Result (b i)) → Result c}}
+ {{h : c → ((i:id) → a i → Result (b i)) → Result d}}
+ (Hgvalid : is_valid_p k g)
+ (Hhvalid : ∀ y, is_valid_p k (h y)) :
+ is_valid_p k (λ k => do let y ← g k; h y k) := by
+ apply Fix.is_valid_p_bind
+ . apply Hgvalid
+ . apply Hhvalid
+
end FixI
namespace Ex1
@@ -768,55 +909,29 @@ namespace Ex4
let b ← k 0 (i - 1)
.ret b
- inductive Funs : List (Type u) → List (Type u) → Type (u + 1) :=
- | Nil : Funs [] []
- | Cons {ity oty : Type u} {itys otys : List (Type u)}
- (f : ity → Result oty) (tl : Funs itys otys) : Funs (ity :: itys) (oty :: otys)
-
- theorem Funs.length_eq {itys otys : List (Type)} (fl : Funs itys otys) :
- itys.length = otys.length :=
- match fl with
- | .Nil => by simp
- | .Cons f tl =>
- have h:= Funs.length_eq tl
- by simp [h]
-
- @[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 ⟩
-
@[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 get_fun {itys otys : List (Type)} (fl : Funs itys otys) :
- (i : Fin itys.length) → 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 =>
- λ i =>
- if h: i.val = 0 then
- Eq.mp (by cases i; simp_all [List.get]) f
- else
- let j := i.val - 1
- have Hj: j < itys1.length := by
- have Hi := i.isLt
- simp at Hi
- revert Hi
- cases Heq: i.val <;> simp_all
- simp_arith
- let j: Fin itys1.length := ⟨ j, Hj ⟩
- Eq.mp
- (by
- cases Heq: i; rename_i val isLt;
- cases Heq': j; rename_i val' isLt;
- cases val <;> simp_all [List.get])
- (get_fun tl j)
-
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
- theorem body_is_valid : is_valid body := by sorry
+ 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 for_all_fin_imp_forall
+ simp [for_all_fin]
+ repeat (unfold for_all_fin_aux; simp)
+ simp [get_fun]
+ (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