From 3e8060b5501ec83940a4309389a68898df26ebd0 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 17 Jul 2023 23:37:31 +0200
Subject: Reorganize the Lean backend

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

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

diff --git a/backends/lean/Base/Arith/Scalar.lean b/backends/lean/Base/Arith/Scalar.lean
new file mode 100644
index 00000000..f8903ecf
--- /dev/null
+++ b/backends/lean/Base/Arith/Scalar.lean
@@ -0,0 +1,48 @@
+import Base.Arith.Int
+import Base.Primitives.Scalar
+
+/- Automation for scalars - TODO: not sure it is worth having two files (Int.lean and Scalar.lean) -/
+namespace Arith
+
+open Lean Lean.Elab Lean.Meta
+open Primitives
+
+def scalarTacExtraPreprocess : Tactic.TacticM Unit := do
+   Tactic.withMainContext do
+   -- Inroduce the bounds for the isize/usize types
+   let add (e : Expr) : Tactic.TacticM Unit := do
+     let ty ← inferType e
+     let _ ← Utils.addDeclTac (← mkFreshUserName `h) e ty (asLet := false)
+   add (← mkAppM ``Scalar.cMin_bound #[.const ``ScalarTy.Isize []])
+   add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Usize []])
+   add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Isize []])
+   -- Reveal the concrete bounds
+   Utils.simpAt [``Scalar.min, ``Scalar.max, ``Scalar.cMin, ``Scalar.cMax,
+                 ``I8.min, ``I16.min, ``I32.min, ``I64.min, ``I128.min,
+                 ``I8.max, ``I16.max, ``I32.max, ``I64.max, ``I128.max,
+                 ``U8.min, ``U16.min, ``U32.min, ``U64.min, ``U128.min,
+                 ``U8.max, ``U16.max, ``U32.max, ``U64.max, ``U128.max
+                 ] [] [] .wildcard
+
+elab "scalar_tac_preprocess" : tactic =>
+  intTacPreprocess scalarTacExtraPreprocess
+
+-- A tactic to solve linear arithmetic goals in the presence of scalars
+def scalarTac : Tactic.TacticM Unit := do
+  intTac scalarTacExtraPreprocess
+
+elab "scalar_tac" : tactic =>
+  scalarTac
+
+instance (ty : ScalarTy) : HasIntProp (Scalar ty) where
+  -- prop_ty is inferred
+  prop := λ x => And.intro x.hmin x.hmax
+
+example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by
+  intro_has_int_prop_instances
+  simp [*]
+
+example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by
+  scalar_tac
+
+end Arith
-- 
cgit v1.2.3


From 876137dff361620d8ade1a4ee94fa9274df0bdc6 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 25 Jul 2023 14:08:44 +0200
Subject: Improve int_tac and scalar_tac

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

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

diff --git a/backends/lean/Base/Arith/Scalar.lean b/backends/lean/Base/Arith/Scalar.lean
index f8903ecf..a56ea08b 100644
--- a/backends/lean/Base/Arith/Scalar.lean
+++ b/backends/lean/Base/Arith/Scalar.lean
@@ -28,11 +28,11 @@ elab "scalar_tac_preprocess" : tactic =>
   intTacPreprocess scalarTacExtraPreprocess
 
 -- A tactic to solve linear arithmetic goals in the presence of scalars
-def scalarTac : Tactic.TacticM Unit := do
-  intTac scalarTacExtraPreprocess
+def scalarTac (splitGoalConjs : Bool) : Tactic.TacticM Unit := do
+  intTac splitGoalConjs scalarTacExtraPreprocess
 
 elab "scalar_tac" : tactic =>
-  scalarTac
+  scalarTac false
 
 instance (ty : ScalarTy) : HasIntProp (Scalar ty) where
   -- prop_ty is inferred
-- 
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/Scalar.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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

diff --git a/backends/lean/Base/Arith/Scalar.lean b/backends/lean/Base/Arith/Scalar.lean
index a56ea08b..6f4a8eba 100644
--- a/backends/lean/Base/Arith/Scalar.lean
+++ b/backends/lean/Base/Arith/Scalar.lean
@@ -21,7 +21,8 @@ def scalarTacExtraPreprocess : Tactic.TacticM Unit := do
                  ``I8.min, ``I16.min, ``I32.min, ``I64.min, ``I128.min,
                  ``I8.max, ``I16.max, ``I32.max, ``I64.max, ``I128.max,
                  ``U8.min, ``U16.min, ``U32.min, ``U64.min, ``U128.min,
-                 ``U8.max, ``U16.max, ``U32.max, ``U64.max, ``U128.max
+                 ``U8.max, ``U16.max, ``U32.max, ``U64.max, ``U128.max,
+                 ``Usize.min
                  ] [] [] .wildcard
 
 elab "scalar_tac_preprocess" : tactic =>
-- 
cgit v1.2.3


From 81e991822879a942af34489b7a072f31739f28f6 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 26 Jul 2023 12:37:17 +0200
Subject: Update the syntax of the progress tactic

---
 backends/lean/Base/Arith/Scalar.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

diff --git a/backends/lean/Base/Arith/Scalar.lean b/backends/lean/Base/Arith/Scalar.lean
index 6f4a8eba..b792ff21 100644
--- a/backends/lean/Base/Arith/Scalar.lean
+++ b/backends/lean/Base/Arith/Scalar.lean
@@ -12,7 +12,7 @@ def scalarTacExtraPreprocess : Tactic.TacticM Unit := do
    -- Inroduce the bounds for the isize/usize types
    let add (e : Expr) : Tactic.TacticM Unit := do
      let ty ← inferType e
-     let _ ← Utils.addDeclTac (← mkFreshUserName `h) e ty (asLet := false)
+     let _ ← Utils.addDeclTac (← Utils.mkFreshAnonPropUserName) e ty (asLet := false)
    add (← mkAppM ``Scalar.cMin_bound #[.const ``ScalarTy.Isize []])
    add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Usize []])
    add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Isize []])
-- 
cgit v1.2.3