summaryrefslogtreecommitdiff
path: root/backends/lean/Base
diff options
context:
space:
mode:
authorSon Ho2023-06-26 18:40:47 +0200
committerSon Ho2023-06-26 18:40:47 +0200
commit4cc411a30b19f5c5eea67b2e4da232337af8f12b (patch)
tree4a9ada0f798c01eeac5431e8da5daefa74469110 /backends/lean/Base
parent87fd14e74fe00752df7759372093543ae77a51ae (diff)
Generalize some definitions
Diffstat (limited to '')
-rw-r--r--backends/lean/Base/Diverge.lean34
1 files changed, 22 insertions, 12 deletions
diff --git a/backends/lean/Base/Diverge.lean b/backends/lean/Base/Diverge.lean
index d65e77a1..0c1028bd 100644
--- a/backends/lean/Base/Diverge.lean
+++ b/backends/lean/Base/Diverge.lean
@@ -321,7 +321,6 @@ namespace Fix
simp_all [is_mono_p, karrow_rel, result_rel]
-- The important lemma about `is_mono_p`
- -- TODO: generalize d?
theorem is_mono_p_bind
(g : ((x:a) → Result (b x)) → Result c)
(h : c → ((x:a) → Result (b x)) → Result d) :
@@ -700,24 +699,28 @@ namespace Ex4
let b ← k 0 (i - 1)
.ret b
- inductive Funs : List (Type 0) → List (Type 0) → Type 1 :=
+ inductive Funs : List (Type u) → List (Type u) → Type (u + 1) :=
| Nil : Funs [] []
- | Cons {ity oty : Type 0} {itys otys : List (Type 0)} (f : ity → Result oty) (tl : Funs itys otys) : Funs (ity :: itys) (oty :: otys)
+ | 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 0)} (fl : Funs itys otys) : itys.length = otys.length :=
+ 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 0)} (fl : Funs itys otys) (i : Fin itys.length) : Fin otys.length :=
+ @[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] :=
+ @[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 0)} (fl : Funs itys otys) :
+ @[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
@@ -734,11 +737,18 @@ namespace Ex4
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
-
- def fix_ {n : Nat} {ity oty : Fin n → Type 0} (f : ((i:Fin n) → ity i → Result (oty i)) → (i:Fin n) → ity i → Result (oty i)) :
+ 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
+
+ def fix_ {n : Nat} {ity oty : Fin n → Type}
+ (f : ((i:Fin n) → ity i → Result (oty i)) → (i:Fin n) → ity i → Result (oty i)) :
(i:Fin n) → ity i → Result (oty i) :=
sorry