From 7206b48a73d6204baea99f4f4675be2518a8f8c2 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 10 Jul 2023 15:06:12 +0200
Subject: Start working on the progress tactic

---
 backends/lean/Base/Arith/Base.lean | 10 ++++++++++
 1 file changed, 10 insertions(+)
 create mode 100644 backends/lean/Base/Arith/Base.lean

(limited to 'backends/lean/Base/Arith/Base.lean')

diff --git a/backends/lean/Base/Arith/Base.lean b/backends/lean/Base/Arith/Base.lean
new file mode 100644
index 00000000..ddd2dc24
--- /dev/null
+++ b/backends/lean/Base/Arith/Base.lean
@@ -0,0 +1,10 @@
+import Lean
+
+namespace Arith
+
+open Lean Elab Term Meta
+
+-- We can't define and use trace classes in the same file
+initialize registerTraceClass `Arith
+
+end Arith
-- 
cgit v1.2.3


From 2dbd529b499c2bb9dae754df0e449cad577ac7a0 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 13 Jul 2023 14:00:11 +0200
Subject: Add IList.lean

---
 backends/lean/Base/Arith/Base.lean | 40 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)

(limited to 'backends/lean/Base/Arith/Base.lean')

diff --git a/backends/lean/Base/Arith/Base.lean b/backends/lean/Base/Arith/Base.lean
index ddd2dc24..a6e59b74 100644
--- a/backends/lean/Base/Arith/Base.lean
+++ b/backends/lean/Base/Arith/Base.lean
@@ -1,4 +1,6 @@
 import Lean
+import Std.Data.Int.Lemmas
+import Mathlib.Tactic.Linarith
 
 namespace Arith
 
@@ -7,4 +9,42 @@ 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
+
+
+/- 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
+
 end Arith
-- 
cgit v1.2.3


From 0a8211041814b5eafac0b9e2dbcd956957a322b5 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 18 Jul 2023 18:02:03 +0200
Subject: Move an arithmetic lemma

---
 backends/lean/Base/Arith/Base.lean | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'backends/lean/Base/Arith/Base.lean')

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
-- 
cgit v1.2.3


From 1854c631a6a7a3f8d45ad18e05547f9d3782c3ee Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 25 Jul 2023 16:26:08 +0200
Subject: Make progress on the hashmap properties

---
 backends/lean/Base/Arith/Base.lean | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'backends/lean/Base/Arith/Base.lean')

diff --git a/backends/lean/Base/Arith/Base.lean b/backends/lean/Base/Arith/Base.lean
index e008f7b9..9c11ed45 100644
--- a/backends/lean/Base/Arith/Base.lean
+++ b/backends/lean/Base/Arith/Base.lean
@@ -53,4 +53,8 @@ theorem int_pos_ind (p : Int → Prop) :
     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
-- 
cgit v1.2.3