diff options
| author | Son Ho | 2023-07-18 18:02:03 +0200 |
|---|---|---|
| committer | Son Ho | 2023-07-18 18:02:03 +0200 |
| commit | 0a8211041814b5eafac0b9e2dbcd956957a322b5 (patch) | |
| tree | c823a5a3668201ddcc0caded7933dea0061a059a | |
| parent | 0f430c055c3a531ceab83635adc5df92f0015c6e (diff) | |
Move an arithmetic lemma
| -rw-r--r-- | backends/lean/Base/Arith/Base.lean | 6 | ||||
| -rw-r--r-- | backends/lean/Base/Diverge/Base.lean | 14 |
2 files changed, 10 insertions, 10 deletions
diff --git a/backends/lean/Base/Arith/Base.lean b/backends/lean/Base/Arith/Base.lean index a6e59b74..e008f7b9 100644 --- a/backends/lean/Base/Arith/Base.lean +++ b/backends/lean/Base/Arith/Base.lean @@ -28,6 +28,12 @@ theorem ne_is_lt_or_gt {x y : Int} (hne : x ≠ y) : x < y ∨ x > y := by | .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 diff --git a/backends/lean/Base/Diverge/Base.lean b/backends/lean/Base/Diverge/Base.lean index 4ff1d923..1d548389 100644 --- a/backends/lean/Base/Diverge/Base.lean +++ b/backends/lean/Base/Diverge/Base.lean @@ -4,6 +4,7 @@ import Init.Data.List.Basic import Mathlib.Tactic.RunCmd import Mathlib.Tactic.Linarith import Base.Primitives.Base +import Base.Arith.Base /- TODO: this is very useful, but is there more? -/ set_option profiler true @@ -537,23 +538,16 @@ namespace FixI let j: Fin tys1.length := ⟨ j, jLt ⟩ Eq.mp (by simp) (get_fun tl j) - -- 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 - def for_all_fin_aux {n : Nat} (f : Fin n → Prop) (m : Nat) (h : m ≤ n) : Prop := if heq: m = n then True else f ⟨ m, by simp_all [Nat.lt_iff_le_and_ne] ⟩ ∧ - for_all_fin_aux f (m + 1) (by simp_all [add_one_le_iff_le_ne]) + for_all_fin_aux f (m + 1) (by simp_all [Arith.add_one_le_iff_le_ne]) termination_by for_all_fin_aux n _ m h => n - m decreasing_by simp_wf apply Nat.sub_add_lt_sub <;> simp - simp_all [add_one_le_iff_le_ne] + simp_all [Arith.add_one_le_iff_le_ne] def for_all_fin {n : Nat} (f : Fin n → Prop) := for_all_fin_aux f 0 (by simp) @@ -603,7 +597,7 @@ namespace FixI apply hi <;> simp_all . unfold for_all_fin_aux at hf simp_all - . simp_all [add_one_le_iff_le_ne] + . simp_all [Arith.add_one_le_iff_le_ne] -- TODO: this is not necessary anymore theorem for_all_fin_imp_forall (n : Nat) (f : Fin n → Prop) : |