feat: Elementarized tactics with motives, congruence, and absurdity #72

Merged
aniva merged 41 commits from goal/mapply into dev 2024-06-12 13:52:46 -07:00
3 changed files with 13 additions and 7 deletions
Showing only changes of commit cf17428001 - Show all commits

View File

@ -14,18 +14,24 @@ def instantiatePartialDelayedMVars (e: Expr): MetaM Expr := do
Meta.transform e
(pre := fun e => e.withApp fun f args => do
if let .mvar mvarId := f then
if ← mvarId.isAssigned then
return .visit <| (← instantiateMVars e)
if let some decl ← getDelayedMVarAssignment? mvarId then
if args.size ≥ decl.fvars.size then
-- Do not use instantiateMVars here. Only one step of instantiation should happen.
let pending ← instantiateMVars (.mvar decl.mvarIdPending)
if !pending.isMVar then
return .visit <| (← Meta.mkLambdaFVars decl.fvars pending).beta args
let pending := pending.abstract decl.fvars
let pending := pending.instantiateRevRange 0 decl.fvars.size args
let pending := mkAppRange pending decl.fvars.size args.size args
return .visit <| pending
return .continue)
@[export pantograph_instantiate_all_meta_m]
def instantiateAll (e: Expr): MetaM Expr := do
let e ← instantiateMVars e
let e ← instantiatePartialDelayedMVars e
let e ← unfoldAuxLemmas e
--let e ← instantiatePartialDelayedMVars e
return e
structure DelayedMVarInvocation where

View File

@ -88,11 +88,11 @@ def test_tactic : IO LSpec.TestSeq :=
vars := #[{ name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
}
let goal2: Protocol.Goal := {
name := "_uniq.14",
name := "_uniq.17",
target := { pp? := .some "x y → y x" },
vars := #[
{ name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }},
{ name := "_uniq.13", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}
{ name := "_uniq.16", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}
],
}
subroutine_runner [

View File

@ -771,7 +771,7 @@ def test_nat_zero_add_alt: TestM Unit := do
| other => do
addTest $ assertUnreachable $ other.toString
return ()
let (eqL, eqR, eqT) := ("_uniq.85", "_uniq.86", "_uniq.84")
let (eqL, eqR, eqT) := ("_uniq.88", "_uniq.89", "_uniq.87")
addTest $ LSpec.check tactic $ state3m2.goals.map (·.name.toString) = [eqL, eqR, eqT]
let [_motive, _major, _step, conduit] := state2.goals | panic! "Goals conflict"
let state2b ← match state3m2.resume [conduit] with
@ -789,8 +789,8 @@ def test_nat_zero_add_alt: TestM Unit := do
name := "_uniq.70",
userName? := .some "conduit",
target := {
pp? := .some "?m.79 ?m.68 = (n + 0 = n)",
sexp? := .some s!"((:c Eq) (:sort 0) (:subst ((:c Eq) (:mv {eqT}) (:mv {eqL}) (:mv {eqR})) (:fv {fvN}) (:mv {major})) ((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN})))",
pp? := .some "(?motive.a = ?motive.a) = (n + 0 = n)",
sexp? := .some s!"((:c Eq) (:sort 0) ((:c Eq) (:mv {eqT}) (:mv {eqL}) (:mv {eqR})) ((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN})))",
},
vars := #[{
name := fvN,