aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 10 Pull Requests 1 Packages Projects Releases 1 Wiki Activity

fix: Remove determination of major

This commit is contained in:
Leni Aniva 2024-04-22 09:52:13 -07:00
parent 3812aa56ec
commit feff62a3c5
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
3 changed files with 9 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
Pantograph/Tactic/MotivatedApply.lean
View File

@ -22,7 +22,6 @@ structure RecursorWithMotive where
-- .bvar index for the motive and major from the body -- .bvar index for the motive and major from the body
iMotive: Nat iMotive: Nat
iMajor: Nat
namespace RecursorWithMotive namespace RecursorWithMotive
@ -39,22 +38,22 @@ protected def surrogateMotiveType (info: RecursorWithMotive) (resultant: Expr):
return replaceForallBody motiveType resultantType return replaceForallBody motiveType resultantType
protected def phantomType (info: RecursorWithMotive) (mvars: Array Expr) (resultant: Expr): MetaM Expr := do protected def phantomType (info: RecursorWithMotive) (mvars: Array Expr) (resultant: Expr): MetaM Expr := do
let goalMotive := mvars.get! (info.nArgs - info.iMotive - 1) let motiveCall := Expr.instantiateRev info.body mvars
let goalMajor := mvars.get! (info.nArgs - info.iMajor - 1) Meta.mkEq motiveCall resultant
Meta.mkEq (.app goalMotive goalMajor) resultant
end RecursorWithMotive end RecursorWithMotive
def getRecursorInformation (recursorType: Expr): Option RecursorWithMotive := do def getRecursorInformation (recursorType: Expr): Option RecursorWithMotive := do
let (args, body) := getForallArgsBody recursorType let (args, body) := getForallArgsBody recursorType
let (iMotive, iMajor) ← match body with if ¬ body.isApp then
| .app (.bvar iMotive) (.bvar iMajor) => pure (iMotive, iMajor) .none
let iMotive ← match body.getAppFn with
| .bvar iMotive => pure iMotive
| _ => .none | _ => .none
return { return {
args, args,
body, body,
iMotive, iMotive,
iMajor,
} }
def collectMotiveArguments (forallBody: Expr): SSet Nat := def collectMotiveArguments (forallBody: Expr): SSet Nat :=
@ -86,8 +85,6 @@ def motivatedApply: Elab.Tactic.Tactic := λ stx => do
let argGoal ← if bvarIndex = info.iMotive then let argGoal ← if bvarIndex = info.iMotive then
let surrogateMotiveType ← info.surrogateMotiveType resultant let surrogateMotiveType ← info.surrogateMotiveType resultant
Meta.mkFreshExprMVar surrogateMotiveType .syntheticOpaque (userName := `motive) Meta.mkFreshExprMVar surrogateMotiveType .syntheticOpaque (userName := `motive)
else if bvarIndex = info.iMajor then
Meta.mkFreshExprMVar argType .syntheticOpaque (userName := `major)
else else
Meta.mkFreshExprMVar argType .syntheticOpaque (userName := .anonymous) Meta.mkFreshExprMVar argType .syntheticOpaque (userName := .anonymous)
let prev := prev ++ [argGoal] let prev := prev ++ [argGoal]

4
Test/Proofs.lean
View File

@ -662,9 +662,9 @@ def test_nat_zero_add: TestM Unit := do
addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) = addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
#[ #[
buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"), buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"),
buildNamedGoal "_uniq.68" [("n", "Nat")] "Nat" (.some "major"), 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 ?major = (n + 0 = n)" (.some "phantom") buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "phantom")
]) ])
let tactic := "exact n" let tactic := "exact n"

3
Test/Tactic/MotivatedApply.lean
View File

@ -31,7 +31,6 @@ def test_type_extract (env: Environment): IO LSpec.TestSeq :=
| .some info => pure info | .some info => pure info
| .none => throwError "Failed to extract recursor info" | .none => throwError "Failed to extract recursor info"
tests := tests ++ LSpec.check "iMotive" (info.iMotive = 2) tests := tests ++ LSpec.check "iMotive" (info.iMotive = 2)
tests := tests ++ LSpec.check "iMajor" (info.iMajor = 1)
let motiveType := info.getMotiveType let motiveType := info.getMotiveType
tests := tests ++ LSpec.check "motiveType" ("Nat → Sort ?u.1" = tests := tests ++ LSpec.check "motiveType" ("Nat → Sort ?u.1" =
(← exprToStr motiveType)) (← exprToStr motiveType))
@ -60,7 +59,7 @@ def test_execute (env: Environment): IO LSpec.TestSeq :=
"Nat → Prop", "Nat → Prop",
"Nat", "Nat",
"∀ (t : Nat), Nat.below t → ?motive t", "∀ (t : Nat), Nat.below t → ?motive t",
"?motive ?major = (n + 0 = n)", "?motive ?m.69 = (n + 0 = n)",
]) ])
tests := tests ++ test tests := tests ++ test
return tests return tests