summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--backends/lean/Base/Diverge.lean31
-rw-r--r--backends/lean/Base/Primitives.lean1
2 files changed, 26 insertions, 6 deletions
diff --git a/backends/lean/Base/Diverge.lean b/backends/lean/Base/Diverge.lean
index b5264d0d..37d8eb27 100644
--- a/backends/lean/Base/Diverge.lean
+++ b/backends/lean/Base/Diverge.lean
@@ -11,6 +11,27 @@ open Result
variable {a b : Type}
+/-
+TODO:
+- we want an easier to use cases:
+ - keeps in the goal an equation of the shape: `t = case`
+ - if called on Prop terms, uses Classical.em
+ Actually, the cases from mathlib seems already quite powerful
+ (https://leanprover-community.github.io/mathlib_docs/tactics.html#cases)
+ For instance: cases h : e
+ Also: cases_matching
+- better split tactic
+- we need conversions to operate on the head of applications.
+ Actually, something like this works:
+ ```
+ conv at Hl =>
+ apply congr_fun
+ simp [fix_fuel_P]
+ ```
+ Maybe we need a rpt ... ; focus?
+- simplifier/rewriter have a strange behavior sometimes
+-/
+
/-! # The least fixed point definition and its properties -/
def least_p (p : Nat → Prop) (n : Nat) : Prop := p n ∧ (∀ m, m < n → ¬ p m)
@@ -115,9 +136,7 @@ theorem fix_fuel_mono {f : (a → Result b) → a → Result b} (Hmono : is_mono
match m with
| 0 =>
exfalso
- -- TODO: annoying to do those conversions by hand - try zify?
- have : n1 + 1 ≤ (0 : Int) := by simp [*] at *
- have : 0 ≤ n1 := by simp [*] at *
+ zify at *
linarith
| Nat.succ m1 =>
simp_arith at Hle
@@ -188,9 +207,9 @@ theorem fix_fixed_eq_terminates (f : (a → Result b) → a → Result b) (Hmono
fix f x = f (fix f) x := by
have Hl := fix_fuel_P_least Hmono He
-- TODO: better control of simplification
- have Heq : fix_fuel_P f x (least (fix_fuel_P f x)) = fix_fuel_pred f x (least (fix_fuel_P f x)) :=
- by simp [fix_fuel_P]
- simp [Heq] at Hl; clear Heq
+ conv at Hl =>
+ apply congr_fun
+ simp [fix_fuel_P]
-- The least upper bound is > 0
have ⟨ n, Hsucc ⟩ : ∃ n, least (fix_fuel_P f x) = Nat.succ n := by
revert Hl
diff --git a/backends/lean/Base/Primitives.lean b/backends/lean/Base/Primitives.lean
index 85e088fc..6b922143 100644
--- a/backends/lean/Base/Primitives.lean
+++ b/backends/lean/Base/Primitives.lean
@@ -526,6 +526,7 @@ instance (ty : ScalarTy) : DecidableEq (Scalar ty) :=
def Scalar.toInt {ty} (n : Scalar ty) : Int := n.val
-- Tactic to prove that integers are in bounds
+-- TODO: use this: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/instance.20with.20tactic.20autoparam
syntax "intlit" : tactic
macro_rules