From f3b22b5cca9bc1154f55a81c9a82dc491074067d Mon Sep 17 00:00:00 2001 From: Ryan Lahfa Date: Wed, 12 Jun 2024 13:59:11 +0200 Subject: backends/lean: introduce `HasIntPred` automation `HasIntPred` enable generation of facts based on specific terms in the context rather than their types, e.g. if the "length of a list" occurs in the context, generate the fact 0 ≤ length of that list, which can be further used for `scalar_tac` automation to discharge bounds goals. The aim is to use it to simplify various height related computations, e.g. whenever "height of a (left ; right) tree" is encountered, generate "height left < height of a (left ; right) tree", etc. Signed-off-by: Ryan Lahfa --- backends/lean/Base/Arith/Int.lean | 38 +++++++++++++++++++++++++++++++++----- 1 file changed, 33 insertions(+), 5 deletions(-) (limited to 'backends/lean/Base/Arith') diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean index 4a3db5f8..a1cb9da3 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 : Prop) where concl : Prop @@ -106,12 +111,18 @@ 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 + -- of the inferred type rather than the declaration expression + -- which is often just a name. + 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 → Expr → Array Expr) (instantiateProjectionFn : Expr → Array Expr) : MetaM (Option Expr) := do trace[Arith] fName -- TODO: do we need Lean.observing? -- This actually eliminates the error messages @@ -119,23 +130,31 @@ def lookupProp (fName : String) (className : Name) (e : Expr) : MetaM (Option Ex 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 ty 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 ty _ => #[ty]) (fun e => #[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 => #[term]) (fun _ => #[]) + +-- 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 +212,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 +234,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 -- cgit v1.2.3 From 007c9024c0c3b549049a55243b391ae2337ad616 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 17 Jun 2024 06:26:43 +0200 Subject: Make a minor cleanup --- backends/lean/Base/Arith/Int.lean | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) (limited to 'backends/lean/Base/Arith') diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean index ab6dd4ab..068d6f2f 100644 --- a/backends/lean/Base/Arith/Int.lean +++ b/backends/lean/Base/Arith/Int.lean @@ -112,9 +112,10 @@ def collectInstancesFromMainCtx (k : Expr → MetaM (Option Expr)) : Tactic.Tact -- Explore the declarations let decls ← ctx.getDecls let hs ← decls.foldlM (fun hs d => do - -- Collect instances over all subexpressions - -- of the inferred type rather than the declaration expression - -- which is often just a name. + -- 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 @@ -122,26 +123,27 @@ def collectInstancesFromMainCtx (k : Expr → MetaM (Option Expr)) : Tactic.Tact collectInstances k hs (← Tactic.getMainTarget) -- Helper -def lookupProp (fName : String) (className : Name) (e : Expr) (instantiateClassFn : Expr → Expr → Array Expr) (instantiateProjectionFn : Expr → Array 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 (instantiateClassFn ty e) + 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 (instantiateProjectionFn 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 (fun ty _ => #[ty]) (fun e => #[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 @@ -149,7 +151,7 @@ def collectHasIntPropInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do -- Return an instance of `HasIntPred` for `e` if it has some def lookupHasIntPred (e : Expr) : MetaM (Option Expr) := - lookupProp "lookupHasIntPred" ``HasIntPred e (fun _ term => #[term]) (fun _ => #[]) + 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 -- cgit v1.2.3