From 3971da603ee54d373b4c73d6a20b3d83dea7b5b9 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 21 Jun 2023 16:20:25 +0200
Subject: Start working on Arith.lean

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

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

diff --git a/backends/lean/Base/Arith.lean b/backends/lean/Base/Arith.lean
new file mode 100644
index 00000000..6339f218
--- /dev/null
+++ b/backends/lean/Base/Arith.lean
@@ -0,0 +1,221 @@
+/- 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
+import Base.Primitives
+
+/-
+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
+
+--set_option pp.explicit true
+--set_option pp.notation false
+--set_option pp.coercions false
+
+-- 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
+
+-- We use this type-class to test if an expression is a scalar (if we manage
+-- to lookup an instance of this type-class, then it is)
+class IsScalar (a : Type) where
+
+instance (ty : ScalarTy) : IsScalar (Scalar ty) where
+
+--example (ty : ScalarTy) : IsScalar (Scalar ty) := _
+
+open Lean Lean.Elab Command Term Lean.Meta
+
+-- Return true if the expression is a scalar expression
+def isScalarExpr (e : Expr) : MetaM Bool := do
+  -- Try to convert the expression to a scalar
+  -- TODO: I tried to do it with Lean.Meta.mkAppM but it didn't work: how
+  -- do we allow Lean to perform (controlled) unfoldings for instantiation
+  -- purposes?
+  let r ← Lean.observing? do
+    let ty ← Lean.Meta.inferType e
+    let isScalar ← mkAppM `Arith.IsScalar #[ty]
+    let isScalar ← trySynthInstance isScalar
+    match isScalar with
+    | LOption.some x => some x
+    | _ => none
+  match r with
+  | .some _ => pure true
+  | _       => pure false
+
+-- Explore a term and return the set of scalar expressions found inside
+partial def collectScalarExprsAux (hs : HashSet Expr) (e : Expr) : MetaM (HashSet Expr) := 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 hs ← if ← isScalarExpr f then pure (hs.insert f) else pure hs
+    let hs ← args.foldlM collectScalarExprsAux hs
+    pure hs
+
+-- Explore a term and return the list of scalar expressions found inside
+def collectScalarExprs (e : Expr) : MetaM (HashSet Expr) :=
+  collectScalarExprsAux HashSet.empty e
+
+-- Collect the scalar expressions in the context
+def getScalarExprsFromMainCtx : 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
+  let hs ← decls.foldlM (fun hs d => collectScalarExprsAux hs d.toExpr) hs
+  -- Return
+  pure hs
+
+
+#check TSyntax
+#check mkIdent
+-- TODO: addDecl?
+-- Project the scalar expressions into the context, to retrieve the bound inequalities
+-- def projectScalarExpr (e: Expr) : Tactic.TacticM Unit := do
+--   let e ← `($e)
+--   let e ← Lean.Elab.Term.elabTerm `($e) none
+--   Lean.Elab.Tactic.evalCases `($e)
+
+elab "list_scalar_exprs" : tactic => do
+  let hs ← getScalarExprsFromMainCtx
+  hs.forM fun e => do
+    dbg_trace f!"+ Scalar expression: {e}"
+
+#check LocalContext
+
+elab "list_local_decls_1" : tactic =>
+  Lean.Elab.Tactic.withMainContext do
+  -- Get the local context
+  let ctx ← Lean.MonadLCtx.getLCtx
+  let ctx ← instantiateLCtxMVars ctx
+  let decls ← ctx.getDecls
+  -- Filter the scalar expressions
+  let decls ← decls.filterMapM fun decl: Lean.LocalDecl => do
+    let declExpr := decl.toExpr
+    let declName := decl.userName
+    let declType ← Lean.Meta.inferType declExpr
+    dbg_trace f!"+ local decl: name: {declName} | expr: {declExpr} | ty: {declType}"
+    -- Try to convert the expression to a scalar
+    -- TODO: I tried to do it with Lean.Meta.mkAppM but it didn't work: how
+    -- do we allow Lean to perform (controlled) unfoldings for instantiation
+    -- purposes?
+    let r ← Lean.observing? do
+      let isScalar ← mkAppM `Arith.IsScalar #[declType]
+      let isScalar ← trySynthInstance isScalar
+      match isScalar with
+      | LOption.some x => some x
+      | _ => none
+    match r with
+    | .some _ => dbg_trace f!"  Scalar expression"; pure r
+    | _       => dbg_trace f!"  Not a scalar"; pure .none
+  pure ()
+    -- match ← Lean.observing? (Lean.Meta.mkAppM `Scalar.toInt #[decl.toExpr]) with
+    -- | .none => dbg_trace f!"  Not a scalar"
+    -- | .some _ => dbg_trace f!"  Scalar expression"
+
+#check Lean.Environment.addDecl  
+#check Expr
+#check LocalContext
+#check MVarId
+#check Lean.Elab.Tactic.setGoals
+#check Lean.Elab.Tactic.Context
+#check withLocalDecl
+#check Lean.MVarId.assert
+#check LocalDecl
+
+-- Insert x = 3 in the context
+elab "custom_let" : tactic =>
+  -- I don't think we need that
+  Lean.Elab.Tactic.withMainContext do
+  --
+  let type := (Expr.const `Nat [])
+  let val : Expr  := .lit (.natVal 3)
+  let n := `x -- the name is "x"
+  withLetDecl n type val fun nval => do
+    -- For debugging
+    let lctx ← Lean.MonadLCtx.getLCtx
+    let fid := nval.fvarId!
+    let decl := lctx.get! fid
+    dbg_trace f!"  nval: \"{decl.userName}\" ({nval}) : {decl.type} := {decl.value}"
+    --
+    -- Tranform the main goal `m0?` to `let x = nval in m1?`
+    let mvarId ← Tactic.getMainGoal
+    let newMVar ← mkFreshExprSyntheticOpaqueMVar (← mvarId.getType)
+    let newVal ← mkLetFVars #[nval] newMVar
+    -- Focus on the current goal
+    Tactic.focus do
+    -- Assign the main goal.
+    -- We must do this *after* we focused on the current goal, because
+    -- after we assigned the meta variable the goal is considered as solved
+    mvarId.assign newVal
+    -- Replace the list of goals with the new goal - we can do this because
+    -- we focused on the current goal
+    Lean.Elab.Tactic.setGoals [newMVar.mvarId!]
+
+example : Nat := by
+  custom_let
+  apply x
+
+example (x : Bool) : Nat := by
+  cases x <;> custom_let <;> apply x
+
+end Arith
-- 
cgit v1.2.3


From 34f1f4d877b32002cd292cb1fe27969184efcf94 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 22 Jun 2023 10:37:13 +0200
Subject: Finish the custom_let tactic

---
 backends/lean/Base/Arith.lean | 44 +++++++++++++++++++++----------------------
 1 file changed, 21 insertions(+), 23 deletions(-)

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

diff --git a/backends/lean/Base/Arith.lean b/backends/lean/Base/Arith.lean
index 6339f218..d4611deb 100644
--- a/backends/lean/Base/Arith.lean
+++ b/backends/lean/Base/Arith.lean
@@ -168,36 +168,27 @@ elab "list_local_decls_1" : tactic =>
     | .some _ => dbg_trace f!"  Scalar expression"; pure r
     | _       => dbg_trace f!"  Not a scalar"; pure .none
   pure ()
-    -- match ← Lean.observing? (Lean.Meta.mkAppM `Scalar.toInt #[decl.toExpr]) with
-    -- | .none => dbg_trace f!"  Not a scalar"
-    -- | .some _ => dbg_trace f!"  Scalar expression"
 
-#check Lean.Environment.addDecl  
-#check Expr
-#check LocalContext
-#check MVarId
-#check Lean.Elab.Tactic.setGoals
-#check Lean.Elab.Tactic.Context
-#check withLocalDecl
-#check Lean.MVarId.assert
-#check LocalDecl
-
--- Insert x = 3 in the context
-elab "custom_let" : tactic =>
+def evalCustomLet (name : Name) (val : Syntax) : Tactic.TacticM Unit :=
   -- I don't think we need that
   Lean.Elab.Tactic.withMainContext do
   --
-  let type := (Expr.const `Nat [])
-  let val : Expr  := .lit (.natVal 3)
-  let n := `x -- the name is "x"
-  withLetDecl n type val fun nval => do
+  let val ← elabTerm val .none
+  let type ← inferType val
+  -- In some situations, the type will be left as a metavariable (for instance,
+  -- if the term is `3`, Lean has the choice between `Nat` and `Int` and will
+  -- not choose): we force the instantiation of the meta-variable
+  synthesizeSyntheticMVarsUsingDefault
+  -- Insert the new declaration
+  withLetDecl name type val fun nval => do
     -- For debugging
     let lctx ← Lean.MonadLCtx.getLCtx
     let fid := nval.fvarId!
     let decl := lctx.get! fid
-    dbg_trace f!"  nval: \"{decl.userName}\" ({nval}) : {decl.type} := {decl.value}"
+        -- Remark: logInfo instantiates the mvars (contrary to dbg_trace):
+    logInfo m!"  new decl: \"{decl.userName}\" ({nval}) : {decl.type} := {decl.value}"
     --
-    -- Tranform the main goal `m0?` to `let x = nval in m1?`
+    -- Tranform the main goal `?m0` to `let x = nval in ?m1`
     let mvarId ← Tactic.getMainGoal
     let newMVar ← mkFreshExprSyntheticOpaqueMVar (← mvarId.getType)
     let newVal ← mkLetFVars #[nval] newMVar
@@ -211,11 +202,18 @@ elab "custom_let" : tactic =>
     -- we focused on the current goal
     Lean.Elab.Tactic.setGoals [newMVar.mvarId!]
 
+elab "custom_let " n:ident " := " v:term : tactic =>
+  evalCustomLet n.getId v
+
+-- Insert x = 3 in the context
+elab "custom_let " n:ident " := " v:term : tactic =>
+  evalCustomLet n.getId v
+
 example : Nat := by
-  custom_let
+  custom_let x := 4
   apply x
 
 example (x : Bool) : Nat := by
-  cases x <;> custom_let <;> apply x
+  cases x <;> custom_let x := 3 <;> apply x
 
 end Arith
-- 
cgit v1.2.3


From 9421b215a8911bc545eb524b8b07e7ca2eb717f3 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 22 Jun 2023 16:02:09 +0200
Subject: Make intro_has_prop_instances work

---
 backends/lean/Base/Arith.lean | 171 +++++++++++++++++++++++++++++++++++-------
 1 file changed, 145 insertions(+), 26 deletions(-)

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

diff --git a/backends/lean/Base/Arith.lean b/backends/lean/Base/Arith.lean
index d4611deb..a792deb2 100644
--- a/backends/lean/Base/Arith.lean
+++ b/backends/lean/Base/Arith.lean
@@ -75,7 +75,28 @@ class IsScalar (a : Type) where
 
 instance (ty : ScalarTy) : IsScalar (Scalar ty) where
 
---example (ty : ScalarTy) : IsScalar (Scalar ty) := _
+example (ty : ScalarTy) : IsScalar (Scalar ty) := inferInstance
+
+-- TODO: lookup doesn't work
+class HasProp {a : Type} (x : a) where
+  prop_ty : Prop
+  prop : prop_ty
+
+class HasProp' (a : Type) where
+  prop_ty : a → Prop
+  prop : ∀ x:a, prop_ty x
+
+instance {ty : ScalarTy} (x : Scalar x) : HasProp x where
+  -- prop_ty is inferred
+  prop := And.intro x.hmin x.hmax
+
+instance (ty : ScalarTy) : HasProp' (Scalar ty) where
+  -- prop_ty is inferred
+  prop := λ x => And.intro x.hmin x.hmax
+
+example {a : Type} (x : a) [HasProp x] : Prop :=
+  let i : HasProp x := inferInstance
+  i.prop_ty
 
 open Lean Lean.Elab Command Term Lean.Meta
 
@@ -96,6 +117,40 @@ def isScalarExpr (e : Expr) : MetaM Bool := do
   | .some _ => pure true
   | _       => pure false
 
+#check @HasProp'.prop
+
+-- Return an instance of `HasProp` for `e` if it has some
+def lookupHasProp (e : Expr) : MetaM (Option Expr) := do
+  logInfo f!"lookupHasProp"
+  -- TODO: do we need Lean.observing?
+  -- This actually eliminates the error messages
+  Lean.observing? do
+    logInfo f!"lookupHasProp: observing"
+    let ty ← Lean.Meta.inferType e
+    let hasProp ← mkAppM `Arith.HasProp' #[ty]
+    let hasPropInst ← trySynthInstance hasProp
+    match hasPropInst with
+    | LOption.some i =>
+      logInfo m!"Found HasProp instance"
+      let i_prop ← mkProjection i `prop
+      some (← mkAppM' i_prop #[e])
+    | _ => none
+
+-- Auxiliary function for `collectHasPropInstances`
+private partial def collectHasPropInstancesAux (hs : HashSet Expr) (e : Expr) : MetaM (HashSet Expr) := 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 hasPropInst ← lookupHasProp f
+    let hs := Option.getD (hasPropInst.map hs.insert) hs
+    let hs ← args.foldlM collectHasPropInstancesAux hs
+    pure hs
+
+-- Explore a term and return the instances of `HasProp` found for the sub-expressions
+def collectHasPropInstances (e : Expr) : MetaM (HashSet Expr) :=
+  collectHasPropInstancesAux HashSet.empty e
+
 -- Explore a term and return the set of scalar expressions found inside
 partial def collectScalarExprsAux (hs : HashSet Expr) (e : Expr) : MetaM (HashSet Expr) := do
   -- We do it in a very simpler manner: we deconstruct applications,
@@ -125,22 +180,43 @@ def getScalarExprsFromMainCtx : Tactic.TacticM (HashSet Expr) := do
   -- Return
   pure hs
 
-
-#check TSyntax
-#check mkIdent
--- TODO: addDecl?
--- Project the scalar expressions into the context, to retrieve the bound inequalities
--- def projectScalarExpr (e: Expr) : Tactic.TacticM Unit := do
---   let e ← `($e)
---   let e ← Lean.Elab.Term.elabTerm `($e) none
---   Lean.Elab.Tactic.evalCases `($e)
+-- Collect the instances of `HasProp` for the subexpressions in the context
+def getHasPropInstancesFromMainCtx : 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
+  let hs ← decls.foldlM (fun hs d => collectHasPropInstancesAux hs d.toExpr) hs
+  -- Return
+  pure hs
 
 elab "list_scalar_exprs" : tactic => do
+  logInfo m!"Listing scalar expressions"
   let hs ← getScalarExprsFromMainCtx
   hs.forM fun e => do
-    dbg_trace f!"+ Scalar expression: {e}"
+    logInfo m!"+ Scalar expression: {e}"
+
+example (x y : U32) (z : Usize) : True := by
+  list_scalar_exprs
+  simp
+
+elab "display_has_prop_instances" : tactic => do
+  logInfo m!"Displaying the HasProp instances"
+  let hs ← getHasPropInstancesFromMainCtx
+  hs.forM fun e => do
+    logInfo m!"+ HasProp instance: {e}"
 
-#check LocalContext
+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
 
 elab "list_local_decls_1" : tactic =>
   Lean.Elab.Tactic.withMainContext do
@@ -169,18 +245,12 @@ elab "list_local_decls_1" : tactic =>
     | _       => dbg_trace f!"  Not a scalar"; pure .none
   pure ()
 
-def evalCustomLet (name : Name) (val : Syntax) : Tactic.TacticM Unit :=
+def evalAddDecl (name : Name) (val : Expr) (type : Expr) (asLet : Bool := false) : Tactic.TacticM Unit :=
   -- I don't think we need that
   Lean.Elab.Tactic.withMainContext do
-  --
-  let val ← elabTerm val .none
-  let type ← inferType val
-  -- In some situations, the type will be left as a metavariable (for instance,
-  -- if the term is `3`, Lean has the choice between `Nat` and `Int` and will
-  -- not choose): we force the instantiation of the meta-variable
-  synthesizeSyntheticMVarsUsingDefault
   -- Insert the new declaration
-  withLetDecl name type val fun nval => do
+  let withDecl := if asLet then withLetDecl name type val else withLocalDeclD name type
+  withDecl fun nval => do
     -- For debugging
     let lctx ← Lean.MonadLCtx.getLCtx
     let fid := nval.fvarId!
@@ -192,6 +262,11 @@ def evalCustomLet (name : Name) (val : Syntax) : Tactic.TacticM Unit :=
     let mvarId ← Tactic.getMainGoal
     let newMVar ← mkFreshExprSyntheticOpaqueMVar (← mvarId.getType)
     let newVal ← mkLetFVars #[nval] newMVar
+    -- There are two cases:
+    -- - asLet is true: newVal is `let $name := $val in $newMVar`
+    -- - asLet is false: ewVal is `λ $name => $newMVar`
+    --   We need to apply it to `val`
+    let newVal := if asLet then newVal else mkAppN newVal #[val]
     -- Focus on the current goal
     Tactic.focus do
     -- Assign the main goal.
@@ -202,18 +277,62 @@ def evalCustomLet (name : Name) (val : Syntax) : Tactic.TacticM Unit :=
     -- we focused on the current goal
     Lean.Elab.Tactic.setGoals [newMVar.mvarId!]
 
-elab "custom_let " n:ident " := " v:term : tactic =>
-  evalCustomLet n.getId v
+def evalAddDeclSyntax (name : Name) (val : Syntax) (asLet : Bool := false) : Tactic.TacticM Unit :=
+  -- I don't think we need that
+  Lean.Elab.Tactic.withMainContext do
+  --
+  let val ← elabTerm val .none
+  let type ← inferType val
+  -- In some situations, the type will be left as a metavariable (for instance,
+  -- if the term is `3`, Lean has the choice between `Nat` and `Int` and will
+  -- not choose): we force the instantiation of the meta-variable
+  synthesizeSyntheticMVarsUsingDefault
+  --
+  evalAddDecl name val type asLet
 
--- Insert x = 3 in the context
 elab "custom_let " n:ident " := " v:term : tactic =>
-  evalCustomLet n.getId v
+  evalAddDeclSyntax n.getId v (asLet := true)
+
+elab "custom_have " n:ident " := " v:term : tactic =>
+  evalAddDeclSyntax n.getId v (asLet := false)
 
 example : Nat := by
   custom_let x := 4
-  apply x
+  custom_have y := 4
+  apply y
 
 example (x : Bool) : Nat := by
   cases x <;> custom_let x := 3 <;> apply x
 
+#check mkIdent
+#check Syntax
+
+-- 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
+  logInfo m!"Introducing the HasProp instances"
+  let hs ← getHasPropInstancesFromMainCtx
+  hs.forM fun e => do
+    let type ← inferType e
+    let name := `h
+    evalAddDecl name e type (asLet := false)
+    -- Simplify to unfold the `prop_ty` projector
+    --let simpTheorems :=  ++ [``HasProp'.prop_ty]
+    let simpTheorems ← Tactic.simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems)
+    -- Add the equational theorem for `HashProp'.prop_ty`
+    let simpTheorems ← simpTheorems.addDeclToUnfold ``HasProp'.prop_ty
+    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
+    pure ()
+    -- simpLocation
+
+example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by
+  intro_has_prop_instances
+  simp [*]
+
+
 end Arith
-- 
cgit v1.2.3


From 6b319ece09b0f8a02529dd98bc20ffcb843020d6 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 26 Jun 2023 17:33:17 +0200
Subject: Make minor modifications to Arith.lean

---
 backends/lean/Base/Arith.lean | 64 +++++++++++++++++++++++++------------------
 1 file changed, 37 insertions(+), 27 deletions(-)

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

diff --git a/backends/lean/Base/Arith.lean b/backends/lean/Base/Arith.lean
index a792deb2..bb776b55 100644
--- a/backends/lean/Base/Arith.lean
+++ b/backends/lean/Base/Arith.lean
@@ -5,6 +5,8 @@ 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
 
 /-
@@ -77,26 +79,19 @@ instance (ty : ScalarTy) : IsScalar (Scalar ty) where
 
 example (ty : ScalarTy) : IsScalar (Scalar ty) := inferInstance
 
--- TODO: lookup doesn't work
-class HasProp {a : Type} (x : a) where
-  prop_ty : Prop
-  prop : prop_ty
-
-class HasProp' (a : Type) where
+-- Remark: I tried a version of the shape `HasProp {a : Type} (x : a)`
+-- but the lookup didn't work
+class HasProp (a : Type) where
   prop_ty : a → Prop
   prop : ∀ x:a, prop_ty x
 
-instance {ty : ScalarTy} (x : Scalar x) : HasProp x where
-  -- prop_ty is inferred
-  prop := And.intro x.hmin x.hmax
-
-instance (ty : ScalarTy) : HasProp' (Scalar ty) where
+instance (ty : ScalarTy) : HasProp (Scalar ty) where
   -- prop_ty is inferred
   prop := λ x => And.intro x.hmin x.hmax
 
-example {a : Type} (x : a) [HasProp x] : Prop :=
-  let i : HasProp x := inferInstance
-  i.prop_ty
+instance (a : Type) : HasProp (Vec a) where
+  prop_ty := λ v => v.val.length ≤ Scalar.max ScalarTy.Usize
+  prop := λ ⟨ _, l ⟩ => l
 
 open Lean Lean.Elab Command Term Lean.Meta
 
@@ -117,8 +112,6 @@ def isScalarExpr (e : Expr) : MetaM Bool := do
   | .some _ => pure true
   | _       => pure false
 
-#check @HasProp'.prop
-
 -- Return an instance of `HasProp` for `e` if it has some
 def lookupHasProp (e : Expr) : MetaM (Option Expr) := do
   logInfo f!"lookupHasProp"
@@ -127,7 +120,7 @@ def lookupHasProp (e : Expr) : MetaM (Option Expr) := do
   Lean.observing? do
     logInfo f!"lookupHasProp: observing"
     let ty ← Lean.Meta.inferType e
-    let hasProp ← mkAppM `Arith.HasProp' #[ty]
+    let hasProp ← mkAppM ``Arith.HasProp #[ty]
     let hasPropInst ← trySynthInstance hasProp
     match hasPropInst with
     | LOption.some i =>
@@ -212,9 +205,9 @@ elab "display_has_prop_instances" : tactic => do
     logInfo m!"+ 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
+  let i : HasProp U32 := inferInstance
+  have p := @HasProp.prop _ i x
+  simp only [HasProp.prop_ty] at p
   display_has_prop_instances
   simp
 
@@ -304,10 +297,7 @@ example : Nat := by
 example (x : Bool) : Nat := by
   cases x <;> custom_let x := 3 <;> apply x
 
-#check mkIdent
-#check Syntax
-
--- Lookup the instances of `HasProp' for all the sub-expressions in the context,
+-- 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
   logInfo m!"Introducing the HasProp instances"
@@ -317,10 +307,9 @@ elab "intro_has_prop_instances" : tactic => do
     let name := `h
     evalAddDecl name e type (asLet := false)
     -- Simplify to unfold the `prop_ty` projector
-    --let simpTheorems :=  ++ [``HasProp'.prop_ty]
     let simpTheorems ← Tactic.simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems)
     -- Add the equational theorem for `HashProp'.prop_ty`
-    let simpTheorems ← simpTheorems.addDeclToUnfold ``HasProp'.prop_ty
+    let simpTheorems ← simpTheorems.addDeclToUnfold ``HasProp.prop_ty
     let congrTheorems ← getSimpCongrTheorems
     let ctx : Simp.Context := { simpTheorems := #[simpTheorems], congrTheorems }
     -- Where to apply the simplifier
@@ -328,11 +317,32 @@ elab "intro_has_prop_instances" : tactic => do
     -- Apply the simplifier
     let _ ← Tactic.simpLocation ctx (discharge? := .none) loc
     pure ()
-    -- simpLocation
 
 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]
+
+-- A tactic to solve linear arithmetic goals
+syntax "int_tac" : tactic
+macro_rules
+  | `(tactic| int_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;
+      simp only [*, Scalar.max, Scalar.min, Scalar.cMin, Scalar.cMax] at *;
+      linarith)
+
+example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by
+  int_tac
+
+example {a: Type} (v : Vec a) : v.val.length ≤ Scalar.max ScalarTy.Usize := by
+  int_tac
 
 end Arith
-- 
cgit v1.2.3


From 0d1ac53f88f947ae94f6afb57b2a7e18a77460a7 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 9 Jul 2023 10:11:13 +0200
Subject: Make progress on the int tactic

---
 backends/lean/Base/Arith.lean | 413 ++++++++++++++++++++++++++----------------
 1 file changed, 257 insertions(+), 156 deletions(-)

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

diff --git a/backends/lean/Base/Arith.lean b/backends/lean/Base/Arith.lean
index bb776b55..df48a6a2 100644
--- a/backends/lean/Base/Arith.lean
+++ b/backends/lean/Base/Arith.lean
@@ -8,6 +8,7 @@ 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.ArithBase
 
 /-
 Mathlib tactics:
@@ -53,9 +54,24 @@ namespace Arith
 
 open Primitives
 
---set_option pp.explicit true
---set_option pp.notation false
---set_option pp.coercions false
+-- 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
@@ -71,17 +87,9 @@ 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
 
--- We use this type-class to test if an expression is a scalar (if we manage
--- to lookup an instance of this type-class, then it is)
-class IsScalar (a : Type) where
-
-instance (ty : ScalarTy) : IsScalar (Scalar ty) where
-
-example (ty : ScalarTy) : IsScalar (Scalar ty) := inferInstance
-
 -- Remark: I tried a version of the shape `HasProp {a : Type} (x : a)`
 -- but the lookup didn't work
-class HasProp (a : Type) where
+class HasProp (a : Sort u) where
   prop_ty : a → Prop
   prop : ∀ x:a, prop_ty x
 
@@ -93,73 +101,50 @@ instance (a : Type) : HasProp (Vec a) where
   prop_ty := λ v => v.val.length ≤ Scalar.max ScalarTy.Usize
   prop := λ ⟨ _, l ⟩ => l
 
-open Lean Lean.Elab Command Term Lean.Meta
-
--- Return true if the expression is a scalar expression
-def isScalarExpr (e : Expr) : MetaM Bool := do
-  -- Try to convert the expression to a scalar
-  -- TODO: I tried to do it with Lean.Meta.mkAppM but it didn't work: how
-  -- do we allow Lean to perform (controlled) unfoldings for instantiation
-  -- purposes?
-  let r ← Lean.observing? do
-    let ty ← Lean.Meta.inferType e
-    let isScalar ← mkAppM `Arith.IsScalar #[ty]
-    let isScalar ← trySynthInstance isScalar
-    match isScalar with
-    | LOption.some x => some x
-    | _ => none
-  match r with
-  | .some _ => pure true
-  | _       => pure false
+class PropHasImp (x : Prop) where
+  concl : Prop
+  prop : x → concl
 
--- Return an instance of `HasProp` for `e` if it has some
-def lookupHasProp (e : Expr) : MetaM (Option Expr) := do
-  logInfo f!"lookupHasProp"
-  -- TODO: do we need Lean.observing?
-  -- This actually eliminates the error messages
-  Lean.observing? do
-    logInfo f!"lookupHasProp: observing"
-    let ty ← Lean.Meta.inferType e
-    let hasProp ← mkAppM ``Arith.HasProp #[ty]
-    let hasPropInst ← trySynthInstance hasProp
-    match hasPropInst with
-    | LOption.some i =>
-      logInfo m!"Found HasProp instance"
-      let i_prop ← mkProjection i `prop
-      some (← mkAppM' i_prop #[e])
-    | _ => none
+-- 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
 
--- Auxiliary function for `collectHasPropInstances`
-private partial def collectHasPropInstancesAux (hs : HashSet Expr) (e : Expr) : MetaM (HashSet Expr) := 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 hasPropInst ← lookupHasProp f
-    let hs := Option.getD (hasPropInst.map hs.insert) hs
-    let hs ← args.foldlM collectHasPropInstancesAux hs
-    pure hs
+open Lean Lean.Elab Command Term Lean.Meta
 
--- Explore a term and return the instances of `HasProp` found for the sub-expressions
-def collectHasPropInstances (e : Expr) : MetaM (HashSet Expr) :=
-  collectHasPropInstancesAux HashSet.empty e
+-- 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 and return the set of scalar expressions found inside
-partial def collectScalarExprsAux (hs : HashSet Expr) (e : Expr) : MetaM (HashSet Expr) := do
+-- 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 hs ← if ← isScalarExpr f then pure (hs.insert f) else pure hs
-    let hs ← args.foldlM collectScalarExprsAux hs
-    pure hs
-
--- Explore a term and return the list of scalar expressions found inside
-def collectScalarExprs (e : Expr) : MetaM (HashSet Expr) :=
-  collectScalarExprsAux HashSet.empty e
-
--- Collect the scalar expressions in the context
-def getScalarExprsFromMainCtx : Tactic.TacticM (HashSet Expr) := 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
@@ -169,40 +154,37 @@ def getScalarExprsFromMainCtx : Tactic.TacticM (HashSet Expr) := do
   let hs := HashSet.empty
   -- Explore the declarations
   let decls ← ctx.getDecls
-  let hs ← decls.foldlM (fun hs d => collectScalarExprsAux hs d.toExpr) hs
-  -- Return
-  pure hs
+  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 getHasPropInstancesFromMainCtx : 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
-  let hs ← decls.foldlM (fun hs d => collectHasPropInstancesAux hs d.toExpr) hs
-  -- Return
-  pure hs
+def collectHasPropInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do
+  collectInstancesFromMainCtx lookupHasProp
 
-elab "list_scalar_exprs" : tactic => do
-  logInfo m!"Listing scalar expressions"
-  let hs ← getScalarExprsFromMainCtx
+elab "display_has_prop_instances" : tactic => do
+  trace[Arith] "Displaying the HasProp instances"
+  let hs ← collectHasPropInstancesFromMainCtx
   hs.forM fun e => do
-    logInfo m!"+ Scalar expression: {e}"
+    trace[Arith] "+ HasProp instance: {e}"
 
-example (x y : U32) (z : Usize) : True := by
-  list_scalar_exprs
-  simp
 
-elab "display_has_prop_instances" : tactic => do
-  logInfo m!"Displaying the HasProp instances"
-  let hs ← getHasPropInstancesFromMainCtx
-  hs.forM fun e => do
-    logInfo m!"+ HasProp instance: {e}"
+set_option trace.Arith true
 
 example (x : U32) : True := by
   let i : HasProp U32 := inferInstance
@@ -211,34 +193,45 @@ example (x : U32) : True := by
   display_has_prop_instances
   simp
 
-elab "list_local_decls_1" : tactic =>
-  Lean.Elab.Tactic.withMainContext do
-  -- Get the local context
-  let ctx ← Lean.MonadLCtx.getLCtx
-  let ctx ← instantiateLCtxMVars ctx
-  let decls ← ctx.getDecls
-  -- Filter the scalar expressions
-  let decls ← decls.filterMapM fun decl: Lean.LocalDecl => do
-    let declExpr := decl.toExpr
-    let declName := decl.userName
-    let declType ← Lean.Meta.inferType declExpr
-    dbg_trace f!"+ local decl: name: {declName} | expr: {declExpr} | ty: {declType}"
-    -- Try to convert the expression to a scalar
-    -- TODO: I tried to do it with Lean.Meta.mkAppM but it didn't work: how
-    -- do we allow Lean to perform (controlled) unfoldings for instantiation
-    -- purposes?
-    let r ← Lean.observing? do
-      let isScalar ← mkAppM `Arith.IsScalar #[declType]
-      let isScalar ← trySynthInstance isScalar
-      match isScalar with
-      | LOption.some x => some x
-      | _ => none
-    match r with
-    | .some _ => dbg_trace f!"  Scalar expression"; pure r
-    | _       => dbg_trace f!"  Not a scalar"; pure .none
-  pure ()
+set_option trace.Arith false
 
-def evalAddDecl (name : Name) (val : Expr) (type : Expr) (asLet : Bool := false) : Tactic.TacticM Unit :=
+-- 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}"
+
+set_option trace.Arith true
+
+example (x y : Int) (h0 : x ≠ y) (h1 : ¬ x = y) : True := by
+  display_prop_has_imp_instances
+  simp
+
+set_option trace.Arith false
+
+def addDecl (name : Name) (val : Expr) (type : Expr) (asLet : Bool) (k : Expr → Tactic.TacticM Unit) : Tactic.TacticM Unit :=
   -- I don't think we need that
   Lean.Elab.Tactic.withMainContext do
   -- Insert the new declaration
@@ -248,8 +241,7 @@ def evalAddDecl (name : Name) (val : Expr) (type : Expr) (asLet : Bool := false)
     let lctx ← Lean.MonadLCtx.getLCtx
     let fid := nval.fvarId!
     let decl := lctx.get! fid
-        -- Remark: logInfo instantiates the mvars (contrary to dbg_trace):
-    logInfo m!"  new decl: \"{decl.userName}\" ({nval}) : {decl.type} := {decl.value}"
+    trace[Arith] "  new decl: \"{decl.userName}\" ({nval}) : {decl.type} := {decl.value}"
     --
     -- Tranform the main goal `?m0` to `let x = nval in ?m1`
     let mvarId ← Tactic.getMainGoal
@@ -260,17 +252,14 @@ def evalAddDecl (name : Name) (val : Expr) (type : Expr) (asLet : Bool := false)
     -- - asLet is false: ewVal is `λ $name => $newMVar`
     --   We need to apply it to `val`
     let newVal := if asLet then newVal else mkAppN newVal #[val]
-    -- Focus on the current goal
-    Tactic.focus do
-    -- Assign the main goal.
-    -- We must do this *after* we focused on the current goal, because
-    -- after we assigned the meta variable the goal is considered as solved
+    -- Assign the main goal and update the current goal
     mvarId.assign newVal
-    -- Replace the list of goals with the new goal - we can do this because
-    -- we focused on the current goal
-    Lean.Elab.Tactic.setGoals [newMVar.mvarId!]
+    let goals ← Tactic.getUnsolvedGoals
+    Lean.Elab.Tactic.setGoals (newMVar.mvarId! :: goals)
+    -- Call the continuation
+    k nval
 
-def evalAddDeclSyntax (name : Name) (val : Syntax) (asLet : Bool := false) : Tactic.TacticM Unit :=
+def addDeclSyntax (name : Name) (val : Syntax) (asLet : Bool) (k : Expr → Tactic.TacticM Unit) : Tactic.TacticM Unit :=
   -- I don't think we need that
   Lean.Elab.Tactic.withMainContext do
   --
@@ -281,13 +270,13 @@ def evalAddDeclSyntax (name : Name) (val : Syntax) (asLet : Bool := false) : Tac
   -- not choose): we force the instantiation of the meta-variable
   synthesizeSyntheticMVarsUsingDefault
   --
-  evalAddDecl name val type asLet
+  addDecl name val type asLet k
 
 elab "custom_let " n:ident " := " v:term : tactic =>
-  evalAddDeclSyntax n.getId v (asLet := true)
+  addDeclSyntax n.getId v (asLet := true) (λ _ => pure ())
 
 elab "custom_have " n:ident " := " v:term : tactic =>
-  evalAddDeclSyntax n.getId v (asLet := false)
+  addDeclSyntax n.getId v (asLet := false) (λ _ => pure ())
 
 example : Nat := by
   custom_let x := 4
@@ -297,26 +286,32 @@ example : Nat := by
 example (x : Bool) : Nat := by
   cases x <;> custom_let x := 3 <;> apply x
 
--- 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
-  logInfo m!"Introducing the HasProp instances"
-  let hs ← getHasPropInstancesFromMainCtx
+-- Lookup instances in a context and introduce them with additional declarations.
+def introInstances (declToUnfold : Name) (lookup : Expr → MetaM (Option Expr)) (k : Expr → Tactic.TacticM Unit) : Tactic.TacticM Unit := do
+  let hs ← collectInstancesFromMainCtx lookup
   hs.forM fun e => do
     let type ← inferType e
-    let name := `h
-    evalAddDecl name e type (asLet := false)
-    -- Simplify to unfold the `prop_ty` projector
+    let name ← mkFreshUserName `h
+    -- Add a declaration
+    addDecl name e type (asLet := false) λ nval => do
+    -- Simplify to unfold the declaration to unfold (i.e., the projector)
     let simpTheorems ← Tactic.simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems)
-    -- Add the equational theorem for `HashProp'.prop_ty`
-    let simpTheorems ← simpTheorems.addDeclToUnfold ``HasProp.prop_ty
+    -- 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
-    pure ()
+    -- Call the continuation
+    k 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"
+  introInstances ``HasProp.prop_ty lookupHasProp (fun _ => pure ())
 
 example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by
   intro_has_prop_instances
@@ -326,23 +321,129 @@ example {a: Type} (v : Vec a) : v.val.length ≤ Scalar.max ScalarTy.Usize := by
   intro_has_prop_instances
   simp_all [Scalar.max, Scalar.min]
 
--- A tactic to solve linear arithmetic goals
-syntax "int_tac" : tactic
+-- Tactic to split on a disjunction
+def splitDisj (h : Expr) : 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
+  -- 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`)
+    let asmName ← mkFreshUserName `h
+    withLocalDeclD asmName hTy fun var => do
+    -- The new goal
+    let mgoal ← mkFreshExprSyntheticOpaqueMVar goalType (tag := Name.mkSimple nGoalName)
+    -- The branch expression
+    let branch ← mkLambdaFVars #[var] mgoal
+    pure (branch, mgoal.mvarId!)
+  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
+  Tactic.setGoals (mleft :: mright :: 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
+
+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"
+  introInstances ``PropHasImp.concl lookupPropHasImp (fun _ => pure ())
+
+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
+
+syntax "int_tac_preprocess" : tactic
+
+/- 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
+  -- Get the local context
+  let ctx ← Lean.MonadLCtx.getLCtx
+  -- Just a matter of precaution
+  let ctx ← instantiateLCtxMVars ctx
+  -- Explore the declarations - Remark: we don't explore the subexpressions
+  -- (we could, but it is rarely necessary, because terms of the shape `x ≠ y`
+  -- are often introduced because of branchings in the code, and using `split`
+  -- introduces exactly the assumptions `x = y` and `x ≠ y`).
+  let decls ← ctx.getDecls
+  for decl in decls do
+    let ty ← Lean.Meta.inferType decl.toExpr
+    ty.withApp fun f args => do
+      trace[Arith] "decl: {f} {args}"
+      -- Check if this is an inequality between integers
+  pure ()
+
+-- TODO: int_tac
+
+elab "int_tac_preprocess" : tactic =>
+  intTacPreprocess
+
+example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by
+  int_tac_preprocess
+  simp_all
+  int_tac_preprocess
+
+-- A tactic to solve linear arithmetic goals in the presence of scalars
+syntax "scalar_tac" : tactic
 macro_rules
-  | `(tactic| int_tac) =>
+  | `(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 *;
+      -- TODO: use int_tac
       linarith)
 
 example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by
-  int_tac
+  scalar_tac
 
 example {a: Type} (v : Vec a) : v.val.length ≤ Scalar.max ScalarTy.Usize := by
-  int_tac
+  scalar_tac
 
 end Arith
-- 
cgit v1.2.3


From 1c251c13b1e6698f3c7c974ea88c2c8a28777cc1 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 9 Jul 2023 10:50:50 +0200
Subject: Implement a first working version of int_tac

---
 backends/lean/Base/Arith.lean | 96 ++++++++++++++++++++++++++-----------------
 1 file changed, 58 insertions(+), 38 deletions(-)

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

diff --git a/backends/lean/Base/Arith.lean b/backends/lean/Base/Arith.lean
index df48a6a2..8cdf75a3 100644
--- a/backends/lean/Base/Arith.lean
+++ b/backends/lean/Base/Arith.lean
@@ -231,7 +231,7 @@ example (x y : Int) (h0 : x ≠ y) (h1 : ¬ x = y) : True := by
 
 set_option trace.Arith false
 
-def addDecl (name : Name) (val : Expr) (type : Expr) (asLet : Bool) (k : Expr → Tactic.TacticM Unit) : Tactic.TacticM Unit :=
+def addDecl (name : Name) (val : Expr) (type : Expr) (asLet : Bool) : Tactic.TacticM Expr :=
   -- I don't think we need that
   Lean.Elab.Tactic.withMainContext do
   -- Insert the new declaration
@@ -256,10 +256,11 @@ def addDecl (name : Name) (val : Expr) (type : Expr) (asLet : Bool) (k : Expr 
     mvarId.assign newVal
     let goals ← Tactic.getUnsolvedGoals
     Lean.Elab.Tactic.setGoals (newMVar.mvarId! :: goals)
-    -- Call the continuation
-    k nval
+    -- Return the new value - note: we are in the *new* context, created
+    -- after the declaration was added, so it will persist
+    pure nval
 
-def addDeclSyntax (name : Name) (val : Syntax) (asLet : Bool) (k : Expr → Tactic.TacticM Unit) : Tactic.TacticM Unit :=
+def addDeclSyntax (name : Name) (val : Syntax) (asLet : Bool) : Tactic.TacticM Unit :=
   -- I don't think we need that
   Lean.Elab.Tactic.withMainContext do
   --
@@ -270,13 +271,13 @@ def addDeclSyntax (name : Name) (val : Syntax) (asLet : Bool) (k : Expr → Tact
   -- not choose): we force the instantiation of the meta-variable
   synthesizeSyntheticMVarsUsingDefault
   --
-  addDecl name val type asLet k
+  let _ ← addDecl name val type asLet
 
-elab "custom_let " n:ident " := " v:term : tactic =>
-  addDeclSyntax n.getId v (asLet := true) (λ _ => pure ())
+elab "custom_let " n:ident " := " v:term : tactic => do
+  addDeclSyntax n.getId v (asLet := true)
 
 elab "custom_have " n:ident " := " v:term : tactic =>
-  addDeclSyntax n.getId v (asLet := false) (λ _ => pure ())
+  addDeclSyntax n.getId v (asLet := false)
 
 example : Nat := by
   custom_let x := 4
@@ -287,13 +288,13 @@ example (x : Bool) : Nat := by
   cases x <;> custom_let x := 3 <;> apply x
 
 -- Lookup instances in a context and introduce them with additional declarations.
-def introInstances (declToUnfold : Name) (lookup : Expr → MetaM (Option Expr)) (k : Expr → Tactic.TacticM Unit) : Tactic.TacticM Unit := do
+def introInstances (declToUnfold : Name) (lookup : Expr → MetaM (Option Expr)) : Tactic.TacticM (Array Expr) := do
   let hs ← collectInstancesFromMainCtx lookup
-  hs.forM fun e => do
+  hs.toArray.mapM fun e => do
     let type ← inferType e
     let name ← mkFreshUserName `h
     -- Add a declaration
-    addDecl name e type (asLet := false) λ nval => do
+    let nval ← 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
@@ -304,14 +305,14 @@ def introInstances (declToUnfold : Name) (lookup : Expr → MetaM (Option Expr))
     let loc := Tactic.Location.targets #[mkIdent name] false
     -- Apply the simplifier
     let _ ← Tactic.simpLocation ctx (discharge? := .none) loc
-    -- Call the continuation
-    k nval
+    -- 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"
-  introInstances ``HasProp.prop_ty lookupHasProp (fun _ => pure ())
+  let _ ← introInstances ``HasProp.prop_ty lookupHasProp
 
 example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by
   intro_has_prop_instances
@@ -322,7 +323,7 @@ example {a: Type} (v : Vec a) : v.val.length ≤ Scalar.max ScalarTy.Usize := by
   simp_all [Scalar.max, Scalar.min]
 
 -- Tactic to split on a disjunction
-def splitDisj (h : Expr) : Tactic.TacticM Unit := do
+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
@@ -361,14 +362,23 @@ def splitDisj (h : Expr) : Tactic.TacticM Unit := do
   trace[Arith] "main goal: {mgoal}"
   mgoal.assign casesExpr
   let goals ← Tactic.getUnsolvedGoals
-  Tactic.setGoals (mleft :: mright :: goals)
+  -- 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
+  splitDisj fvar (fun _ => pure ()) (fun _ => pure ())
 
 example (x y : Int) (h0 : x ≤ y ∨ x ≥ y) : x ≤ y ∨ x ≥ y := by
   split_disj h0
@@ -379,7 +389,7 @@ example (x y : Int) (h0 : x ≤ y ∨ x ≥ y) : x ≤ y ∨ x ≥ y := by
 -- and introduce the corresponding assumptions
 elab "intro_prop_has_imp_instances" : tactic => do
   trace[Arith] "Introducing the PropHasImp instances"
-  introInstances ``PropHasImp.concl lookupPropHasImp (fun _ => pure ())
+  let _ ← introInstances ``PropHasImp.concl lookupPropHasImp
 
 example (x y : Int) (h0 : x ≤ y) (h1 : x ≠ y) : x < y := by
   intro_prop_has_imp_instances
@@ -388,7 +398,7 @@ example (x y : Int) (h0 : x ≤ y) (h1 : x ≠ y) : x < y := by
   . linarith
   . linarith
 
-syntax "int_tac_preprocess" : tactic
+--syntax "int_tac_preprocess" : tactic
 
 /- Boosting a bit the linarith tac.
 
@@ -399,31 +409,41 @@ syntax "int_tac_preprocess" : tactic
  -/
 def intTacPreprocess : Tactic.TacticM Unit := do
   Lean.Elab.Tactic.withMainContext do
-  -- Get the local context
-  let ctx ← Lean.MonadLCtx.getLCtx
-  -- Just a matter of precaution
-  let ctx ← instantiateLCtxMVars ctx
-  -- Explore the declarations - Remark: we don't explore the subexpressions
-  -- (we could, but it is rarely necessary, because terms of the shape `x ≠ y`
-  -- are often introduced because of branchings in the code, and using `split`
-  -- introduces exactly the assumptions `x = y` and `x ≠ y`).
-  let decls ← ctx.getDecls
-  for decl in decls do
-    let ty ← Lean.Meta.inferType decl.toExpr
-    ty.withApp fun f args => do
-      trace[Arith] "decl: {f} {args}"
-      -- Check if this is an inequality between integers
-  pure ()
-
--- TODO: int_tac
+  -- 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 assumption 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
-  simp_all
-  int_tac_preprocess
+  linarith
+  linarith
+
+syntax "int_tac" : tactic
+macro_rules
+  | `(tactic| int_tac) =>
+    `(tactic|
+      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_preprocess <;> apply And.intro <;> linarith
 
 -- A tactic to solve linear arithmetic goals in the presence of scalars
 syntax "scalar_tac" : tactic
-- 
cgit v1.2.3


From d9a11b312ef0df13795d9a1982ca1cd2eba0e124 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 9 Jul 2023 22:27:44 +0200
Subject: Improve int_tac

---
 backends/lean/Base/Arith.lean | 41 ++++++++++++++++++-----------------------
 1 file changed, 18 insertions(+), 23 deletions(-)

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

diff --git a/backends/lean/Base/Arith.lean b/backends/lean/Base/Arith.lean
index 8cdf75a3..364447ed 100644
--- a/backends/lean/Base/Arith.lean
+++ b/backends/lean/Base/Arith.lean
@@ -183,9 +183,6 @@ elab "display_has_prop_instances" : tactic => do
   hs.forM fun e => do
     trace[Arith] "+ HasProp instance: {e}"
 
-
-set_option trace.Arith true
-
 example (x : U32) : True := by
   let i : HasProp U32 := inferInstance
   have p := @HasProp.prop _ i x
@@ -193,8 +190,6 @@ example (x : U32) : True := by
   display_has_prop_instances
   simp
 
-set_option trace.Arith false
-
 -- Return an instance of `PropHasImp` for `e` if it has some
 def lookupPropHasImp (e : Expr) : MetaM (Option Expr) := do
   trace[Arith] "lookupPropHasImp"
@@ -223,14 +218,10 @@ elab "display_prop_has_imp_instances" : tactic => do
   hs.forM fun e => do
     trace[Arith] "+ PropHasImp instance: {e}"
 
-set_option trace.Arith true
-
-example (x y : Int) (h0 : x ≠ y) (h1 : ¬ x = y) : True := by
+example (x y : Int) (_ : x ≠ y) (_ : ¬ x = y) : True := by
   display_prop_has_imp_instances
   simp
 
-set_option trace.Arith false
-
 def addDecl (name : Name) (val : Expr) (type : Expr) (asLet : Bool) : Tactic.TacticM Expr :=
   -- I don't think we need that
   Lean.Elab.Tactic.withMainContext do
@@ -322,12 +313,15 @@ 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
+-- 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
@@ -341,14 +335,16 @@ def splitDisj (h : Expr) (kleft kright : Tactic.TacticM Unit) : Tactic.TacticM U
   -- - 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`)
-    let asmName ← mkFreshUserName `h
-    withLocalDeclD asmName hTy fun var => 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] mgoal
-    pure (branch, mgoal.mvarId!)
+    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}"
@@ -398,8 +394,6 @@ example (x y : Int) (h0 : x ≤ y) (h1 : x ≠ y) : x < y := by
   . linarith
   . linarith
 
---syntax "int_tac_preprocess" : tactic
-
 /- Boosting a bit the linarith tac.
 
    We do the following:
@@ -412,7 +406,7 @@ def intTacPreprocess : Tactic.TacticM Unit := 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 assumption that we split
+  -- TODO: get rid of the assumptions that we split
   let rec splitOnAsms (asms : List Expr) : Tactic.TacticM Unit :=
     match asms with
     | [] => pure ()
@@ -436,14 +430,16 @@ 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
+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_preprocess <;> apply And.intro <;> linarith
+  int_tac
 
 -- A tactic to solve linear arithmetic goals in the presence of scalars
 syntax "scalar_tac" : tactic
@@ -457,8 +453,7 @@ macro_rules
       have := Scalar.cMax_bound ScalarTy.Isize;
       -- TODO: not too sure about that
       simp only [*, Scalar.max, Scalar.min, Scalar.cMin, Scalar.cMax] at *;
-      -- TODO: use int_tac
-      linarith)
+      int_tac)
 
 example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by
   scalar_tac
-- 
cgit v1.2.3


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.lean | 464 ------------------------------------------
 1 file changed, 464 deletions(-)
 delete mode 100644 backends/lean/Base/Arith.lean

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

diff --git a/backends/lean/Base/Arith.lean b/backends/lean/Base/Arith.lean
deleted file mode 100644
index 364447ed..00000000
--- a/backends/lean/Base/Arith.lean
+++ /dev/null
@@ -1,464 +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.ArithBase
-
-/-
-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
-
-def addDecl (name : Name) (val : Expr) (type : Expr) (asLet : Bool) : Tactic.TacticM Expr :=
-  -- I don't think we need that
-  Lean.Elab.Tactic.withMainContext do
-  -- Insert the new declaration
-  let withDecl := if asLet then withLetDecl name type val else withLocalDeclD name type
-  withDecl fun nval => do
-    -- For debugging
-    let lctx ← Lean.MonadLCtx.getLCtx
-    let fid := nval.fvarId!
-    let decl := lctx.get! fid
-    trace[Arith] "  new decl: \"{decl.userName}\" ({nval}) : {decl.type} := {decl.value}"
-    --
-    -- Tranform the main goal `?m0` to `let x = nval in ?m1`
-    let mvarId ← Tactic.getMainGoal
-    let newMVar ← mkFreshExprSyntheticOpaqueMVar (← mvarId.getType)
-    let newVal ← mkLetFVars #[nval] newMVar
-    -- There are two cases:
-    -- - asLet is true: newVal is `let $name := $val in $newMVar`
-    -- - asLet is false: ewVal is `λ $name => $newMVar`
-    --   We need to apply it to `val`
-    let newVal := if asLet then newVal else mkAppN newVal #[val]
-    -- Assign the main goal and update the current goal
-    mvarId.assign newVal
-    let goals ← Tactic.getUnsolvedGoals
-    Lean.Elab.Tactic.setGoals (newMVar.mvarId! :: goals)
-    -- Return the new value - note: we are in the *new* context, created
-    -- after the declaration was added, so it will persist
-    pure nval
-
-def addDeclSyntax (name : Name) (val : Syntax) (asLet : Bool) : Tactic.TacticM Unit :=
-  -- I don't think we need that
-  Lean.Elab.Tactic.withMainContext do
-  --
-  let val ← elabTerm val .none
-  let type ← inferType val
-  -- In some situations, the type will be left as a metavariable (for instance,
-  -- if the term is `3`, Lean has the choice between `Nat` and `Int` and will
-  -- not choose): we force the instantiation of the meta-variable
-  synthesizeSyntheticMVarsUsingDefault
-  --
-  let _ ← addDecl name val type asLet
-
-elab "custom_let " n:ident " := " v:term : tactic => do
-  addDeclSyntax n.getId v (asLet := true)
-
-elab "custom_have " n:ident " := " v:term : tactic =>
-  addDeclSyntax n.getId v (asLet := false)
-
-example : Nat := by
-  custom_let x := 4
-  custom_have y := 4
-  apply y
-
-example (x : Bool) : Nat := by
-  cases x <;> custom_let x := 3 <;> apply x
-
--- 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 ← 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
-- 
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.lean | 1 +
 1 file changed, 1 insertion(+)
 create mode 100644 backends/lean/Base/Arith.lean

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

diff --git a/backends/lean/Base/Arith.lean b/backends/lean/Base/Arith.lean
new file mode 100644
index 00000000..fd5698c5
--- /dev/null
+++ b/backends/lean/Base/Arith.lean
@@ -0,0 +1 @@
+import Base.Arith.Arith
-- 
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.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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

diff --git a/backends/lean/Base/Arith.lean b/backends/lean/Base/Arith.lean
index fd5698c5..c0d09fd2 100644
--- a/backends/lean/Base/Arith.lean
+++ b/backends/lean/Base/Arith.lean
@@ -1 +1,2 @@
-import Base.Arith.Arith
+import Base.Arith.Int
+import Base.Arith.Scalar
-- 
cgit v1.2.3