From 92acf7782c66f9efc6026a5896be35b84b202f5d Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 20 May 2024 11:51:35 -0700 Subject: [PATCH] test: CongruenceArg tactic --- Pantograph/Tactic/Congruence.lean | 81 +++++++++++++++++-------------- Test/Common.lean | 15 ++++++ Test/Main.lean | 1 + Test/Tactic.lean | 1 + Test/Tactic/Congruence.lean | 36 ++++++++++++++ Test/Tactic/NoConfuse.lean | 6 +-- 6 files changed, 100 insertions(+), 40 deletions(-) create mode 100644 Test/Tactic/Congruence.lean diff --git a/Pantograph/Tactic/Congruence.lean b/Pantograph/Tactic/Congruence.lean index 3de904f..bbb9d75 100644 --- a/Pantograph/Tactic/Congruence.lean +++ b/Pantograph/Tactic/Congruence.lean @@ -6,73 +6,80 @@ namespace Pantograph.Tactic def congruenceArg: Elab.Tactic.TacticM Unit := do let goal ← Elab.Tactic.getMainGoal - let .some (beta, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq" - -- Create the descendant goals + let .some (β, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq" + let userName := (← goal.getDecl).userName let nextGoals ← goal.withContext do let u ← Meta.mkFreshLevelMVar - let alpha ← Meta.mkFreshExprMVar (.some $ mkSort u) .natural .anonymous - let f ← Meta.mkFreshExprMVar (.some <| .forallE .anonymous alpha beta .default) - .synthetic (userName := goal.name ++ `f) - let a₁ ← Meta.mkFreshExprMVar (.some alpha) - .synthetic (userName := goal.name ++ `a₁) - let a₂ ← Meta.mkFreshExprMVar (.some alpha) - .synthetic (userName := goal.name ++ `a₂) - let h ← Meta.mkEq a₁ a₂ + let α ← Meta.mkFreshExprMVar (.some $ mkSort u) + .natural (userName := userName ++ `α) + let f ← Meta.mkFreshExprMVar (.some <| .forallE .anonymous α β .default) + .synthetic (userName := userName ++ `f) + let a₁ ← Meta.mkFreshExprMVar (.some α) + .synthetic (userName := userName ++ `a₁) + let a₂ ← Meta.mkFreshExprMVar (.some α) + .synthetic (userName := userName ++ `a₂) + let h ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq a₁ a₂) + .synthetic (userName := userName ++ `h) let conduitType ← Meta.mkEq (← Meta.mkEq (.app f a₁) (.app f a₂)) (← goal.getType) let conduit ← Meta.mkFreshExprMVar conduitType - .synthetic (userName := goal.name ++ `conduit) + .synthetic (userName := userName ++ `conduit) goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrArg f h) - return [alpha, a₁, a₂, f, h, conduit] + return [α, a₁, a₂, f, h, conduit] Elab.Tactic.setGoals <| nextGoals.map (·.mvarId!) def congruenceFun: Elab.Tactic.TacticM Unit := do let goal ← Elab.Tactic.getMainGoal - let .some (beta, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq" - -- Create the descendant goals + let .some (β, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq" + let userName := (← goal.getDecl).userName let nextGoals ← goal.withContext do let u ← Meta.mkFreshLevelMVar - let alpha ← Meta.mkFreshExprMVar (.some $ mkSort u) .natural .anonymous - let fType := .forallE .anonymous alpha beta .default + let α ← Meta.mkFreshExprMVar (.some $ mkSort u) + .natural (userName := userName ++ `α) + let fType := .forallE .anonymous α β .default let f₁ ← Meta.mkFreshExprMVar (.some fType) - .synthetic (userName := goal.name ++ `f₁) + .synthetic (userName := userName ++ `f₁) let f₂ ← Meta.mkFreshExprMVar (.some fType) - .synthetic (userName := goal.name ++ `f₂) - let a ← Meta.mkFreshExprMVar (.some alpha) - .synthetic (userName := goal.name ++ `a) - let h ← Meta.mkEq f₁ f₂ + .synthetic (userName := userName ++ `f₂) + let a ← Meta.mkFreshExprMVar (.some α) + .synthetic (userName := userName ++ `a) + let h ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq f₁ f₂) + .synthetic (userName := userName ++ `h) let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a) (.app f₂ a)) (← goal.getType) let conduit ← Meta.mkFreshExprMVar conduitType - .synthetic (userName := goal.name ++ `conduit) + .synthetic (userName := userName ++ `conduit) goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrFun h a) - return [alpha, f₁, f₂, h, a, conduit] + return [α, f₁, f₂, h, a, conduit] Elab.Tactic.setGoals <| nextGoals.map (·.mvarId!) def congruence: Elab.Tactic.TacticM Unit := do let goal ← Elab.Tactic.getMainGoal - let .some (beta, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq" - -- Create the descendant goals + let .some (β, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq" + let userName := (← goal.getDecl).userName let nextGoals ← goal.withContext do let u ← Meta.mkFreshLevelMVar - let alpha ← Meta.mkFreshExprMVar (.some $ mkSort u) .natural .anonymous - let fType := .forallE .anonymous alpha beta .default + let α ← Meta.mkFreshExprMVar (.some $ mkSort u) + .natural (userName := userName ++ `α) + let fType := .forallE .anonymous α β .default let f₁ ← Meta.mkFreshExprMVar (.some fType) - .synthetic (userName := goal.name ++ `f₁) + .synthetic (userName := userName ++ `f₁) let f₂ ← Meta.mkFreshExprMVar (.some fType) - .synthetic (userName := goal.name ++ `f₂) - let a₁ ← Meta.mkFreshExprMVar (.some alpha) - .synthetic (userName := goal.name ++ `a₁) - let a₂ ← Meta.mkFreshExprMVar (.some alpha) - .synthetic (userName := goal.name ++ `a₂) - let h₁ ← Meta.mkEq f₁ f₂ - let h₂ ← Meta.mkEq a₁ a₂ + .synthetic (userName := userName ++ `f₂) + let a₁ ← Meta.mkFreshExprMVar (.some α) + .synthetic (userName := userName ++ `a₁) + let a₂ ← Meta.mkFreshExprMVar (.some α) + .synthetic (userName := userName ++ `a₂) + let h₁ ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq f₁ f₂) + .synthetic (userName := userName ++ `h₁) + let h₂ ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq a₁ a₂) + .synthetic (userName := userName ++ `h₂) let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a₁) (.app f₂ a₂)) (← goal.getType) let conduit ← Meta.mkFreshExprMVar conduitType - .synthetic (userName := goal.name ++ `conduit) + .synthetic (userName := userName ++ `conduit) goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongr h₁ h₂) - return [alpha, f₁, f₂, a₁, a₂, h₁, h₂, conduit] + return [α, f₁, f₂, a₁, a₂, h₁, h₂, conduit] Elab.Tactic.setGoals <| nextGoals.map (·.mvarId!) end Pantograph.Tactic diff --git a/Test/Common.lean b/Test/Common.lean index 6ea4fb2..c656309 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -27,6 +27,7 @@ def Goal.devolatilize (goal: Goal): Goal := name := "", } +deriving instance DecidableEq, Repr for Name deriving instance DecidableEq, Repr for Expression deriving instance DecidableEq, Repr for Variable deriving instance DecidableEq, Repr for Goal @@ -65,9 +66,23 @@ def runTermElabMInMeta { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e +def parseSentence (s: String): MetaM Expr := do + let recursor ← match Parser.runParserCategory + (env := ← MonadEnv.getEnv) + (catName := `term) + (input := s) + (fileName := filename) with + | .ok syn => pure syn + | .error error => throwError "Failed to parse: {error}" + runTermElabMInMeta $ Elab.Term.elabTerm (stx := recursor) .none + def runTacticOnMVar (tacticM: Elab.Tactic.TacticM Unit) (goal: MVarId): Elab.TermElabM (List MVarId) := do let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] } return newGoals.goals +def mvarUserNameAndType (mvarId: MVarId): MetaM (Name × String) := do + let name := (← mvarId.getDecl).userName + let t ← exprToStr (← mvarId.getType) + return (name, t) end Test diff --git a/Test/Main.lean b/Test/Main.lean index 4a1ca69..31042c5 100644 --- a/Test/Main.lean +++ b/Test/Main.lean @@ -49,6 +49,7 @@ def main (args: List String) := do ("Metavar", Metavar.suite env_default), ("Proofs", Proofs.suite env_default), ("Serial", Serial.suite env_default), + ("Tactic/Congruence", Tactic.Congruence.suite env_default), ("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default), ("Tactic/No Confuse", Tactic.NoConfuse.suite env_default), ] diff --git a/Test/Tactic.lean b/Test/Tactic.lean index f1e2649..5863ec0 100644 --- a/Test/Tactic.lean +++ b/Test/Tactic.lean @@ -1,2 +1,3 @@ +import Test.Tactic.Congruence import Test.Tactic.MotivatedApply import Test.Tactic.NoConfuse diff --git a/Test/Tactic/Congruence.lean b/Test/Tactic/Congruence.lean new file mode 100644 index 0000000..7ef358a --- /dev/null +++ b/Test/Tactic/Congruence.lean @@ -0,0 +1,36 @@ +import LSpec +import Lean +import Test.Common + +open Lean +open Pantograph + +namespace Pantograph.Test.Tactic.Congruence + +def test_congr_arg (env: Environment): IO LSpec.TestSeq := + let expr := "λ (n m: Nat) (h: n = m) => n * n = m * m" + runMetaMSeq env do + let expr ← parseSentence expr + Meta.lambdaTelescope expr $ λ _ body => do + let mut tests := LSpec.TestSeq.done + let target ← Meta.mkFreshExprSyntheticOpaqueMVar body + let test ← runTermElabMInMeta do + let newGoals ← runTacticOnMVar Tactic.congruenceArg target.mvarId! + pure $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) = + [ + (`α, "Sort ?u.70"), + (`a₁, "?α"), + (`a₂, "?α"), + (`f, "?α → Nat"), + (`h, "?a₁ = ?a₂"), + (`conduit, "(?f ?a₁ = ?f ?a₂) = (n * n = m * m)"), + ]) + tests := tests ++ test + return tests + +def suite (env: Environment): List (String × IO LSpec.TestSeq) := + [ + ("congrArg", test_congr_arg env), + ] + +end Pantograph.Test.Tactic.Congruence diff --git a/Test/Tactic/NoConfuse.lean b/Test/Tactic/NoConfuse.lean index 54c2be7..442e2ca 100644 --- a/Test/Tactic/NoConfuse.lean +++ b/Test/Tactic/NoConfuse.lean @@ -92,9 +92,9 @@ def test_list (env: Environment): IO LSpec.TestSeq := def suite (env: Environment): List (String × IO LSpec.TestSeq) := [ - ("nat", test_nat env), - ("nat_fail", test_nat_fail env), - ("list", test_list env), + ("Nat", test_nat env), + ("Nat fail", test_nat_fail env), + ("List", test_list env), ] end Pantograph.Test.Tactic.NoConfuse