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

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
Conversation 6 Commits 41 Files Changed 22 +19 -44
2 changed files with 19 additions and 44 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit 75df7268c5 - Show all commits

44
Test/Tactic/MotivatedApply.lean
View File

@ -7,24 +7,11 @@ open Pantograph
namespace Pantograph.Test.Tactic.MotivatedApply namespace Pantograph.Test.Tactic.MotivatedApply
def valueAndType (recursor: String): MetaM (Expr × Expr) := do
let recursor ← match Parser.runParserCategory
(env := ← MonadEnv.getEnv)
(catName := `term)
(input := recursor)
(fileName := filename) with
| .ok syn => pure syn
| .error error => throwError "Failed to parse: {error}"
runTermElabMInMeta do
let recursor ← Elab.Term.elabTerm (stx := recursor) .none
let recursorType ← Meta.inferType recursor
return (recursor, recursorType)
def test_type_extract (env: Environment): IO LSpec.TestSeq := def test_type_extract (env: Environment): IO LSpec.TestSeq :=
runMetaMSeq env do runMetaMSeq env do
let mut tests := LSpec.TestSeq.done let mut tests := LSpec.TestSeq.done
let (recursor, recursorType) ← valueAndType "@Nat.brecOn" let recursor ← parseSentence "@Nat.brecOn"
let recursorType ← Meta.inferType recursor
tests := tests ++ LSpec.check "recursorType" ("{motive : Nat → Sort ?u.1} → (t : Nat) → ((t : Nat) → Nat.below t → motive t) → motive t" = tests := tests ++ LSpec.check "recursorType" ("{motive : Nat → Sort ?u.1} → (t : Nat) → ((t : Nat) → Nat.below t → motive t) → motive t" =
(← exprToStr recursorType)) (← exprToStr recursorType))
let info ← match Tactic.getRecursorInformation recursorType with let info ← match Tactic.getRecursorInformation recursorType with
@ -39,7 +26,7 @@ def test_type_extract (env: Environment): IO LSpec.TestSeq :=
def test_nat_brec_on (env: Environment): IO LSpec.TestSeq := def test_nat_brec_on (env: Environment): IO LSpec.TestSeq :=
let expr := "λ (n t: Nat) => n + 0 = n" let expr := "λ (n t: Nat) => n + 0 = n"
runMetaMSeq env do runMetaMSeq env do
let (expr, exprType) ← valueAndType expr let expr ← parseSentence expr
Meta.lambdaTelescope expr $ λ _ body => do Meta.lambdaTelescope expr $ λ _ body => do
let recursor ← match Parser.runParserCategory let recursor ← match Parser.runParserCategory
(env := ← MonadEnv.getEnv) (env := ← MonadEnv.getEnv)
@ -59,7 +46,7 @@ def test_nat_brec_on (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 ?m.69 = (n + 0 = n)", "?motive ?m.67 = (n + 0 = n)",
]) ])
tests := tests ++ test tests := tests ++ test
return tests return tests
@ -67,7 +54,7 @@ def test_nat_brec_on (env: Environment): IO LSpec.TestSeq :=
def test_list_brec_on (env: Environment): IO LSpec.TestSeq := def test_list_brec_on (env: Environment): IO LSpec.TestSeq :=
let expr := "λ {α : Type} (l: List α) => l ++ [] = [] ++ l" let expr := "λ {α : Type} (l: List α) => l ++ [] = [] ++ l"
runMetaMSeq env do runMetaMSeq env do
let (expr, exprType) ← valueAndType expr let expr ← parseSentence expr
Meta.lambdaTelescope expr $ λ _ body => do Meta.lambdaTelescope expr $ λ _ body => do
let recursor ← match Parser.runParserCategory let recursor ← match Parser.runParserCategory
(env := ← MonadEnv.getEnv) (env := ← MonadEnv.getEnv)
@ -84,11 +71,11 @@ def test_list_brec_on (env: Environment): IO LSpec.TestSeq :=
let newGoals ← runTacticOnMVar tactic target.mvarId! let newGoals ← runTacticOnMVar tactic target.mvarId!
pure $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = pure $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
[ [
"Type ?u.92", "Type ?u.90",
"List ?m.94 → Prop", "List ?m.92 → Prop",
"List ?m.94", "List ?m.92",
"∀ (t : List ?m.94), List.below t → ?motive t", "∀ (t : List ?m.92), List.below t → ?motive t",
"?motive ?m.96 = (l ++ [] = [] ++ l)", "?motive ?m.94 = (l ++ [] = [] ++ l)",
]) ])
tests := tests ++ test tests := tests ++ test
return tests return tests
@ -103,30 +90,31 @@ def test_partial_motive_instantiation (env: Environment): IO LSpec.TestSeq := do
(fileName := filename) with (fileName := filename) with
| .ok syn => pure syn | .ok syn => pure syn
| .error error => throwError "Failed to parse: {error}" | .error error => throwError "Failed to parse: {error}"
let (expr, exprType) ← valueAndType expr let expr ← parseSentence expr
Meta.lambdaTelescope expr $ λ _ body => do Meta.lambdaTelescope expr $ λ _ body => do
let mut tests := LSpec.TestSeq.done let mut tests := LSpec.TestSeq.done
-- Apply the tactic -- Apply the tactic
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
let tactic := Tactic.motivatedApply recursor let tactic := Tactic.motivatedApply recursor
let newGoals ← runTacticOnMVar tactic target.mvarId! let newGoals ← runTacticOnMVar tactic target.mvarId!
let majorId := 67
tests := tests ++ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = tests := tests ++ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
[ [
"Nat → Prop", "Nat → Prop",
"Nat", "Nat",
"∀ (t : Nat), Nat.below t → ?motive t", "∀ (t : Nat), Nat.below t → ?motive t",
"?motive ?m.69 = (n + 0 = n)", s!"?motive ?m.{majorId} = (n + 0 = n)",
])) ]))
let [motive, major, step, conduit] := newGoals | panic! "Incorrect goal number" let [motive, major, step, conduit] := newGoals | panic! "Incorrect goal number"
tests := tests ++ (LSpec.check "goal name" (major.name.toString = "_uniq.69")) tests := tests ++ (LSpec.check "goal name" (major.name.toString = s!"_uniq.{majorId}"))
-- Assign motive to `λ x => x + _` -- Assign motive to `λ x => x + _`
let (motive_assign, _) ← valueAndType "λ (x: Nat) => @Nat.add x + 0 = _" let motive_assign ← parseSentence "λ (x: Nat) => @Nat.add x + 0 = _"
motive.assign motive_assign motive.assign motive_assign
let test ← conduit.withContext do let test ← conduit.withContext do
let t := toString (← Meta.ppExpr $ ← conduit.getType) let t := toString (← Meta.ppExpr $ ← conduit.getType)
return LSpec.check "conduit" (t = "(?m.69.add + 0 = ?m.140 ?m.69) = (n + 0 = n)") return LSpec.check "conduit" (t = s!"(?m.{majorId}.add + 0 = ?m.138 ?m.{majorId}) = (n + 0 = n)")
tests := tests ++ test tests := tests ++ test
return tests return tests

19
Test/Tactic/NoConfuse.lean
View File

@ -7,23 +7,10 @@ open Pantograph
namespace Pantograph.Test.Tactic.NoConfuse namespace Pantograph.Test.Tactic.NoConfuse
def valueAndType (recursor: String): MetaM (Expr × Expr) := do
let recursor ← match Parser.runParserCategory
(env := ← MonadEnv.getEnv)
(catName := `term)
(input := recursor)
(fileName := filename) with
| .ok syn => pure syn
| .error error => throwError "Failed to parse: {error}"
runTermElabMInMeta do
let recursor ← Elab.Term.elabTerm (stx := recursor) .none
let recursorType ← Meta.inferType recursor
return (recursor, recursorType)
def test_nat (env: Environment): IO LSpec.TestSeq := def test_nat (env: Environment): IO LSpec.TestSeq :=
let expr := "λ (n: Nat) (h: 0 = n + 1) => False" let expr := "λ (n: Nat) (h: 0 = n + 1) => False"
runMetaMSeq env do runMetaMSeq env do
let (expr, exprType) ← valueAndType expr let expr ← parseSentence expr
Meta.lambdaTelescope expr $ λ _ body => do Meta.lambdaTelescope expr $ λ _ body => do
let recursor ← match Parser.runParserCategory let recursor ← match Parser.runParserCategory
(env := ← MonadEnv.getEnv) (env := ← MonadEnv.getEnv)
@ -46,7 +33,7 @@ def test_nat (env: Environment): IO LSpec.TestSeq :=
def test_nat_fail (env: Environment): IO LSpec.TestSeq := def test_nat_fail (env: Environment): IO LSpec.TestSeq :=
let expr := "λ (n: Nat) (h: n = n) => False" let expr := "λ (n: Nat) (h: n = n) => False"
runMetaMSeq env do runMetaMSeq env do
let (expr, _) ← valueAndType expr let expr ← parseSentence expr
Meta.lambdaTelescope expr $ λ _ body => do Meta.lambdaTelescope expr $ λ _ body => do
let recursor ← match Parser.runParserCategory let recursor ← match Parser.runParserCategory
(env := ← MonadEnv.getEnv) (env := ← MonadEnv.getEnv)
@ -70,7 +57,7 @@ def test_nat_fail (env: Environment): IO LSpec.TestSeq :=
def test_list (env: Environment): IO LSpec.TestSeq := def test_list (env: Environment): IO LSpec.TestSeq :=
let expr := "λ (l: List Nat) (h: [] = 1 :: l) => False" let expr := "λ (l: List Nat) (h: [] = 1 :: l) => False"
runMetaMSeq env do runMetaMSeq env do
let (expr, exprType) ← valueAndType expr let expr ← parseSentence expr
Meta.lambdaTelescope expr $ λ _ body => do Meta.lambdaTelescope expr $ λ _ body => do
let recursor ← match Parser.runParserCategory let recursor ← match Parser.runParserCategory
(env := ← MonadEnv.getEnv) (env := ← MonadEnv.getEnv)