summaryrefslogtreecommitdiff
path: root/backends
diff options
context:
space:
mode:
Diffstat (limited to 'backends')
-rw-r--r--backends/lean/Base/Diverge.lean48
1 files changed, 20 insertions, 28 deletions
diff --git a/backends/lean/Base/Diverge.lean b/backends/lean/Base/Diverge.lean
index c97674dd..c62e6dd5 100644
--- a/backends/lean/Base/Diverge.lean
+++ b/backends/lean/Base/Diverge.lean
@@ -25,6 +25,11 @@ TODO:
- simplifier/rewriter have a strange behavior sometimes
-/
+
+/- TODO: this is very useful, but is there more? -/
+set_option profiler true
+set_option profiler.threshold 100
+
namespace Diverge
namespace Primitives
@@ -533,10 +538,10 @@ namespace FixI
fix f = f (fix f) := by
have Hvalid' : Fix.is_valid (k_to_gen f) := by
intro k x
- simp [is_valid, is_valid_p] at Hvalid
+ simp only [is_valid, is_valid_p] at Hvalid
let ⟨ i, x ⟩ := x
have Hvalid := Hvalid (k_of_gen k) i x
- simp [k_to_gen, k_of_gen, kk_to_gen, kk_of_gen] at Hvalid
+ simp only [k_to_gen, k_of_gen, kk_to_gen, kk_of_gen] at Hvalid
refine Hvalid
have Heq := Fix.is_valid_fix_fixed_eq Hvalid'
simp [fix]
@@ -612,7 +617,7 @@ namespace FixI
termination_by for_all_fin_aux n _ m h => n - m
decreasing_by
simp_wf
- apply Nat.sub_add_lt_sub <;> simp_all
+ apply Nat.sub_add_lt_sub <;> simp
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)
@@ -665,6 +670,7 @@ namespace FixI
simp_all
. simp_all [add_one_le_iff_le_ne]
+ -- TODO: this is not necessary anymore
theorem for_all_fin_imp_forall (n : Nat) (f : Fin n → Prop) :
for_all_fin f → ∀ i, f i
:= by
@@ -702,7 +708,6 @@ namespace FixI
| .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}
@@ -724,11 +729,11 @@ namespace FixI
simp_all
case succ n Hn =>
intro itys otys Heq fl Hvalid Hlen i x;
- cases fl <;> simp at *
+ cases fl <;> simp at Hlen i x Heq Hvalid
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]
+ simp [Hvalid, Funs.is_valid_p]
have Hn := @Hn itys otys (by simp[*]) fl Hvf1 (by simp [*])
-- Case disjunction on i
match i with
@@ -989,29 +994,12 @@ namespace Ex4
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_is_valid' : is_valid body := by
- -- Split the proof into proofs of validity of the individual bodies
- rw [is_valid]
- simp [body]
+ simp only [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]
+ simp only [is_even_body, is_odd_body]
-- Prove the validity of the individual bodies
. split <;> simp
apply is_valid_p_bind <;> simp
@@ -1088,11 +1076,15 @@ namespace Ex5
theorem id_body_is_valid :
∀ k x, is_valid_p k (λ k => @id_body a k x) := by
intro k x
- simp [id_body]
+ simp only [id_body]
split <;> simp
- apply is_valid_p_bind <;> simp_all
+ apply is_valid_p_bind <;> simp [*]
-- We have to show that `map k tl` is valid
- apply map_is_valid; simp
+ apply map_is_valid;
+ -- Remark: if we don't do the intro, then the last step is expensive:
+ -- "typeclass inference of Nonempty took 119ms"
+ intro k x
+ simp only [is_valid_p_same, is_valid_p_rec]
noncomputable def id (t : Tree a) := fix id_body t