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/Int.lean | 236 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 236 insertions(+)
 create mode 100644 backends/lean/Base/Arith/Int.lean

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

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
-- 
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/Int.lean')

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/Int.lean')

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 ++++++++++++++++++++++++++++++++++-----
 1 file changed, 56 insertions(+), 7 deletions(-)

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

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
-- 
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/Int.lean | 2 ++
 1 file changed, 2 insertions(+)

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

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
-- 
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/Int.lean')

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 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

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