summaryrefslogtreecommitdiff
path: root/backends
diff options
context:
space:
mode:
authorSon HO2024-06-17 23:29:51 +0200
committerGitHub2024-06-17 23:29:51 +0200
commit76ab141814644a94bffc8497e5845436d86b1083 (patch)
tree664f9b51b9dac1abbf34bca8add6c88fbe7bcec9 /backends
parent95e3219b7814dd454dd82dd0b7f607af9ac02826 (diff)
parent359410257a4b803dd972a248b46ede377b1bed15 (diff)
Merge pull request #240 from RaitoBezarius/has-int-pred
backends/lean: introduce `HasIntPred` automation
Diffstat (limited to 'backends')
-rw-r--r--backends/lean/Base/Arith/Int.lean42
-rw-r--r--backends/lean/Base/IList/IList.lean8
2 files changed, 41 insertions, 9 deletions
diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index 1d3e82be..068d6f2f 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -21,6 +21,11 @@ class HasIntProp (a : Sort u) where
prop_ty : a → Prop
prop : ∀ x:a, prop_ty x
+/- Terms that induces predicates: if we can find the term `x`, we can introduce `concl` in the context. -/
+class HasIntPred {a: Sort u} (x: a) where
+ concl : Prop
+ prop : concl
+
/- Proposition with implications: if we find P we can introduce Q in the context -/
class PropHasImp (x : Sort u) where
concl : Prop
@@ -106,36 +111,52 @@ def collectInstancesFromMainCtx (k : Expr → MetaM (Option Expr)) : Tactic.Tact
let hs := HashSet.empty
-- Explore the declarations
let decls ← ctx.getDecls
- let hs ← decls.foldlM (fun hs d => collectInstances k hs d.toExpr) hs
+ let hs ← decls.foldlM (fun hs d => do
+ -- Collect instances over all subexpressions in the context.
+ -- Note that we explore the *type* of the local declarations: if we have
+ -- for instance `h : A ∧ B` in the context, the expression itself is simply
+ -- `h`; the information we are interested in is its type.
+ let ty ← Lean.Meta.inferType d.toExpr
+ collectInstances k hs ty
+ ) hs
-- Also explore the goal
collectInstances k hs (← Tactic.getMainTarget)
-- Helper
-def lookupProp (fName : String) (className : Name) (e : Expr) : MetaM (Option Expr) := do
+def lookupProp (fName : String) (className : Name) (e : Expr)
+ (instantiateClassFn : Expr → MetaM (Array Expr))
+ (instantiateProjectionFn : Expr → MetaM (Array Expr)) : MetaM (Option Expr) := do
trace[Arith] fName
-- TODO: do we need Lean.observing?
-- This actually eliminates the error messages
trace[Arith] m!"{fName}: {e}"
Lean.observing? do
trace[Arith] m!"{fName}: observing: {e}"
- let ty ← Lean.Meta.inferType e
- let hasProp ← mkAppM className #[ty]
+ let hasProp ← mkAppM className (← instantiateClassFn e)
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])
+ some (← mkAppM' i_prop (← instantiateProjectionFn e))
| _ => none
-- Return an instance of `HasIntProp` for `e` if it has some
def lookupHasIntProp (e : Expr) : MetaM (Option Expr) :=
- lookupProp "lookupHasIntProp" ``HasIntProp e
+ lookupProp "lookupHasIntProp" ``HasIntProp e (fun e => do pure #[← Lean.Meta.inferType e]) (fun e => pure #[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 `HasIntPred` for `e` if it has some
+def lookupHasIntPred (e : Expr) : MetaM (Option Expr) :=
+ lookupProp "lookupHasIntPred" ``HasIntPred e (fun term => pure #[term]) (fun _ => pure #[])
+
+-- Collect the instances of `HasIntPred` for the subexpressions in the context
+def collectHasIntPredInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do
+ collectInstancesFromMainCtx lookupHasIntPred
+
-- Return an instance of `PropHasImp` for `e` if it has some
def lookupPropHasImp (e : Expr) : MetaM (Option Expr) := do
trace[Arith] m!"lookupPropHasImp: {e}"
@@ -193,6 +214,13 @@ def introHasIntPropInstances : Tactic.TacticM (Array Expr) := do
elab "intro_has_int_prop_instances" : tactic => do
let _ ← introHasIntPropInstances
+def introHasIntPredInstances : Tactic.TacticM (Array Expr) := do
+ trace[Arith] "Introducing the HasIntPred instances"
+ introInstances ``HasIntPred.concl lookupHasIntPred
+
+elab "intro_has_int_pred_instances" : tactic => do
+ let _ ← introHasIntPredInstances
+
def introPropHasImpInstances : Tactic.TacticM (Array Expr) := do
trace[Arith] "Introducing the PropHasImp instances"
introInstances ``PropHasImp.concl lookupPropHasImp
@@ -208,6 +236,8 @@ def intTacPreprocess (extraPreprocess : Tactic.TacticM Unit) : Tactic.TacticM U
Tactic.withMainContext do
-- Introduce the instances of `HasIntProp`
let _ ← introHasIntPropInstances
+ -- Introduce the instances of `HasIntPred`
+ let _ ← introHasIntPredInstances
-- Introduce the instances of `PropHasImp`
let _ ← introPropHasImpInstances
-- Extra preprocessing
diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean
index a1897191..96843f55 100644
--- a/backends/lean/Base/IList/IList.lean
+++ b/backends/lean/Base/IList/IList.lean
@@ -18,9 +18,11 @@ theorem len_pos : 0 ≤ (ls : List α).len := by
induction ls <;> simp [*]
omega
-instance (a : Type u) : Arith.HasIntProp (List a) where
- prop_ty := λ ls => 0 ≤ ls.len
- prop := λ ls => ls.len_pos
+instance (l: List a) : Arith.HasIntPred (l.len) where
+ concl := 0 ≤ l.len
+ prop := l.len_pos
+
+example (l: List a): 0 ≤ l.len := by scalar_tac
-- Remark: if i < 0, then the result is none
def indexOpt (ls : List α) (i : Int) : Option α :=