diff options
| -rw-r--r-- | backends/lean/Base/Diverge.lean | 31 | ||||
| -rw-r--r-- | backends/lean/Base/Primitives.lean | 1 |
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 |