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/Arith.lean | 409 ++++++++++++++++++++++++++++++++++++
 backends/lean/Base/Arith/Base.lean  |  10 +
 2 files changed, 419 insertions(+)
 create mode 100644 backends/lean/Base/Arith/Arith.lean
 create mode 100644 backends/lean/Base/Arith/Base.lean

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

diff --git a/backends/lean/Base/Arith/Arith.lean b/backends/lean/Base/Arith/Arith.lean
new file mode 100644
index 00000000..0ba73d18
--- /dev/null
+++ b/backends/lean/Base/Arith/Arith.lean
@@ -0,0 +1,409 @@
+/- This file contains tactics to solve arithmetic goals -/
+
+import Lean
+import Lean.Meta.Tactic.Simp
+import Init.Data.List.Basic
+import Mathlib.Tactic.RunCmd
+import Mathlib.Tactic.Linarith
+-- TODO: there is no Omega tactic for now - it seems it hasn't been ported yet
+--import Mathlib.Tactic.Omega
+import Base.Primitives
+import Base.Utils
+import Base.Arith.Base
+
+/-
+Mathlib tactics:
+- rcases: https://leanprover-community.github.io/mathlib_docs/tactics.html#rcases
+- split_ifs: https://leanprover-community.github.io/mathlib_docs/tactics.html#split_ifs
+- norm_num: https://leanprover-community.github.io/mathlib_docs/tactics.html#norm_num
+- should we use linarith or omega?
+- hint: https://leanprover-community.github.io/mathlib_docs/tactics.html#hint
+- classical: https://leanprover-community.github.io/mathlib_docs/tactics.html#classical
+-/
+
+namespace List
+
+  -- TODO: I could not find this function??
+  @[simp] def flatten {a : Type u} : List (List a) → List a
+  | [] => []
+  | x :: ls => x ++ flatten ls
+
+end List
+
+namespace Lean
+
+namespace LocalContext
+
+  open Lean Lean.Elab Command Term Lean.Meta
+
+  -- Small utility: return the list of declarations in the context, from
+  -- the last to the first.
+  def getAllDecls (lctx : Lean.LocalContext) : MetaM (List Lean.LocalDecl) :=
+    lctx.foldrM (fun d ls => do let d ← instantiateLocalDeclMVars d; pure (d :: ls)) []
+
+  -- Return the list of declarations in the context, but filter the
+  -- declarations which are considered as implementation details
+  def getDecls (lctx : Lean.LocalContext) : MetaM (List Lean.LocalDecl) := do
+    let ls ← lctx.getAllDecls
+    pure (ls.filter (fun d => not d.isImplementationDetail))
+
+end LocalContext
+
+end Lean
+
+namespace Arith
+
+open Primitives
+
+-- 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
+instance Vec.cast (a : Type): Coe (Vec a) (List a)  where coe := λ v => v.val
+
+-- TODO: move
+/- Remark: we can't write the following instance because of restrictions about
+   the type class parameters (`ty` doesn't appear in the return type, which is
+   forbidden):
+
+   ```
+   instance Scalar.cast (ty : ScalarTy) : Coe (Scalar ty) Int where coe := λ v => v.val
+   ```
+ -/
+def Scalar.toInt {ty : ScalarTy} (x : Scalar ty) : Int := x.val
+
+-- Remark: I tried a version of the shape `HasProp {a : Type} (x : a)`
+-- but the lookup didn't work
+class HasProp (a : Sort u) where
+  prop_ty : a → Prop
+  prop : ∀ x:a, prop_ty x
+
+instance (ty : ScalarTy) : HasProp (Scalar ty) where
+  -- prop_ty is inferred
+  prop := λ x => And.intro x.hmin x.hmax
+
+instance (a : Type) : HasProp (Vec a) where
+  prop_ty := λ v => v.val.length ≤ Scalar.max ScalarTy.Usize
+  prop := λ ⟨ _, l ⟩ => l
+
+class PropHasImp (x : Prop) where
+  concl : Prop
+  prop : x → concl
+
+-- This also works for `x ≠ y` because this expression reduces to `¬ x = y`
+-- and `Ne` is marked as `reducible`
+instance (x y : Int) : PropHasImp (¬ x = y) where
+  concl := x < y ∨ x > y
+  prop := λ (h:x ≠ y) => ne_is_lt_or_gt h
+
+open Lean Lean.Elab Command Term Lean.Meta
+
+-- Small utility: print all the declarations in the context
+elab "print_all_decls" : tactic => do
+  let ctx ← Lean.MonadLCtx.getLCtx
+  for decl in ← ctx.getDecls do
+    let ty ← Lean.Meta.inferType decl.toExpr
+    logInfo m!"{decl.toExpr} : {ty}"
+  pure ()
+
+-- Explore a term by decomposing the applications (we explore the applied
+-- functions and their arguments, but ignore lambdas, forall, etc. -
+-- should we go inside?).
+partial def foldTermApps (k : α → Expr → MetaM α) (s : α) (e : Expr) : MetaM α := do
+  -- We do it in a very simpler manner: we deconstruct applications,
+  -- and recursively explore the sub-expressions. Note that we do
+  -- not go inside foralls and abstractions (should we?).
+  e.withApp fun f args => do
+    let s ← k s f
+    args.foldlM (foldTermApps k) s
+
+-- Provided a function `k` which lookups type class instances on an expression,
+-- collect all the instances lookuped by applying `k` on the sub-expressions of `e`.
+def collectInstances
+  (k : Expr → MetaM (Option Expr)) (s : HashSet Expr) (e : Expr) : MetaM (HashSet Expr) := do
+  let k s e := do
+    match ← k e with
+    | none => pure s
+    | some i => pure (s.insert i)
+  foldTermApps k s e
+
+-- Similar to `collectInstances`, but explores all the local declarations in the
+-- main context.
+def collectInstancesFromMainCtx (k : Expr → MetaM (Option Expr)) : Tactic.TacticM (HashSet Expr) := do
+  Lean.Elab.Tactic.withMainContext do
+  -- Get the local context
+  let ctx ← Lean.MonadLCtx.getLCtx
+  -- Just a matter of precaution
+  let ctx ← instantiateLCtxMVars ctx
+  -- Initialize the hashset
+  let hs := HashSet.empty
+  -- Explore the declarations
+  let decls ← ctx.getDecls
+  decls.foldlM (fun hs d => collectInstances k hs d.toExpr) hs
+
+-- Return an instance of `HasProp` for `e` if it has some
+def lookupHasProp (e : Expr) : MetaM (Option Expr) := do
+  trace[Arith] "lookupHasProp"
+  -- TODO: do we need Lean.observing?
+  -- This actually eliminates the error messages
+  Lean.observing? do
+    trace[Arith] "lookupHasProp: observing"
+    let ty ← Lean.Meta.inferType e
+    let hasProp ← mkAppM ``HasProp #[ty]
+    let hasPropInst ← trySynthInstance hasProp
+    match hasPropInst with
+    | LOption.some i =>
+      trace[Arith] "Found HasProp instance"
+      let i_prop ← mkProjection i (Name.mkSimple "prop")
+      some (← mkAppM' i_prop #[e])
+    | _ => none
+
+-- Collect the instances of `HasProp` for the subexpressions in the context
+def collectHasPropInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do
+  collectInstancesFromMainCtx lookupHasProp
+
+elab "display_has_prop_instances" : tactic => do
+  trace[Arith] "Displaying the HasProp instances"
+  let hs ← collectHasPropInstancesFromMainCtx
+  hs.forM fun e => do
+    trace[Arith] "+ HasProp instance: {e}"
+
+example (x : U32) : True := by
+  let i : HasProp U32 := inferInstance
+  have p := @HasProp.prop _ i x
+  simp only [HasProp.prop_ty] at p
+  display_has_prop_instances
+  simp
+
+-- Return an instance of `PropHasImp` for `e` if it has some
+def lookupPropHasImp (e : Expr) : MetaM (Option Expr) := do
+  trace[Arith] "lookupPropHasImp"
+  -- TODO: do we need Lean.observing?
+  -- This actually eliminates the error messages
+  Lean.observing? do
+    trace[Arith] "lookupPropHasImp: observing"
+    let ty ← Lean.Meta.inferType e
+    trace[Arith] "lookupPropHasImp: ty: {ty}"
+    let cl ← mkAppM ``PropHasImp #[ty]
+    let inst ← trySynthInstance cl
+    match inst with
+    | LOption.some i =>
+      trace[Arith] "Found PropHasImp instance"
+      let i_prop ←  mkProjection i (Name.mkSimple "prop")
+      some (← mkAppM' i_prop #[e])
+    | _ => none
+
+-- Collect the instances of `PropHasImp` for the subexpressions in the context
+def collectPropHasImpInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do
+  collectInstancesFromMainCtx lookupPropHasImp
+
+elab "display_prop_has_imp_instances" : tactic => do
+  trace[Arith] "Displaying the PropHasImp instances"
+  let hs ← collectPropHasImpInstancesFromMainCtx
+  hs.forM fun e => do
+    trace[Arith] "+ PropHasImp instance: {e}"
+
+example (x y : Int) (_ : x ≠ y) (_ : ¬ x = y) : True := by
+  display_prop_has_imp_instances
+  simp
+
+-- Lookup instances in a context and introduce them with additional declarations.
+def introInstances (declToUnfold : Name) (lookup : Expr → MetaM (Option Expr)) : Tactic.TacticM (Array Expr) := do
+  let hs ← collectInstancesFromMainCtx lookup
+  hs.toArray.mapM fun e => do
+    let type ← inferType e
+    let name ← mkFreshUserName `h
+    -- Add a declaration
+    let nval ← Utils.addDecl name e type (asLet := false)
+    -- Simplify to unfold the declaration to unfold (i.e., the projector)
+    let simpTheorems ← Tactic.simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems)
+    -- Add the equational theorem for the decl to unfold
+    let simpTheorems ← simpTheorems.addDeclToUnfold declToUnfold
+    let congrTheorems ← getSimpCongrTheorems
+    let ctx : Simp.Context := { simpTheorems := #[simpTheorems], congrTheorems }
+    -- Where to apply the simplifier
+    let loc := Tactic.Location.targets #[mkIdent name] false
+    -- Apply the simplifier
+    let _ ← Tactic.simpLocation ctx (discharge? := .none) loc
+    -- Return the new value
+    pure nval
+
+-- Lookup the instances of `HasProp for all the sub-expressions in the context,
+-- and introduce the corresponding assumptions
+elab "intro_has_prop_instances" : tactic => do
+  trace[Arith] "Introducing the HasProp instances"
+  let _ ← introInstances ``HasProp.prop_ty lookupHasProp
+
+example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by
+  intro_has_prop_instances
+  simp [*]
+
+example {a: Type} (v : Vec a) : v.val.length ≤ Scalar.max ScalarTy.Usize := by
+  intro_has_prop_instances
+  simp_all [Scalar.max, Scalar.min]
+
+-- Tactic to split on a disjunction.
+-- The expression `h` should be an fvar.
+def splitDisj (h : Expr) (kleft kright : Tactic.TacticM Unit) : Tactic.TacticM Unit := do
+  trace[Arith] "assumption on which to split: {h}"
+  -- Retrieve the main goal
+  Lean.Elab.Tactic.withMainContext do
+  let goalType ← Lean.Elab.Tactic.getMainTarget
+  let hDecl := (← getLCtx).get! h.fvarId!
+  let hName := hDecl.userName
+  -- Case disjunction
+  let hTy ← inferType h
+  hTy.withApp fun f xs => do
+  trace[Arith] "as app: {f} {xs}"
+  -- Sanity check
+  if ¬ (f.isConstOf ``Or ∧ xs.size = 2) then throwError "Invalid argument to splitDisj"
+  let a := xs.get! 0
+  let b := xs.get! 1
+  -- Introduce the new goals
+  -- Returns:
+  -- - the match branch
+  -- - a fresh new mvar id
+  let mkGoal (hTy : Expr) (nGoalName : String) : MetaM (Expr × MVarId) := do
+    -- Introduce a variable for the assumption (`a` or `b`). Note that we reuse
+    -- the name of the assumption we split.
+    withLocalDeclD hName hTy fun var => do
+    -- The new goal
+    let mgoal ← mkFreshExprSyntheticOpaqueMVar goalType (tag := Name.mkSimple nGoalName)
+    -- Clear the assumption that we split
+    let mgoal ← mgoal.mvarId!.tryClearMany #[h.fvarId!]
+    -- The branch expression
+    let branch ← mkLambdaFVars #[var] (mkMVar mgoal)
+    pure (branch, mgoal)
+  let (inl, mleft) ← mkGoal a "left"
+  let (inr, mright) ← mkGoal b "right"
+  trace[Arith] "left: {inl}: {mleft}"
+  trace[Arith] "right: {inr}: {mright}"
+  -- Create the match expression
+  withLocalDeclD (← mkFreshUserName `h) hTy fun hVar => do
+  let motive ← mkLambdaFVars #[hVar] goalType
+  let casesExpr ← mkAppOptM ``Or.casesOn #[a, b, motive, h, inl, inr]
+  let mgoal ← Tactic.getMainGoal
+  trace[Arith] "goals: {← Tactic.getUnsolvedGoals}"
+  trace[Arith] "main goal: {mgoal}"
+  mgoal.assign casesExpr
+  let goals ← Tactic.getUnsolvedGoals
+  -- Focus on the left
+  Tactic.setGoals [mleft]
+  kleft
+  let leftGoals ← Tactic.getUnsolvedGoals
+  -- Focus on the right
+  Tactic.setGoals [mright]
+  kright
+  let rightGoals ← Tactic.getUnsolvedGoals
+  -- Put all the goals back
+  Tactic.setGoals (leftGoals ++ rightGoals ++ goals)
+  trace[Arith] "new goals: {← Tactic.getUnsolvedGoals}"
+
+elab "split_disj " n:ident : tactic => do
+  Lean.Elab.Tactic.withMainContext do
+  let decl ← Lean.Meta.getLocalDeclFromUserName n.getId
+  let fvar := mkFVar decl.fvarId
+  splitDisj fvar (fun _ => pure ()) (fun _ => pure ())
+
+example (x y : Int) (h0 : x ≤ y ∨ x ≥ y) : x ≤ y ∨ x ≥ y := by
+  split_disj h0
+  . left; assumption
+  . right; assumption
+
+-- Lookup the instances of `PropHasImp for all the sub-expressions in the context,
+-- and introduce the corresponding assumptions
+elab "intro_prop_has_imp_instances" : tactic => do
+  trace[Arith] "Introducing the PropHasImp instances"
+  let _ ← introInstances ``PropHasImp.concl lookupPropHasImp
+
+example (x y : Int) (h0 : x ≤ y) (h1 : x ≠ y) : x < y := by
+  intro_prop_has_imp_instances
+  rename_i h
+  split_disj h
+  . linarith
+  . linarith
+
+/- Boosting a bit the linarith tac.
+
+   We do the following:
+   - for all the assumptions of the shape `(x : Int) ≠ y` or `¬ (x = y), we
+     introduce two goals with the assumptions `x < y` and `x > y`
+     TODO: we could create a PR for mathlib.
+ -/
+def intTacPreprocess : Tactic.TacticM Unit := do
+  Lean.Elab.Tactic.withMainContext do
+  -- Lookup the instances of PropHasImp (this is how we detect assumptions
+  -- of the proper shape), introduce assumptions in the context and split
+  -- on those
+  -- TODO: get rid of the assumptions that we split
+  let rec splitOnAsms (asms : List Expr) : Tactic.TacticM Unit :=
+    match asms with
+    | [] => pure ()
+    | asm :: asms =>
+      let k := splitOnAsms asms
+      splitDisj asm k k
+  -- Introduce
+  let asms ← introInstances ``PropHasImp.concl lookupPropHasImp
+  -- Split
+  splitOnAsms asms.toList
+
+elab "int_tac_preprocess" : tactic =>
+  intTacPreprocess
+
+example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by
+  int_tac_preprocess
+  linarith
+  linarith
+
+syntax "int_tac" : tactic
+macro_rules
+  | `(tactic| int_tac) =>
+    `(tactic|
+      (repeat (apply And.intro)) <;> -- TODO: improve this
+      int_tac_preprocess <;>
+      linarith)
+
+example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by
+  int_tac
+
+-- Checking that things append correctly when there are several disjunctions
+example (x y : Int) (h0: 0 ≤ x) (h1: x ≠ 0) (h2 : 0 ≤ y) (h3 : y ≠ 0) : 0 < x ∧ 0 < y := by
+  int_tac
+
+-- A tactic to solve linear arithmetic goals in the presence of scalars
+syntax "scalar_tac" : tactic
+macro_rules
+  | `(tactic| scalar_tac) =>
+    `(tactic|
+      intro_has_prop_instances;
+      have := Scalar.cMin_bound ScalarTy.Usize;
+      have := Scalar.cMin_bound ScalarTy.Isize;
+      have := Scalar.cMax_bound ScalarTy.Usize;
+      have := Scalar.cMax_bound ScalarTy.Isize;
+      -- TODO: not too sure about that
+      simp only [*, Scalar.max, Scalar.min, Scalar.cMin, Scalar.cMax] at *;
+      int_tac)
+
+example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by
+  scalar_tac
+
+example {a: Type} (v : Vec a) : v.val.length ≤ Scalar.max ScalarTy.Usize := by
+  scalar_tac
+
+end Arith
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 6166c410a4b3353377e640acbae9f56e877a9118 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 11 Jul 2023 15:23:49 +0200
Subject: Work on the progress tactic

---
 backends/lean/Base/Arith/Arith.lean | 42 +++++++++++++++++++++++++------------
 1 file changed, 29 insertions(+), 13 deletions(-)

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

diff --git a/backends/lean/Base/Arith/Arith.lean b/backends/lean/Base/Arith/Arith.lean
index 0ba73d18..ff628cf3 100644
--- a/backends/lean/Base/Arith/Arith.lean
+++ b/backends/lean/Base/Arith/Arith.lean
@@ -146,7 +146,7 @@ def collectInstances
 -- Similar to `collectInstances`, but explores all the local declarations in the
 -- main context.
 def collectInstancesFromMainCtx (k : Expr → MetaM (Option Expr)) : Tactic.TacticM (HashSet Expr) := do
-  Lean.Elab.Tactic.withMainContext do
+  Tactic.withMainContext do
   -- Get the local context
   let ctx ← Lean.MonadLCtx.getLCtx
   -- Just a matter of precaution
@@ -263,8 +263,8 @@ example {a: Type} (v : Vec a) : v.val.length ≤ Scalar.max ScalarTy.Usize := by
 def splitDisj (h : Expr) (kleft kright : Tactic.TacticM Unit) : Tactic.TacticM Unit := do
   trace[Arith] "assumption on which to split: {h}"
   -- Retrieve the main goal
-  Lean.Elab.Tactic.withMainContext do
-  let goalType ← Lean.Elab.Tactic.getMainTarget
+  Tactic.withMainContext do
+  let goalType ← Tactic.getMainTarget
   let hDecl := (← getLCtx).get! h.fvarId!
   let hName := hDecl.userName
   -- Case disjunction
@@ -316,7 +316,7 @@ def splitDisj (h : Expr) (kleft kright : Tactic.TacticM Unit) : Tactic.TacticM U
   trace[Arith] "new goals: {← Tactic.getUnsolvedGoals}"
 
 elab "split_disj " n:ident : tactic => do
-  Lean.Elab.Tactic.withMainContext do
+  Tactic.withMainContext do
   let decl ← Lean.Meta.getLocalDeclFromUserName n.getId
   let fvar := mkFVar decl.fvarId
   splitDisj fvar (fun _ => pure ()) (fun _ => pure ())
@@ -347,7 +347,7 @@ example (x y : Int) (h0 : x ≤ y) (h1 : x ≠ y) : x < y := by
      TODO: we could create a PR for mathlib.
  -/
 def intTacPreprocess : Tactic.TacticM Unit := do
-  Lean.Elab.Tactic.withMainContext do
+  Tactic.withMainContext do
   -- Lookup the instances of PropHasImp (this is how we detect assumptions
   -- of the proper shape), introduce assumptions in the context and split
   -- on those
@@ -366,19 +366,31 @@ def intTacPreprocess : Tactic.TacticM Unit := do
 elab "int_tac_preprocess" : tactic =>
   intTacPreprocess
 
+def intTac : Tactic.TacticM Unit := do
+  Tactic.withMainContext do
+  Tactic.focus do
+  -- Preprocess - wondering if we should do this before or after splitting
+  -- the goal. I think before leads to a smaller proof term?
+  Tactic.allGoals intTacPreprocess
+  -- Split the conjunctions in the goal
+  Utils.repeatTac Utils.splitConjTarget
+  -- Call linarith
+  let linarith :=
+    let cfg : Linarith.LinarithConfig := {
+      -- We do this with our custom preprocessing
+      splitNe := false
+    }
+    Tactic.liftMetaFinishingTactic <| Linarith.linarith false [] cfg
+  Tactic.allGoals linarith
+
+elab "int_tac" : tactic =>
+  intTac
+
 example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by
   int_tac_preprocess
   linarith
   linarith
 
-syntax "int_tac" : tactic
-macro_rules
-  | `(tactic| int_tac) =>
-    `(tactic|
-      (repeat (apply And.intro)) <;> -- TODO: improve this
-      int_tac_preprocess <;>
-      linarith)
-
 example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by
   int_tac
 
@@ -386,6 +398,10 @@ example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by
 example (x y : Int) (h0: 0 ≤ x) (h1: x ≠ 0) (h2 : 0 ≤ y) (h3 : y ≠ 0) : 0 < x ∧ 0 < y := by
   int_tac
 
+-- Checking that things append correctly when there are several disjunctions
+example (x y : Int) (h0: 0 ≤ x) (h1: x ≠ 0) (h2 : 0 ≤ y) (h3 : y ≠ 0) : 0 < x ∧ 0 < y ∧ x + y ≥ 2 := by
+  int_tac
+
 -- A tactic to solve linear arithmetic goals in the presence of scalars
 syntax "scalar_tac" : tactic
 macro_rules
-- 
cgit v1.2.3


From a18d899a2c2b9bdd36f4a5a4b70472c12a835a96 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jul 2023 14:34:55 +0200
Subject: Finish a first version of the progress tactic

---
 backends/lean/Base/Arith/Arith.lean | 122 +++++++++---------------------------
 1 file changed, 29 insertions(+), 93 deletions(-)

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

diff --git a/backends/lean/Base/Arith/Arith.lean b/backends/lean/Base/Arith/Arith.lean
index ff628cf3..3557d350 100644
--- a/backends/lean/Base/Arith/Arith.lean
+++ b/backends/lean/Base/Arith/Arith.lean
@@ -230,25 +230,20 @@ def introInstances (declToUnfold : Name) (lookup : Expr → MetaM (Option Expr))
     let type ← inferType e
     let name ← mkFreshUserName `h
     -- Add a declaration
-    let nval ← Utils.addDecl name e type (asLet := false)
+    let nval ← Utils.addDeclTac name e type (asLet := false)
     -- Simplify to unfold the declaration to unfold (i.e., the projector)
-    let simpTheorems ← Tactic.simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems)
-    -- Add the equational theorem for the decl to unfold
-    let simpTheorems ← simpTheorems.addDeclToUnfold declToUnfold
-    let congrTheorems ← getSimpCongrTheorems
-    let ctx : Simp.Context := { simpTheorems := #[simpTheorems], congrTheorems }
-    -- Where to apply the simplifier
-    let loc := Tactic.Location.targets #[mkIdent name] false
-    -- Apply the simplifier
-    let _ ← Tactic.simpLocation ctx (discharge? := .none) loc
+    Utils.simpAt [declToUnfold] [] [] (Tactic.Location.targets #[mkIdent name] false)
     -- Return the new value
     pure nval
 
+def introHasPropInstances : Tactic.TacticM (Array Expr) := do
+  trace[Arith] "Introducing the HasProp instances"
+  introInstances ``HasProp.prop_ty lookupHasProp
+
 -- Lookup the instances of `HasProp for all the sub-expressions in the context,
 -- and introduce the corresponding assumptions
 elab "intro_has_prop_instances" : tactic => do
-  trace[Arith] "Introducing the HasProp instances"
-  let _ ← introInstances ``HasProp.prop_ty lookupHasProp
+  let _ ← introHasPropInstances
 
 example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by
   intro_has_prop_instances
@@ -258,74 +253,6 @@ example {a: Type} (v : Vec a) : v.val.length ≤ Scalar.max ScalarTy.Usize := by
   intro_has_prop_instances
   simp_all [Scalar.max, Scalar.min]
 
--- Tactic to split on a disjunction.
--- The expression `h` should be an fvar.
-def splitDisj (h : Expr) (kleft kright : Tactic.TacticM Unit) : Tactic.TacticM Unit := do
-  trace[Arith] "assumption on which to split: {h}"
-  -- Retrieve the main goal
-  Tactic.withMainContext do
-  let goalType ← Tactic.getMainTarget
-  let hDecl := (← getLCtx).get! h.fvarId!
-  let hName := hDecl.userName
-  -- Case disjunction
-  let hTy ← inferType h
-  hTy.withApp fun f xs => do
-  trace[Arith] "as app: {f} {xs}"
-  -- Sanity check
-  if ¬ (f.isConstOf ``Or ∧ xs.size = 2) then throwError "Invalid argument to splitDisj"
-  let a := xs.get! 0
-  let b := xs.get! 1
-  -- Introduce the new goals
-  -- Returns:
-  -- - the match branch
-  -- - a fresh new mvar id
-  let mkGoal (hTy : Expr) (nGoalName : String) : MetaM (Expr × MVarId) := do
-    -- Introduce a variable for the assumption (`a` or `b`). Note that we reuse
-    -- the name of the assumption we split.
-    withLocalDeclD hName hTy fun var => do
-    -- The new goal
-    let mgoal ← mkFreshExprSyntheticOpaqueMVar goalType (tag := Name.mkSimple nGoalName)
-    -- Clear the assumption that we split
-    let mgoal ← mgoal.mvarId!.tryClearMany #[h.fvarId!]
-    -- The branch expression
-    let branch ← mkLambdaFVars #[var] (mkMVar mgoal)
-    pure (branch, mgoal)
-  let (inl, mleft) ← mkGoal a "left"
-  let (inr, mright) ← mkGoal b "right"
-  trace[Arith] "left: {inl}: {mleft}"
-  trace[Arith] "right: {inr}: {mright}"
-  -- Create the match expression
-  withLocalDeclD (← mkFreshUserName `h) hTy fun hVar => do
-  let motive ← mkLambdaFVars #[hVar] goalType
-  let casesExpr ← mkAppOptM ``Or.casesOn #[a, b, motive, h, inl, inr]
-  let mgoal ← Tactic.getMainGoal
-  trace[Arith] "goals: {← Tactic.getUnsolvedGoals}"
-  trace[Arith] "main goal: {mgoal}"
-  mgoal.assign casesExpr
-  let goals ← Tactic.getUnsolvedGoals
-  -- Focus on the left
-  Tactic.setGoals [mleft]
-  kleft
-  let leftGoals ← Tactic.getUnsolvedGoals
-  -- Focus on the right
-  Tactic.setGoals [mright]
-  kright
-  let rightGoals ← Tactic.getUnsolvedGoals
-  -- Put all the goals back
-  Tactic.setGoals (leftGoals ++ rightGoals ++ goals)
-  trace[Arith] "new goals: {← Tactic.getUnsolvedGoals}"
-
-elab "split_disj " n:ident : tactic => do
-  Tactic.withMainContext do
-  let decl ← Lean.Meta.getLocalDeclFromUserName n.getId
-  let fvar := mkFVar decl.fvarId
-  splitDisj fvar (fun _ => pure ()) (fun _ => pure ())
-
-example (x y : Int) (h0 : x ≤ y ∨ x ≥ y) : x ≤ y ∨ x ≥ y := by
-  split_disj h0
-  . left; assumption
-  . right; assumption
-
 -- Lookup the instances of `PropHasImp for all the sub-expressions in the context,
 -- and introduce the corresponding assumptions
 elab "intro_prop_has_imp_instances" : tactic => do
@@ -357,7 +284,7 @@ def intTacPreprocess : Tactic.TacticM Unit := do
     | [] => pure ()
     | asm :: asms =>
       let k := splitOnAsms asms
-      splitDisj asm k k
+      Utils.splitDisjTac asm k k
   -- Introduce
   let asms ← introInstances ``PropHasImp.concl lookupPropHasImp
   -- Split
@@ -403,18 +330,27 @@ example (x y : Int) (h0: 0 ≤ x) (h1: x ≠ 0) (h2 : 0 ≤ y) (h3 : y ≠ 0) :
   int_tac
 
 -- A tactic to solve linear arithmetic goals in the presence of scalars
-syntax "scalar_tac" : tactic
-macro_rules
-  | `(tactic| scalar_tac) =>
-    `(tactic|
-      intro_has_prop_instances;
-      have := Scalar.cMin_bound ScalarTy.Usize;
-      have := Scalar.cMin_bound ScalarTy.Isize;
-      have := Scalar.cMax_bound ScalarTy.Usize;
-      have := Scalar.cMax_bound ScalarTy.Isize;
-      -- TODO: not too sure about that
-      simp only [*, Scalar.max, Scalar.min, Scalar.cMin, Scalar.cMax] at *;
-      int_tac)
+def scalarTac : Tactic.TacticM Unit := do
+  Tactic.withMainContext do
+  -- Introduce the scalar bounds
+  let _ ← introHasPropInstances
+  Tactic.allGoals 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.Usize []])
+  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 - TODO: not too sure about that.
+  -- Maybe we should reveal the "concrete" bounds (after normalization)
+  Utils.simpAt [``Scalar.max, ``Scalar.min, ``Scalar.cMin, ``Scalar.cMax] [] [] .wildcard
+  -- Apply the integer tactic
+  intTac
+
+elab "scalar_tac" : tactic =>
+  scalarTac
 
 example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by
   scalar_tac
-- 
cgit v1.2.3


From 59e4a06480b5365f48dc68de80f44841f94094ed Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jul 2023 15:41:29 +0200
Subject: Improve the handling of arithmetic bounds

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

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

diff --git a/backends/lean/Base/Arith/Arith.lean b/backends/lean/Base/Arith/Arith.lean
index 3557d350..20420f36 100644
--- a/backends/lean/Base/Arith/Arith.lean
+++ b/backends/lean/Base/Arith/Arith.lean
@@ -339,13 +339,17 @@ def scalarTac : Tactic.TacticM Unit := do
   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.Usize []])
   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 - TODO: not too sure about that.
   -- Maybe we should reveal the "concrete" bounds (after normalization)
-  Utils.simpAt [``Scalar.max, ``Scalar.min, ``Scalar.cMin, ``Scalar.cMax] [] [] .wildcard
+  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
   -- Apply the integer tactic
   intTac
 
-- 
cgit v1.2.3


From eb97bdb6761437e492bcf1a95b4fa43d2b69601b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jul 2023 18:04:19 +0200
Subject: Improve progress to use assumptions and start working on a nice
 syntax

---
 backends/lean/Base/Arith/Arith.lean | 42 +------------------------------------
 1 file changed, 1 insertion(+), 41 deletions(-)

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

diff --git a/backends/lean/Base/Arith/Arith.lean b/backends/lean/Base/Arith/Arith.lean
index 20420f36..ab4fd182 100644
--- a/backends/lean/Base/Arith/Arith.lean
+++ b/backends/lean/Base/Arith/Arith.lean
@@ -11,49 +11,9 @@ import Base.Primitives
 import Base.Utils
 import Base.Arith.Base
 
-/-
-Mathlib tactics:
-- rcases: https://leanprover-community.github.io/mathlib_docs/tactics.html#rcases
-- split_ifs: https://leanprover-community.github.io/mathlib_docs/tactics.html#split_ifs
-- norm_num: https://leanprover-community.github.io/mathlib_docs/tactics.html#norm_num
-- should we use linarith or omega?
-- hint: https://leanprover-community.github.io/mathlib_docs/tactics.html#hint
-- classical: https://leanprover-community.github.io/mathlib_docs/tactics.html#classical
--/
-
-namespace List
-
-  -- TODO: I could not find this function??
-  @[simp] def flatten {a : Type u} : List (List a) → List a
-  | [] => []
-  | x :: ls => x ++ flatten ls
-
-end List
-
-namespace Lean
-
-namespace LocalContext
-
-  open Lean Lean.Elab Command Term Lean.Meta
-
-  -- Small utility: return the list of declarations in the context, from
-  -- the last to the first.
-  def getAllDecls (lctx : Lean.LocalContext) : MetaM (List Lean.LocalDecl) :=
-    lctx.foldrM (fun d ls => do let d ← instantiateLocalDeclMVars d; pure (d :: ls)) []
-
-  -- Return the list of declarations in the context, but filter the
-  -- declarations which are considered as implementation details
-  def getDecls (lctx : Lean.LocalContext) : MetaM (List Lean.LocalDecl) := do
-    let ls ← lctx.getAllDecls
-    pure (ls.filter (fun d => not d.isImplementationDetail))
-
-end LocalContext
-
-end Lean
-
 namespace Arith
 
-open Primitives
+open Primitives Utils
 
 -- TODO: move?
 theorem ne_zero_is_lt_or_gt {x : Int} (hne : x ≠ 0) : x < 0 ∨ x > 0 := by
-- 
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/Arith.lean | 136 +++++++++++++++++++-----------------
 backends/lean/Base/Arith/Base.lean  |  40 +++++++++++
 2 files changed, 112 insertions(+), 64 deletions(-)

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

diff --git a/backends/lean/Base/Arith/Arith.lean b/backends/lean/Base/Arith/Arith.lean
index ab4fd182..2ff030fe 100644
--- a/backends/lean/Base/Arith/Arith.lean
+++ b/backends/lean/Base/Arith/Arith.lean
@@ -15,25 +15,6 @@ namespace Arith
 
 open Primitives Utils
 
--- 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
 instance Vec.cast (a : Type): Coe (Vec a) (List a)  where coe := λ v => v.val
 
@@ -48,17 +29,21 @@ instance Vec.cast (a : Type): Coe (Vec a) (List a)  where coe := λ v => v.val
  -/
 def Scalar.toInt {ty : ScalarTy} (x : Scalar ty) : Int := x.val
 
--- Remark: I tried a version of the shape `HasProp {a : Type} (x : a)`
+-- Remark: I tried a version of the shape `HasScalarProp {a : Type} (x : a)`
 -- but the lookup didn't work
-class HasProp (a : Sort u) where
+class HasScalarProp (a : Sort u) where
+  prop_ty : a → Prop
+  prop : ∀ x:a, prop_ty x
+
+class HasIntProp (a : Sort u) where
   prop_ty : a → Prop
   prop : ∀ x:a, prop_ty x
 
-instance (ty : ScalarTy) : HasProp (Scalar ty) where
+instance (ty : ScalarTy) : HasScalarProp (Scalar ty) where
   -- prop_ty is inferred
   prop := λ x => And.intro x.hmin x.hmax
 
-instance (a : Type) : HasProp (Vec a) where
+instance (a : Type) : HasScalarProp (Vec a) where
   prop_ty := λ v => v.val.length ≤ Scalar.max ScalarTy.Usize
   prop := λ ⟨ _, l ⟩ => l
 
@@ -117,37 +102,49 @@ def collectInstancesFromMainCtx (k : Expr → MetaM (Option Expr)) : Tactic.Tact
   let decls ← ctx.getDecls
   decls.foldlM (fun hs d => collectInstances k hs d.toExpr) hs
 
--- Return an instance of `HasProp` for `e` if it has some
-def lookupHasProp (e : Expr) : MetaM (Option Expr) := do
-  trace[Arith] "lookupHasProp"
+-- Helper
+def lookupProp (fName : String) (className : Name) (e : Expr) : MetaM (Option Expr) := do
+  trace[Arith] fName
   -- TODO: do we need Lean.observing?
   -- This actually eliminates the error messages
   Lean.observing? do
-    trace[Arith] "lookupHasProp: observing"
+    trace[Arith] m!"{fName}: observing"
     let ty ← Lean.Meta.inferType e
-    let hasProp ← mkAppM ``HasProp #[ty]
+    let hasProp ← mkAppM className #[ty]
     let hasPropInst ← trySynthInstance hasProp
     match hasPropInst with
     | LOption.some i =>
-      trace[Arith] "Found HasProp instance"
+      trace[Arith] "Found HasScalarProp instance"
       let i_prop ← mkProjection i (Name.mkSimple "prop")
       some (← mkAppM' i_prop #[e])
     | _ => none
 
--- Collect the instances of `HasProp` for the subexpressions in the context
-def collectHasPropInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do
-  collectInstancesFromMainCtx lookupHasProp
+-- Return an instance of `HasIntProp` for `e` if it has some
+def lookupHasIntProp (e : Expr) : MetaM (Option Expr) :=
+  lookupProp "lookupHasScalarProp" ``HasIntProp e
+
+-- Return an instance of `HasScalarProp` for `e` if it has some
+def lookupHasScalarProp (e : Expr) : MetaM (Option Expr) :=
+  lookupProp "lookupHasScalarProp" ``HasScalarProp e
+
+-- Collect the instances of `HasIntProp` for the subexpressions in the context
+def collectHasIntPropInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do
+  collectInstancesFromMainCtx lookupHasIntProp
+
+-- Collect the instances of `HasScalarProp` for the subexpressions in the context
+def collectHasScalarPropInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do
+  collectInstancesFromMainCtx lookupHasScalarProp
 
 elab "display_has_prop_instances" : tactic => do
-  trace[Arith] "Displaying the HasProp instances"
-  let hs ← collectHasPropInstancesFromMainCtx
+  trace[Arith] "Displaying the HasScalarProp instances"
+  let hs ← collectHasScalarPropInstancesFromMainCtx
   hs.forM fun e => do
-    trace[Arith] "+ HasProp instance: {e}"
+    trace[Arith] "+ HasScalarProp instance: {e}"
 
 example (x : U32) : True := by
-  let i : HasProp U32 := inferInstance
-  have p := @HasProp.prop _ i x
-  simp only [HasProp.prop_ty] at p
+  let i : HasScalarProp U32 := inferInstance
+  have p := @HasScalarProp.prop _ i x
+  simp only [HasScalarProp.prop_ty] at p
   display_has_prop_instances
   simp
 
@@ -196,14 +193,18 @@ def introInstances (declToUnfold : Name) (lookup : Expr → MetaM (Option Expr))
     -- Return the new value
     pure nval
 
-def introHasPropInstances : Tactic.TacticM (Array Expr) := do
-  trace[Arith] "Introducing the HasProp instances"
-  introInstances ``HasProp.prop_ty lookupHasProp
+def introHasIntPropInstances : Tactic.TacticM (Array Expr) := do
+  trace[Arith] "Introducing the HasIntProp instances"
+  introInstances ``HasIntProp.prop_ty lookupHasIntProp
+
+def introHasScalarPropInstances : Tactic.TacticM (Array Expr) := do
+  trace[Arith] "Introducing the HasScalarProp instances"
+  introInstances ``HasScalarProp.prop_ty lookupHasScalarProp
 
--- Lookup the instances of `HasProp for all the sub-expressions in the context,
+-- Lookup the instances of `HasScalarProp for all the sub-expressions in the context,
 -- and introduce the corresponding assumptions
 elab "intro_has_prop_instances" : tactic => do
-  let _ ← introHasPropInstances
+  let _ ← introHasScalarPropInstances
 
 example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by
   intro_has_prop_instances
@@ -246,6 +247,7 @@ def intTacPreprocess : Tactic.TacticM Unit := do
       let k := splitOnAsms asms
       Utils.splitDisjTac asm k k
   -- Introduce
+  let _ ← introHasIntPropInstances
   let asms ← introInstances ``PropHasImp.concl lookupPropHasImp
   -- Split
   splitOnAsms asms.toList
@@ -289,29 +291,35 @@ example (x y : Int) (h0: 0 ≤ x) (h1: x ≠ 0) (h2 : 0 ≤ y) (h3 : y ≠ 0) :
 example (x y : Int) (h0: 0 ≤ x) (h1: x ≠ 0) (h2 : 0 ≤ y) (h3 : y ≠ 0) : 0 < x ∧ 0 < y ∧ x + y ≥ 2 := by
   int_tac
 
+def scalarTacPreprocess (tac : Tactic.TacticM Unit) : Tactic.TacticM Unit := do
+   Tactic.withMainContext do
+   -- Introduce the scalar bounds
+   let _ ← introHasScalarPropInstances
+   Tactic.allGoals 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 - TODO: not too sure about that.
+   -- Maybe we should reveal the "concrete" bounds (after normalization)
+   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
+   -- Finish the proof
+   tac
+
+elab "scalar_tac_preprocess" : tactic =>
+  scalarTacPreprocess intTacPreprocess
+
 -- A tactic to solve linear arithmetic goals in the presence of scalars
 def scalarTac : Tactic.TacticM Unit := do
-  Tactic.withMainContext do
-  -- Introduce the scalar bounds
-  let _ ← introHasPropInstances
-  Tactic.allGoals 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 - TODO: not too sure about that.
-  -- Maybe we should reveal the "concrete" bounds (after normalization)
-  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
-  -- Apply the integer tactic
-  intTac
+  scalarTacPreprocess intTac
 
 elab "scalar_tac" : tactic =>
   scalarTac
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 a9a3376443e4c6d9a5257bdd310966a59aa9e716 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 13 Jul 2023 14:00:48 +0200
Subject: Update a comment

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

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

diff --git a/backends/lean/Base/Arith/Arith.lean b/backends/lean/Base/Arith/Arith.lean
index 2ff030fe..8bfad6ae 100644
--- a/backends/lean/Base/Arith/Arith.lean
+++ b/backends/lean/Base/Arith/Arith.lean
@@ -303,8 +303,7 @@ def scalarTacPreprocess (tac : Tactic.TacticM Unit) : Tactic.TacticM Unit := do
    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 - TODO: not too sure about that.
-   -- Maybe we should reveal the "concrete" bounds (after normalization)
+   -- 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,
-- 
cgit v1.2.3


From d45c6ed9e8049b81170c3e6950043d08006ba9f2 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 17 Jul 2023 12:14:03 +0200
Subject: Move a definition

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

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

diff --git a/backends/lean/Base/Arith/Arith.lean b/backends/lean/Base/Arith/Arith.lean
index 8bfad6ae..da263e86 100644
--- a/backends/lean/Base/Arith/Arith.lean
+++ b/backends/lean/Base/Arith/Arith.lean
@@ -15,9 +15,6 @@ namespace Arith
 
 open Primitives Utils
 
--- TODO: move
-instance Vec.cast (a : Type): Coe (Vec a) (List a)  where coe := λ v => v.val
-
 -- TODO: move
 /- Remark: we can't write the following instance because of restrictions about
    the type class parameters (`ty` doesn't appear in the return type, which is
-- 
cgit v1.2.3


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/Arith.lean  | 329 -----------------------------------
 backends/lean/Base/Arith/Int.lean    | 236 +++++++++++++++++++++++++
 backends/lean/Base/Arith/Scalar.lean |  48 +++++
 3 files changed, 284 insertions(+), 329 deletions(-)
 create mode 100644 backends/lean/Base/Arith/Int.lean
 create mode 100644 backends/lean/Base/Arith/Scalar.lean

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

diff --git a/backends/lean/Base/Arith/Arith.lean b/backends/lean/Base/Arith/Arith.lean
index da263e86..e69de29b 100644
--- a/backends/lean/Base/Arith/Arith.lean
+++ b/backends/lean/Base/Arith/Arith.lean
@@ -1,329 +0,0 @@
-/- This file contains tactics to solve arithmetic goals -/
-
-import Lean
-import Lean.Meta.Tactic.Simp
-import Init.Data.List.Basic
-import Mathlib.Tactic.RunCmd
-import Mathlib.Tactic.Linarith
--- TODO: there is no Omega tactic for now - it seems it hasn't been ported yet
---import Mathlib.Tactic.Omega
-import Base.Primitives
-import Base.Utils
-import Base.Arith.Base
-
-namespace Arith
-
-open Primitives Utils
-
--- TODO: move
-/- Remark: we can't write the following instance because of restrictions about
-   the type class parameters (`ty` doesn't appear in the return type, which is
-   forbidden):
-
-   ```
-   instance Scalar.cast (ty : ScalarTy) : Coe (Scalar ty) Int where coe := λ v => v.val
-   ```
- -/
-def Scalar.toInt {ty : ScalarTy} (x : Scalar ty) : Int := x.val
-
--- Remark: I tried a version of the shape `HasScalarProp {a : Type} (x : a)`
--- but the lookup didn't work
-class HasScalarProp (a : Sort u) where
-  prop_ty : a → Prop
-  prop : ∀ x:a, prop_ty x
-
-class HasIntProp (a : Sort u) where
-  prop_ty : a → Prop
-  prop : ∀ x:a, prop_ty x
-
-instance (ty : ScalarTy) : HasScalarProp (Scalar ty) where
-  -- prop_ty is inferred
-  prop := λ x => And.intro x.hmin x.hmax
-
-instance (a : Type) : HasScalarProp (Vec a) where
-  prop_ty := λ v => v.val.length ≤ Scalar.max ScalarTy.Usize
-  prop := λ ⟨ _, l ⟩ => l
-
-class PropHasImp (x : Prop) where
-  concl : Prop
-  prop : x → concl
-
--- This also works for `x ≠ y` because this expression reduces to `¬ x = y`
--- and `Ne` is marked as `reducible`
-instance (x y : Int) : PropHasImp (¬ x = y) where
-  concl := x < y ∨ x > y
-  prop := λ (h:x ≠ y) => ne_is_lt_or_gt h
-
-open Lean Lean.Elab Command Term Lean.Meta
-
--- Small utility: print all the declarations in the context
-elab "print_all_decls" : tactic => do
-  let ctx ← Lean.MonadLCtx.getLCtx
-  for decl in ← ctx.getDecls do
-    let ty ← Lean.Meta.inferType decl.toExpr
-    logInfo m!"{decl.toExpr} : {ty}"
-  pure ()
-
--- Explore a term by decomposing the applications (we explore the applied
--- functions and their arguments, but ignore lambdas, forall, etc. -
--- should we go inside?).
-partial def foldTermApps (k : α → Expr → MetaM α) (s : α) (e : Expr) : MetaM α := do
-  -- We do it in a very simpler manner: we deconstruct applications,
-  -- and recursively explore the sub-expressions. Note that we do
-  -- not go inside foralls and abstractions (should we?).
-  e.withApp fun f args => do
-    let s ← k s f
-    args.foldlM (foldTermApps k) s
-
--- Provided a function `k` which lookups type class instances on an expression,
--- collect all the instances lookuped by applying `k` on the sub-expressions of `e`.
-def collectInstances
-  (k : Expr → MetaM (Option Expr)) (s : HashSet Expr) (e : Expr) : MetaM (HashSet Expr) := do
-  let k s e := do
-    match ← k e with
-    | none => pure s
-    | some i => pure (s.insert i)
-  foldTermApps k s e
-
--- Similar to `collectInstances`, but explores all the local declarations in the
--- main context.
-def collectInstancesFromMainCtx (k : Expr → MetaM (Option Expr)) : Tactic.TacticM (HashSet Expr) := do
-  Tactic.withMainContext do
-  -- Get the local context
-  let ctx ← Lean.MonadLCtx.getLCtx
-  -- Just a matter of precaution
-  let ctx ← instantiateLCtxMVars ctx
-  -- Initialize the hashset
-  let hs := HashSet.empty
-  -- Explore the declarations
-  let decls ← ctx.getDecls
-  decls.foldlM (fun hs d => collectInstances k hs d.toExpr) hs
-
--- Helper
-def lookupProp (fName : String) (className : Name) (e : Expr) : MetaM (Option Expr) := do
-  trace[Arith] fName
-  -- TODO: do we need Lean.observing?
-  -- This actually eliminates the error messages
-  Lean.observing? do
-    trace[Arith] m!"{fName}: observing"
-    let ty ← Lean.Meta.inferType e
-    let hasProp ← mkAppM className #[ty]
-    let hasPropInst ← trySynthInstance hasProp
-    match hasPropInst with
-    | LOption.some i =>
-      trace[Arith] "Found HasScalarProp instance"
-      let i_prop ← mkProjection i (Name.mkSimple "prop")
-      some (← mkAppM' i_prop #[e])
-    | _ => none
-
--- Return an instance of `HasIntProp` for `e` if it has some
-def lookupHasIntProp (e : Expr) : MetaM (Option Expr) :=
-  lookupProp "lookupHasScalarProp" ``HasIntProp e
-
--- Return an instance of `HasScalarProp` for `e` if it has some
-def lookupHasScalarProp (e : Expr) : MetaM (Option Expr) :=
-  lookupProp "lookupHasScalarProp" ``HasScalarProp e
-
--- Collect the instances of `HasIntProp` for the subexpressions in the context
-def collectHasIntPropInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do
-  collectInstancesFromMainCtx lookupHasIntProp
-
--- Collect the instances of `HasScalarProp` for the subexpressions in the context
-def collectHasScalarPropInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do
-  collectInstancesFromMainCtx lookupHasScalarProp
-
-elab "display_has_prop_instances" : tactic => do
-  trace[Arith] "Displaying the HasScalarProp instances"
-  let hs ← collectHasScalarPropInstancesFromMainCtx
-  hs.forM fun e => do
-    trace[Arith] "+ HasScalarProp instance: {e}"
-
-example (x : U32) : True := by
-  let i : HasScalarProp U32 := inferInstance
-  have p := @HasScalarProp.prop _ i x
-  simp only [HasScalarProp.prop_ty] at p
-  display_has_prop_instances
-  simp
-
--- Return an instance of `PropHasImp` for `e` if it has some
-def lookupPropHasImp (e : Expr) : MetaM (Option Expr) := do
-  trace[Arith] "lookupPropHasImp"
-  -- TODO: do we need Lean.observing?
-  -- This actually eliminates the error messages
-  Lean.observing? do
-    trace[Arith] "lookupPropHasImp: observing"
-    let ty ← Lean.Meta.inferType e
-    trace[Arith] "lookupPropHasImp: ty: {ty}"
-    let cl ← mkAppM ``PropHasImp #[ty]
-    let inst ← trySynthInstance cl
-    match inst with
-    | LOption.some i =>
-      trace[Arith] "Found PropHasImp instance"
-      let i_prop ←  mkProjection i (Name.mkSimple "prop")
-      some (← mkAppM' i_prop #[e])
-    | _ => none
-
--- Collect the instances of `PropHasImp` for the subexpressions in the context
-def collectPropHasImpInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do
-  collectInstancesFromMainCtx lookupPropHasImp
-
-elab "display_prop_has_imp_instances" : tactic => do
-  trace[Arith] "Displaying the PropHasImp instances"
-  let hs ← collectPropHasImpInstancesFromMainCtx
-  hs.forM fun e => do
-    trace[Arith] "+ PropHasImp instance: {e}"
-
-example (x y : Int) (_ : x ≠ y) (_ : ¬ x = y) : True := by
-  display_prop_has_imp_instances
-  simp
-
--- Lookup instances in a context and introduce them with additional declarations.
-def introInstances (declToUnfold : Name) (lookup : Expr → MetaM (Option Expr)) : Tactic.TacticM (Array Expr) := do
-  let hs ← collectInstancesFromMainCtx lookup
-  hs.toArray.mapM fun e => do
-    let type ← inferType e
-    let name ← mkFreshUserName `h
-    -- Add a declaration
-    let nval ← Utils.addDeclTac name e type (asLet := false)
-    -- Simplify to unfold the declaration to unfold (i.e., the projector)
-    Utils.simpAt [declToUnfold] [] [] (Tactic.Location.targets #[mkIdent name] false)
-    -- Return the new value
-    pure nval
-
-def introHasIntPropInstances : Tactic.TacticM (Array Expr) := do
-  trace[Arith] "Introducing the HasIntProp instances"
-  introInstances ``HasIntProp.prop_ty lookupHasIntProp
-
-def introHasScalarPropInstances : Tactic.TacticM (Array Expr) := do
-  trace[Arith] "Introducing the HasScalarProp instances"
-  introInstances ``HasScalarProp.prop_ty lookupHasScalarProp
-
--- Lookup the instances of `HasScalarProp for all the sub-expressions in the context,
--- and introduce the corresponding assumptions
-elab "intro_has_prop_instances" : tactic => do
-  let _ ← introHasScalarPropInstances
-
-example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by
-  intro_has_prop_instances
-  simp [*]
-
-example {a: Type} (v : Vec a) : v.val.length ≤ Scalar.max ScalarTy.Usize := by
-  intro_has_prop_instances
-  simp_all [Scalar.max, Scalar.min]
-
--- Lookup the instances of `PropHasImp for all the sub-expressions in the context,
--- and introduce the corresponding assumptions
-elab "intro_prop_has_imp_instances" : tactic => do
-  trace[Arith] "Introducing the PropHasImp instances"
-  let _ ← introInstances ``PropHasImp.concl lookupPropHasImp
-
-example (x y : Int) (h0 : x ≤ y) (h1 : x ≠ y) : x < y := by
-  intro_prop_has_imp_instances
-  rename_i h
-  split_disj h
-  . linarith
-  . linarith
-
-/- Boosting a bit the linarith tac.
-
-   We do the following:
-   - for all the assumptions of the shape `(x : Int) ≠ y` or `¬ (x = y), we
-     introduce two goals with the assumptions `x < y` and `x > y`
-     TODO: we could create a PR for mathlib.
- -/
-def intTacPreprocess : Tactic.TacticM Unit := do
-  Tactic.withMainContext do
-  -- Lookup the instances of PropHasImp (this is how we detect assumptions
-  -- of the proper shape), introduce assumptions in the context and split
-  -- on those
-  -- TODO: get rid of the assumptions that we split
-  let rec splitOnAsms (asms : List Expr) : Tactic.TacticM Unit :=
-    match asms with
-    | [] => pure ()
-    | asm :: asms =>
-      let k := splitOnAsms asms
-      Utils.splitDisjTac asm k k
-  -- Introduce
-  let _ ← introHasIntPropInstances
-  let asms ← introInstances ``PropHasImp.concl lookupPropHasImp
-  -- Split
-  splitOnAsms asms.toList
-
-elab "int_tac_preprocess" : tactic =>
-  intTacPreprocess
-
-def intTac : Tactic.TacticM Unit := do
-  Tactic.withMainContext do
-  Tactic.focus do
-  -- Preprocess - wondering if we should do this before or after splitting
-  -- the goal. I think before leads to a smaller proof term?
-  Tactic.allGoals intTacPreprocess
-  -- Split the conjunctions in the goal
-  Utils.repeatTac Utils.splitConjTarget
-  -- Call linarith
-  let linarith :=
-    let cfg : Linarith.LinarithConfig := {
-      -- We do this with our custom preprocessing
-      splitNe := false
-    }
-    Tactic.liftMetaFinishingTactic <| Linarith.linarith false [] cfg
-  Tactic.allGoals linarith
-
-elab "int_tac" : tactic =>
-  intTac
-
-example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by
-  int_tac_preprocess
-  linarith
-  linarith
-
-example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by
-  int_tac
-
--- Checking that things append correctly when there are several disjunctions
-example (x y : Int) (h0: 0 ≤ x) (h1: x ≠ 0) (h2 : 0 ≤ y) (h3 : y ≠ 0) : 0 < x ∧ 0 < y := by
-  int_tac
-
--- Checking that things append correctly when there are several disjunctions
-example (x y : Int) (h0: 0 ≤ x) (h1: x ≠ 0) (h2 : 0 ≤ y) (h3 : y ≠ 0) : 0 < x ∧ 0 < y ∧ x + y ≥ 2 := by
-  int_tac
-
-def scalarTacPreprocess (tac : Tactic.TacticM Unit) : Tactic.TacticM Unit := do
-   Tactic.withMainContext do
-   -- Introduce the scalar bounds
-   let _ ← introHasScalarPropInstances
-   Tactic.allGoals 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
-   -- Finish the proof
-   tac
-
-elab "scalar_tac_preprocess" : tactic =>
-  scalarTacPreprocess intTacPreprocess
-
--- A tactic to solve linear arithmetic goals in the presence of scalars
-def scalarTac : Tactic.TacticM Unit := do
-  scalarTacPreprocess intTac
-
-elab "scalar_tac" : tactic =>
-  scalarTac
-
-example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by
-  scalar_tac
-
-example {a: Type} (v : Vec a) : v.val.length ≤ Scalar.max ScalarTy.Usize := by
-  scalar_tac
-
-end Arith
diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
new file mode 100644
index 00000000..5f00ab52
--- /dev/null
+++ b/backends/lean/Base/Arith/Int.lean
@@ -0,0 +1,236 @@
+/- This file contains tactics to solve arithmetic goals -/
+
+import Lean
+import Lean.Meta.Tactic.Simp
+import Init.Data.List.Basic
+import Mathlib.Tactic.RunCmd
+import Mathlib.Tactic.Linarith
+-- TODO: there is no Omega tactic for now - it seems it hasn't been ported yet
+--import Mathlib.Tactic.Omega
+import Base.Utils
+import Base.Arith.Base
+
+namespace Arith
+
+open Utils
+
+-- Remark: I tried a version of the shape `HasScalarProp {a : Type} (x : a)`
+-- but the lookup didn't work
+class HasIntProp (a : Sort u) where
+  prop_ty : a → Prop
+  prop : ∀ x:a, prop_ty x
+
+class PropHasImp (x : Prop) where
+  concl : Prop
+  prop : x → concl
+
+-- This also works for `x ≠ y` because this expression reduces to `¬ x = y`
+-- and `Ne` is marked as `reducible`
+instance (x y : Int) : PropHasImp (¬ x = y) where
+  concl := x < y ∨ x > y
+  prop := λ (h:x ≠ y) => ne_is_lt_or_gt h
+
+open Lean Lean.Elab Lean.Meta
+
+-- Small utility: print all the declarations in the context
+elab "print_all_decls" : tactic => do
+  let ctx ← Lean.MonadLCtx.getLCtx
+  for decl in ← ctx.getDecls do
+    let ty ← Lean.Meta.inferType decl.toExpr
+    logInfo m!"{decl.toExpr} : {ty}"
+  pure ()
+
+-- Explore a term by decomposing the applications (we explore the applied
+-- functions and their arguments, but ignore lambdas, forall, etc. -
+-- should we go inside?).
+partial def foldTermApps (k : α → Expr → MetaM α) (s : α) (e : Expr) : MetaM α := do
+  -- We do it in a very simpler manner: we deconstruct applications,
+  -- and recursively explore the sub-expressions. Note that we do
+  -- not go inside foralls and abstractions (should we?).
+  e.withApp fun f args => do
+    let s ← k s f
+    args.foldlM (foldTermApps k) s
+
+-- Provided a function `k` which lookups type class instances on an expression,
+-- collect all the instances lookuped by applying `k` on the sub-expressions of `e`.
+def collectInstances
+  (k : Expr → MetaM (Option Expr)) (s : HashSet Expr) (e : Expr) : MetaM (HashSet Expr) := do
+  let k s e := do
+    match ← k e with
+    | none => pure s
+    | some i => pure (s.insert i)
+  foldTermApps k s e
+
+-- Similar to `collectInstances`, but explores all the local declarations in the
+-- main context.
+def collectInstancesFromMainCtx (k : Expr → MetaM (Option Expr)) : Tactic.TacticM (HashSet Expr) := do
+  Tactic.withMainContext do
+  -- Get the local context
+  let ctx ← Lean.MonadLCtx.getLCtx
+  -- Just a matter of precaution
+  let ctx ← instantiateLCtxMVars ctx
+  -- Initialize the hashset
+  let hs := HashSet.empty
+  -- Explore the declarations
+  let decls ← ctx.getDecls
+  decls.foldlM (fun hs d => collectInstances k hs d.toExpr) hs
+
+-- Helper
+def lookupProp (fName : String) (className : Name) (e : Expr) : MetaM (Option Expr) := do
+  trace[Arith] fName
+  -- TODO: do we need Lean.observing?
+  -- This actually eliminates the error messages
+  Lean.observing? do
+    trace[Arith] m!"{fName}: observing"
+    let ty ← Lean.Meta.inferType e
+    let hasProp ← mkAppM className #[ty]
+    let hasPropInst ← trySynthInstance hasProp
+    match hasPropInst with
+    | LOption.some i =>
+      trace[Arith] "Found {fName} instance"
+      let i_prop ← mkProjection i (Name.mkSimple "prop")
+      some (← mkAppM' i_prop #[e])
+    | _ => none
+
+-- Return an instance of `HasIntProp` for `e` if it has some
+def lookupHasIntProp (e : Expr) : MetaM (Option Expr) :=
+  lookupProp "lookupHasIntProp" ``HasIntProp e
+
+-- Collect the instances of `HasIntProp` for the subexpressions in the context
+def collectHasIntPropInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do
+  collectInstancesFromMainCtx lookupHasIntProp
+
+-- Return an instance of `PropHasImp` for `e` if it has some
+def lookupPropHasImp (e : Expr) : MetaM (Option Expr) := do
+  trace[Arith] "lookupPropHasImp"
+  -- TODO: do we need Lean.observing?
+  -- This actually eliminates the error messages
+  Lean.observing? do
+    trace[Arith] "lookupPropHasImp: observing"
+    let ty ← Lean.Meta.inferType e
+    trace[Arith] "lookupPropHasImp: ty: {ty}"
+    let cl ← mkAppM ``PropHasImp #[ty]
+    let inst ← trySynthInstance cl
+    match inst with
+    | LOption.some i =>
+      trace[Arith] "Found PropHasImp instance"
+      let i_prop ←  mkProjection i (Name.mkSimple "prop")
+      some (← mkAppM' i_prop #[e])
+    | _ => none
+
+-- Collect the instances of `PropHasImp` for the subexpressions in the context
+def collectPropHasImpInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do
+  collectInstancesFromMainCtx lookupPropHasImp
+
+elab "display_prop_has_imp_instances" : tactic => do
+  trace[Arith] "Displaying the PropHasImp instances"
+  let hs ← collectPropHasImpInstancesFromMainCtx
+  hs.forM fun e => do
+    trace[Arith] "+ PropHasImp instance: {e}"
+
+example (x y : Int) (_ : x ≠ y) (_ : ¬ x = y) : True := by
+  display_prop_has_imp_instances
+  simp
+
+-- Lookup instances in a context and introduce them with additional declarations.
+def introInstances (declToUnfold : Name) (lookup : Expr → MetaM (Option Expr)) : Tactic.TacticM (Array Expr) := do
+  let hs ← collectInstancesFromMainCtx lookup
+  hs.toArray.mapM fun e => do
+    let type ← inferType e
+    let name ← mkFreshUserName `h
+    -- Add a declaration
+    let nval ← Utils.addDeclTac name e type (asLet := false)
+    -- Simplify to unfold the declaration to unfold (i.e., the projector)
+    Utils.simpAt [declToUnfold] [] [] (Tactic.Location.targets #[mkIdent name] false)
+    -- Return the new value
+    pure nval
+
+def introHasIntPropInstances : Tactic.TacticM (Array Expr) := do
+  trace[Arith] "Introducing the HasIntProp instances"
+  introInstances ``HasIntProp.prop_ty lookupHasIntProp
+
+-- Lookup the instances of `HasIntProp for all the sub-expressions in the context,
+-- and introduce the corresponding assumptions
+elab "intro_has_int_prop_instances" : tactic => do
+  let _ ← introHasIntPropInstances
+
+-- Lookup the instances of `PropHasImp for all the sub-expressions in the context,
+-- and introduce the corresponding assumptions
+elab "intro_prop_has_imp_instances" : tactic => do
+  trace[Arith] "Introducing the PropHasImp instances"
+  let _ ← introInstances ``PropHasImp.concl lookupPropHasImp
+
+example (x y : Int) (h0 : x ≤ y) (h1 : x ≠ y) : x < y := by
+  intro_prop_has_imp_instances
+  rename_i h
+  split_disj h
+  . linarith
+  . linarith
+
+/- Boosting a bit the linarith tac.
+
+   We do the following:
+   - for all the assumptions of the shape `(x : Int) ≠ y` or `¬ (x = y), we
+     introduce two goals with the assumptions `x < y` and `x > y`
+     TODO: we could create a PR for mathlib.
+ -/
+def intTacPreprocess (extraPreprocess :  Tactic.TacticM Unit) : Tactic.TacticM Unit := do
+  Tactic.withMainContext do
+  -- Lookup the instances of PropHasImp (this is how we detect assumptions
+  -- of the proper shape), introduce assumptions in the context and split
+  -- on those
+  -- TODO: get rid of the assumptions that we split
+  let rec splitOnAsms (asms : List Expr) : Tactic.TacticM Unit :=
+    match asms with
+    | [] => pure ()
+    | asm :: asms =>
+      let k := splitOnAsms asms
+      Utils.splitDisjTac asm k k
+  -- Introduce the scalar bounds
+  let _ ← introHasIntPropInstances
+  -- Extra preprocessing, before we split on the disjunctions
+  extraPreprocess
+  -- Split
+  let asms ← introInstances ``PropHasImp.concl lookupPropHasImp
+  splitOnAsms asms.toList
+
+elab "int_tac_preprocess" : tactic =>
+  intTacPreprocess (do pure ())
+
+def intTac (extraPreprocess :  Tactic.TacticM Unit) : Tactic.TacticM Unit := do
+  Tactic.withMainContext do
+  Tactic.focus do
+  -- Preprocess - wondering if we should do this before or after splitting
+  -- the goal. I think before leads to a smaller proof term?
+  Tactic.allGoals (intTacPreprocess extraPreprocess)
+  -- Split the conjunctions in the goal
+  Tactic.allGoals (Utils.repeatTac Utils.splitConjTarget)
+  -- Call linarith
+  let linarith :=
+    let cfg : Linarith.LinarithConfig := {
+      -- We do this with our custom preprocessing
+      splitNe := false
+    }
+    Tactic.liftMetaFinishingTactic <| Linarith.linarith false [] cfg
+  Tactic.allGoals linarith
+
+elab "int_tac" : tactic =>
+  intTac (do pure ())
+
+example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by
+  int_tac_preprocess
+  linarith
+  linarith
+
+example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by
+  int_tac
+
+-- Checking that things append correctly when there are several disjunctions
+example (x y : Int) (h0: 0 ≤ x) (h1: x ≠ 0) (h2 : 0 ≤ y) (h3 : y ≠ 0) : 0 < x ∧ 0 < y := by
+  int_tac
+
+-- Checking that things append correctly when there are several disjunctions
+example (x y : Int) (h0: 0 ≤ x) (h1: x ≠ 0) (h2 : 0 ≤ y) (h3 : y ≠ 0) : 0 < x ∧ 0 < y ∧ x + y ≥ 2 := by
+  int_tac
+
+end Arith
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 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')

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 204742bf2449c88abaea8ebd284c55d98b43488a Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 19 Jul 2023 14:48:08 +0200
Subject: Improve progress

---
 backends/lean/Base/Arith/Int.lean | 8 --------
 1 file changed, 8 deletions(-)

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

diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index 5f00ab52..ac011998 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -32,14 +32,6 @@ instance (x y : Int) : PropHasImp (¬ x = y) where
 
 open Lean Lean.Elab Lean.Meta
 
--- Small utility: print all the declarations in the context
-elab "print_all_decls" : tactic => do
-  let ctx ← Lean.MonadLCtx.getLCtx
-  for decl in ← ctx.getDecls do
-    let ty ← Lean.Meta.inferType decl.toExpr
-    logInfo m!"{decl.toExpr} : {ty}"
-  pure ()
-
 -- Explore a term by decomposing the applications (we explore the applied
 -- functions and their arguments, but ignore lambdas, forall, etc. -
 -- should we go inside?).
-- 
cgit v1.2.3


From 03492250b45855fe9db5e0a28a96166607cd84a1 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 20 Jul 2023 14:14:34 +0200
Subject: Make some proofs in Hashmap/Properties.lean and improve progress

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

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

diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index ac011998..fa957293 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -198,7 +198,7 @@ def intTac (extraPreprocess :  Tactic.TacticM Unit) : Tactic.TacticM Unit := do
   -- Split the conjunctions in the goal
   Tactic.allGoals (Utils.repeatTac Utils.splitConjTarget)
   -- Call linarith
-  let linarith :=
+  let linarith := do
     let cfg : Linarith.LinarithConfig := {
       -- We do this with our custom preprocessing
       splitNe := false
-- 
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/Int.lean    | 63 ++++++++++++++++++++++++++++++++----
 backends/lean/Base/Arith/Scalar.lean |  6 ++--
 2 files changed, 59 insertions(+), 10 deletions(-)

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

diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index fa957293..3415866e 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -24,12 +24,29 @@ class PropHasImp (x : Prop) where
   concl : Prop
   prop : x → concl
 
+instance (p : Int → Prop) : HasIntProp (Subtype p) where
+  prop_ty := λ x => p x
+  prop := λ x => x.property
+
 -- This also works for `x ≠ y` because this expression reduces to `¬ x = y`
 -- and `Ne` is marked as `reducible`
 instance (x y : Int) : PropHasImp (¬ x = y) where
   concl := x < y ∨ x > y
   prop := λ (h:x ≠ y) => ne_is_lt_or_gt h
 
+-- Check if a proposition is a linear integer proposition.
+-- We notably use this to check the goals.
+class IsLinearIntProp (x : Prop) where
+
+instance (x y : Int) : IsLinearIntProp (x < y) where
+instance (x y : Int) : IsLinearIntProp (x > y) where
+instance (x y : Int) : IsLinearIntProp (x ≤ y) where
+instance (x y : Int) : IsLinearIntProp (x ≥ y) where
+instance (x y : Int) : IsLinearIntProp (x ≥ y) where
+/- It seems we don't need to do any special preprocessing when the *goal*
+   has the following shape - I guess `linarith` automatically calls `intro` -/
+instance (x y : Int) : IsLinearIntProp (¬ x = y) where
+
 open Lean Lean.Elab Lean.Meta
 
 -- Explore a term by decomposing the applications (we explore the applied
@@ -189,14 +206,27 @@ def intTacPreprocess (extraPreprocess :  Tactic.TacticM Unit) : Tactic.TacticM U
 elab "int_tac_preprocess" : tactic =>
   intTacPreprocess (do pure ())
 
-def intTac (extraPreprocess :  Tactic.TacticM Unit) : Tactic.TacticM Unit := do
+-- Check if the goal is a linear arithmetic goal
+def goalIsLinearInt : Tactic.TacticM Bool := do
+  Tactic.withMainContext do
+  let gty ← Tactic.getMainTarget
+  match ← trySynthInstance (← mkAppM ``IsLinearIntProp #[gty]) with
+  | .some _ => pure true
+  | _ => pure false
+
+def intTac (splitGoalConjs : Bool) (extraPreprocess :  Tactic.TacticM Unit) : Tactic.TacticM Unit := do
   Tactic.withMainContext do
   Tactic.focus do
+  let g ← Tactic.getMainGoal
+  trace[Arith] "Original goal: {g}"
+  -- Introduce all the universally quantified variables (includes the assumptions)
+  let (_, g) ← g.intros
+  Tactic.setGoals [g]
   -- Preprocess - wondering if we should do this before or after splitting
   -- the goal. I think before leads to a smaller proof term?
   Tactic.allGoals (intTacPreprocess extraPreprocess)
   -- Split the conjunctions in the goal
-  Tactic.allGoals (Utils.repeatTac Utils.splitConjTarget)
+  if splitGoalConjs then Tactic.allGoals (Utils.repeatTac Utils.splitConjTarget)
   -- Call linarith
   let linarith := do
     let cfg : Linarith.LinarithConfig := {
@@ -204,10 +234,25 @@ def intTac (extraPreprocess :  Tactic.TacticM Unit) : Tactic.TacticM Unit := do
       splitNe := false
     }
     Tactic.liftMetaFinishingTactic <| Linarith.linarith false [] cfg
-  Tactic.allGoals linarith
-
-elab "int_tac" : tactic =>
-  intTac (do pure ())
+  Tactic.allGoals do
+    -- We check if the goal is a linear arithmetic goal: if yes, we directly
+    -- call linarith, otherwise we first apply exfalso (we do this because
+    -- linarith is too general and sometimes fails to do this correctly).
+    if ← goalIsLinearInt then do
+      trace[Arith] "linarith goal: {← Tactic.getMainGoal}"
+      linarith
+    else do
+      let g ← Tactic.getMainGoal
+      let gs ← g.apply (Expr.const ``False.elim [.zero])
+      let goals ← Tactic.getGoals
+      Tactic.setGoals (gs ++ goals)
+      Tactic.allGoals do
+        trace[Arith] "linarith goal: {← Tactic.getMainGoal}"
+        linarith
+
+elab "int_tac" args:(" split_goal"?): tactic =>
+  let split := args.raw.getArgs.size > 0
+  intTac split (do pure ())
 
 example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by
   int_tac_preprocess
@@ -219,10 +264,14 @@ example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by
 
 -- Checking that things append correctly when there are several disjunctions
 example (x y : Int) (h0: 0 ≤ x) (h1: x ≠ 0) (h2 : 0 ≤ y) (h3 : y ≠ 0) : 0 < x ∧ 0 < y := by
-  int_tac
+  int_tac split_goal
 
 -- Checking that things append correctly when there are several disjunctions
 example (x y : Int) (h0: 0 ≤ x) (h1: x ≠ 0) (h2 : 0 ≤ y) (h3 : y ≠ 0) : 0 < x ∧ 0 < y ∧ x + y ≥ 2 := by
+  int_tac split_goal
+
+-- Checking that we can prove exfalso
+example (a : Prop) (x : Int) (h0: 0 < x) (h1: x < 0) : a := by
   int_tac
 
 end Arith
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/Base.lean   | 4 ++++
 backends/lean/Base/Arith/Int.lean    | 2 ++
 backends/lean/Base/Arith/Scalar.lean | 3 ++-
 3 files changed, 8 insertions(+), 1 deletion(-)

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

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
diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index 3415866e..bc0676d8 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -225,6 +225,8 @@ def intTac (splitGoalConjs : Bool) (extraPreprocess :  Tactic.TacticM Unit) : Ta
   -- Preprocess - wondering if we should do this before or after splitting
   -- the goal. I think before leads to a smaller proof term?
   Tactic.allGoals (intTacPreprocess extraPreprocess)
+  -- More preprocessing
+  Tactic.allGoals (Utils.simpAt [] [``nat_zero_eq_int_zero] [] .wildcard)
   -- Split the conjunctions in the goal
   if splitGoalConjs then Tactic.allGoals (Utils.repeatTac Utils.splitConjTarget)
   -- Call linarith
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 0cc3c78137434d848188eee2a66b1e2cacfd102e Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 25 Jul 2023 19:06:05 +0200
Subject: Make progress on the proofs of the hashmap

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

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

diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index bc0676d8..48a30a49 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -43,6 +43,7 @@ instance (x y : Int) : IsLinearIntProp (x > y) where
 instance (x y : Int) : IsLinearIntProp (x ≤ y) where
 instance (x y : Int) : IsLinearIntProp (x ≥ y) where
 instance (x y : Int) : IsLinearIntProp (x ≥ y) where
+instance (x y : Int) : IsLinearIntProp (x = y) where
 /- It seems we don't need to do any special preprocessing when the *goal*
    has the following shape - I guess `linarith` automatically calls `intro` -/
 instance (x y : Int) : IsLinearIntProp (¬ x = y) where
-- 
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/Int.lean    | 2 +-
 backends/lean/Base/Arith/Scalar.lean | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

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

diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index 48a30a49..7a5bbe98 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -147,7 +147,7 @@ def introInstances (declToUnfold : Name) (lookup : Expr → MetaM (Option Expr))
   let hs ← collectInstancesFromMainCtx lookup
   hs.toArray.mapM fun e => do
     let type ← inferType e
-    let name ← mkFreshUserName `h
+    let name ← mkFreshAnonPropUserName
     -- Add a declaration
     let nval ← Utils.addDeclTac name e type (asLet := false)
     -- Simplify to unfold the declaration to unfold (i.e., the projector)
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