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
2 changed files with 19 additions and 8 deletions
Showing only changes of commit 6ffb227cd6 - Show all commits

View File

@ -37,7 +37,7 @@ protected def surrogateMotiveType (info: RecursorWithMotive) (resultant: Expr):
let resultantType ← Meta.inferType resultant let resultantType ← Meta.inferType resultant
return replaceForallBody motiveType resultantType return replaceForallBody motiveType resultantType
protected def phantomType (info: RecursorWithMotive) (mvars: Array Expr) (resultant: Expr): MetaM Expr := do protected def conduitType (info: RecursorWithMotive) (mvars: Array Expr) (resultant: Expr): MetaM Expr := do
let motiveCall := Expr.instantiateRev info.body mvars let motiveCall := Expr.instantiateRev info.body mvars
Meta.mkEq motiveCall resultant Meta.mkEq motiveCall resultant
@ -92,11 +92,11 @@ def motivatedApply: Elab.Tactic.Tactic := λ stx => do
termination_by info.nArgs - i termination_by info.nArgs - i
let mut newMVars ← go 0 #[] let mut newMVars ← go 0 #[]
goal.assign (mkAppN recursor newMVars) -- Create the conduit type which proves the result of the motive is equal to the goal
let conduitType ← info.conduitType newMVars resultant
let phantomType ← info.phantomType newMVars resultant let goalConduit ← Meta.mkFreshExprMVar conduitType .syntheticOpaque (userName := `conduit)
let goalPhantom ← Meta.mkFreshExprMVar phantomType .syntheticOpaque (userName := `phantom) goal.assign $ ← Meta.mkEqMP goalConduit (mkAppN recursor newMVars)
newMVars := newMVars ++ [goalPhantom] newMVars := newMVars ++ [goalConduit]
let nextGoals ← newMVars.toList.map (·.mvarId!) |>.filterM (not <$> ·.isAssigned) let nextGoals ← newMVars.toList.map (·.mvarId!) |>.filterM (not <$> ·.isAssigned)
pure nextGoals pure nextGoals

View File

@ -664,7 +664,7 @@ def test_nat_zero_add: TestM Unit := do
buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"), buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"),
buildNamedGoal "_uniq.68" [("n", "Nat")] "Nat", buildNamedGoal "_uniq.68" [("n", "Nat")] "Nat",
buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t", buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "phantom") buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit")
]) ])
let tactic := "exact n" let tactic := "exact n"
@ -703,7 +703,18 @@ def test_nat_zero_add: TestM Unit := do
#[buildGoal [("n", "Nat"), ("t", "Nat"), ("h", "Nat.below t")] "t + 0 = t"]) #[buildGoal [("n", "Nat"), ("t", "Nat"), ("h", "Nat.below t")] "t + 0 = t"])
let tactic := "simp" let tactic := "simp"
let stateF ← match ← state3.tryTactic (goalId := 0) (tactic := tactic) with let state3d ← match ← state3.tryTactic (goalId := 0) (tactic := tactic) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
let state2d ← match state3d.continue state2c with
| .ok state => pure state
| .error e => do
addTest $ assertUnreachable e
return ()
let tactic := "rfl"
let stateF ← match ← state2d.tryTactic (goalId := 0) (tactic := tactic) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString