summaryrefslogtreecommitdiff
path: root/backends/lean
diff options
context:
space:
mode:
authorSon Ho2023-07-09 22:27:44 +0200
committerSon Ho2023-07-09 22:27:44 +0200
commitd9a11b312ef0df13795d9a1982ca1cd2eba0e124 (patch)
treece677b31aa230323e907be57f70798ea2d84931e /backends/lean
parent1c251c13b1e6698f3c7c974ea88c2c8a28777cc1 (diff)
Improve int_tac
Diffstat (limited to '')
-rw-r--r--backends/lean/Base/Arith.lean41
1 files changed, 18 insertions, 23 deletions
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