diff options
author | Son HO | 2023-07-31 16:15:58 +0200 |
---|---|---|
committer | GitHub | 2023-07-31 16:15:58 +0200 |
commit | 887d0ef1efc8912c6273b5ebcf979384e9d7fa97 (patch) | |
tree | 92d6021eb549f7cc25501856edd58859786b7e90 /backends/lean/Base/Arith/Base.lean | |
parent | 53adf30fe440eb8b6f58ba89f4a4c0acc7877498 (diff) | |
parent | 9b3a58e423333fc9a4a5a264c3beb0a3d951e86b (diff) |
Merge pull request #31 from AeneasVerif/son_lean_backend
Improve the Lean backend
Diffstat (limited to '')
-rw-r--r-- | backends/lean/Base/Arith/Base.lean | 60 |
1 files changed, 60 insertions, 0 deletions
diff --git a/backends/lean/Base/Arith/Base.lean b/backends/lean/Base/Arith/Base.lean new file mode 100644 index 00000000..9c11ed45 --- /dev/null +++ b/backends/lean/Base/Arith/Base.lean @@ -0,0 +1,60 @@ +import Lean +import Std.Data.Int.Lemmas +import Mathlib.Tactic.Linarith + +namespace Arith + +open Lean Elab Term Meta + +-- We can't define and use trace classes in the same file +initialize registerTraceClass `Arith + +-- TODO: move? +theorem ne_zero_is_lt_or_gt {x : Int} (hne : x ≠ 0) : x < 0 ∨ x > 0 := by + cases h: x <;> simp_all + . rename_i n; + cases n <;> simp_all + . apply Int.negSucc_lt_zero + +-- TODO: move? +theorem ne_is_lt_or_gt {x y : Int} (hne : x ≠ y) : x < y ∨ x > y := by + have hne : x - y ≠ 0 := by + simp + intro h + have: x = y := by linarith + simp_all + have h := ne_zero_is_lt_or_gt hne + match h with + | .inl _ => left; linarith + | .inr _ => right; linarith + +-- 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 + +/- Induction over positive integers -/ +-- TODO: move +theorem int_pos_ind (p : Int → Prop) : + (zero:p 0) → (pos:∀ i, 0 ≤ i → p i → p (i + 1)) → ∀ i, 0 ≤ i → p i := by + intro h0 hr i hpos +-- have heq : Int.toNat i = i := by +-- cases i <;> simp_all + have ⟨ n, heq ⟩ : {n:Nat // n = i } := ⟨ Int.toNat i, by cases i <;> simp_all ⟩ + revert i + induction n + . intro i hpos heq + cases i <;> simp_all + . rename_i n hi + intro i hpos heq + cases i <;> simp_all + rename_i m + cases m <;> simp_all + +-- We sometimes need this to make sure no natural numbers appear in the goals +-- TODO: there is probably something more general to do +theorem nat_zero_eq_int_zero : (0 : Nat) = (0 : Int) := by simp + +end Arith |