Pantograph/Tactic/Congruence.lean

@@ -6,80 +6,73 @@ namespace Pantograph.Tactic
 
 def congruenceArg: Elab.Tactic.TacticM Unit := do
   let goal ← Elab.Tactic.getMainGoal
-  let .some (β, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq"
-  let userName := (← goal.getDecl).userName
+  let .some (beta, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq"
+  -- Create the descendant goals
 
   let nextGoals ← goal.withContext do
     let u ← Meta.mkFreshLevelMVar
-    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 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 conduitType ← Meta.mkEq (← Meta.mkEq (.app f a₁) (.app f a₂)) (← goal.getType)
     let conduit ← Meta.mkFreshExprMVar conduitType
-      .synthetic (userName := userName ++ `conduit)
+      .synthetic (userName := goal.name ++ `conduit)
     goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrArg f h)
-    return [α, a₁, a₂, f,  h, conduit]
+    return [alpha, 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 (β, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq"
-  let userName := (← goal.getDecl).userName
+  let .some (beta, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq"
+  -- Create the descendant goals
 
   let nextGoals ← goal.withContext do
     let u ← Meta.mkFreshLevelMVar
-    let α ← Meta.mkFreshExprMVar (.some $ mkSort u)
-      .natural (userName := userName ++ `α)
-    let fType := .forallE .anonymous α β .default
+    let alpha ← Meta.mkFreshExprMVar (.some $ mkSort u) .natural .anonymous
+    let fType := .forallE .anonymous alpha beta .default
     let f₁ ← Meta.mkFreshExprMVar (.some fType)
-      .synthetic (userName := userName ++ `f₁)
+      .synthetic (userName := goal.name ++ `f₁)
     let f₂ ← Meta.mkFreshExprMVar (.some fType)
-      .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)
+      .synthetic (userName := goal.name ++ `f₂)
+    let a ← Meta.mkFreshExprMVar (.some alpha)
+      .synthetic (userName := goal.name ++ `a)
+    let h ← Meta.mkEq f₁ f₂
     let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a) (.app f₂ a)) (← goal.getType)
     let conduit ← Meta.mkFreshExprMVar conduitType
-      .synthetic (userName := userName ++ `conduit)
+      .synthetic (userName := goal.name ++ `conduit)
     goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrFun h a)
-    return [α, f₁, f₂, h, a, conduit]
+    return [alpha, 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 (β, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq"
-  let userName := (← goal.getDecl).userName
+  let .some (beta, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq"
+  -- Create the descendant goals
 
   let nextGoals ← goal.withContext do
     let u ← Meta.mkFreshLevelMVar
-    let α ← Meta.mkFreshExprMVar (.some $ mkSort u)
-      .natural (userName := userName ++ `α)
-    let fType := .forallE .anonymous α β .default
+    let alpha ← Meta.mkFreshExprMVar (.some $ mkSort u) .natural .anonymous
+    let fType := .forallE .anonymous alpha beta .default
     let f₁ ← Meta.mkFreshExprMVar (.some fType)
-      .synthetic (userName := userName ++ `f₁)
+      .synthetic (userName := goal.name ++ `f₁)
     let f₂ ← Meta.mkFreshExprMVar (.some fType)
-      .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₂)
+      .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₂
     let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a₁) (.app f₂ a₂)) (← goal.getType)
     let conduit ← Meta.mkFreshExprMVar conduitType
-      .synthetic (userName := userName ++ `conduit)
+      .synthetic (userName := goal.name ++ `conduit)
     goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongr h₁ h₂)
-    return [α, f₁, f₂, a₁, a₂, h₁, h₂, conduit]
+    return [alpha, f₁, f₂, a₁, a₂, h₁, h₂, conduit]
   Elab.Tactic.setGoals <| nextGoals.map (·.mvarId!)
 
 end Pantograph.Tactic

Test/Common.lean

@@ -27,7 +27,6 @@ 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
@@ -66,23 +65,9 @@ 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
 

Test/Main.lean

@@ -49,7 +49,6 @@ 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),
   ]

Test/Tactic.lean

@@ -1,3 +1,2 @@
-import Test.Tactic.Congruence
 import Test.Tactic.MotivatedApply
 import Test.Tactic.NoConfuse

Test/Tactic/Congruence.lean

@@ -1,36 +0,0 @@
-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

Test/Tactic/MotivatedApply.lean

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

Test/Tactic/NoConfuse.lean

@@ -7,10 +7,23 @@ open Pantograph
 
 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 :=
   let expr := "λ (n: Nat) (h: 0 = n + 1) => False"
   runMetaMSeq env do
-    let expr ← parseSentence expr
+    let (expr, exprType) ← valueAndType expr
     Meta.lambdaTelescope expr $ λ _ body => do
       let recursor ← match Parser.runParserCategory
         (env := ← MonadEnv.getEnv)
@@ -33,7 +46,7 @@ def test_nat (env: Environment): IO LSpec.TestSeq :=
 def test_nat_fail (env: Environment): IO LSpec.TestSeq :=
   let expr := "λ (n: Nat) (h: n = n) => False"
   runMetaMSeq env do
-    let expr ← parseSentence expr
+    let (expr, _) ← valueAndType expr
     Meta.lambdaTelescope expr $ λ _ body => do
       let recursor ← match Parser.runParserCategory
         (env := ← MonadEnv.getEnv)
@@ -57,7 +70,7 @@ def test_nat_fail (env: Environment): IO LSpec.TestSeq :=
 def test_list (env: Environment): IO LSpec.TestSeq :=
   let expr := "λ (l: List Nat) (h: [] = 1 :: l) => False"
   runMetaMSeq env do
-    let expr ← parseSentence expr
+    let (expr, exprType) ← valueAndType expr
     Meta.lambdaTelescope expr $ λ _ body => do
       let recursor ← match Parser.runParserCategory
         (env := ← MonadEnv.getEnv)
@@ -79,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