From 5e99237e091757e1dab76a9db012df6b9ada4b8d Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 8 Sep 2024 14:13:39 -0700 Subject: [PATCH] fix: Tactics should produce `.syntheticOpaque` goals --- Pantograph/Tactic/Congruence.lean | 80 +++++++++++++-------------- Pantograph/Tactic/MotivatedApply.lean | 7 ++- Test/Tactic/Congruence.lean | 2 +- 3 files changed, 45 insertions(+), 44 deletions(-) diff --git a/Pantograph/Tactic/Congruence.lean b/Pantograph/Tactic/Congruence.lean index f72fc0a..0f6d80d 100644 --- a/Pantograph/Tactic/Congruence.lean +++ b/Pantograph/Tactic/Congruence.lean @@ -11,19 +11,19 @@ def congruenceArg (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do let userName := (← mvarId.getDecl).userName 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 α ← Meta.mkFreshExprSyntheticOpaqueMVar (mkSort u) + (tag := userName ++ `α) + let f ← Meta.mkFreshExprSyntheticOpaqueMVar (.forallE .anonymous α β .default) + (tag := userName ++ `f) + let a₁ ← Meta.mkFreshExprSyntheticOpaqueMVar α + (tag := userName ++ `a₁) + let a₂ ← Meta.mkFreshExprSyntheticOpaqueMVar α + (tag := userName ++ `a₂) + let h ← Meta.mkFreshExprSyntheticOpaqueMVar (← Meta.mkEq a₁ a₂) + (tag := userName ++ `h) let conduitType ← Meta.mkEq (← Meta.mkEq (.app f a₁) (.app f a₂)) target - let conduit ← Meta.mkFreshExprMVar conduitType - .synthetic (userName := userName ++ `conduit) + let conduit ← Meta.mkFreshExprSyntheticOpaqueMVar conduitType + (tag := userName ++ `conduit) mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrArg f h) let result := [α, a₁, a₂, f, h, conduit] return result.map (·.mvarId!) @@ -39,20 +39,20 @@ def congruenceFun (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do let .some (β, _, _) := (← instantiateMVars target).eq? | throwError "Goal is not an Eq" let userName := (← mvarId.getDecl).userName let u ← Meta.mkFreshLevelMVar - let α ← Meta.mkFreshExprMVar (.some $ mkSort u) - .natural (userName := userName ++ `α) + let α ← Meta.mkFreshExprSyntheticOpaqueMVar (mkSort u) + (tag := userName ++ `α) let fType := .forallE .anonymous α β .default - let f₁ ← Meta.mkFreshExprMVar (.some fType) - .synthetic (userName := userName ++ `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) + let f₁ ← Meta.mkFreshExprSyntheticOpaqueMVar fType + (tag := userName ++ `f₁) + let f₂ ← Meta.mkFreshExprSyntheticOpaqueMVar fType + (tag := userName ++ `f₂) + let a ← Meta.mkFreshExprSyntheticOpaqueMVar α + (tag := userName ++ `a) + let h ← Meta.mkFreshExprSyntheticOpaqueMVar (← Meta.mkEq f₁ f₂) + (tag := userName ++ `h) let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a) (.app f₂ a)) target - let conduit ← Meta.mkFreshExprMVar conduitType - .synthetic (userName := userName ++ `conduit) + let conduit ← Meta.mkFreshExprSyntheticOpaqueMVar conduitType + (tag := userName ++ `conduit) mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrFun h a) let result := [α, f₁, f₂, h, a, conduit] return result.map (·.mvarId!) @@ -68,24 +68,24 @@ def congruence (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do let .some (β, _, _) := (← instantiateMVars target).eq? | throwError "Goal is not an Eq" let userName := (← mvarId.getDecl).userName let u ← Meta.mkFreshLevelMVar - let α ← Meta.mkFreshExprMVar (.some $ mkSort u) - .natural (userName := userName ++ `α) + let α ← Meta.mkFreshExprSyntheticOpaqueMVar (mkSort u) + (tag := userName ++ `α) let fType := .forallE .anonymous α β .default - let f₁ ← Meta.mkFreshExprMVar (.some fType) - .synthetic (userName := userName ++ `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₂) + let f₁ ← Meta.mkFreshExprSyntheticOpaqueMVar fType + (tag := userName ++ `f₁) + let f₂ ← Meta.mkFreshExprSyntheticOpaqueMVar fType + (tag := userName ++ `f₂) + let a₁ ← Meta.mkFreshExprSyntheticOpaqueMVar α + (tag := userName ++ `a₁) + let a₂ ← Meta.mkFreshExprSyntheticOpaqueMVar α + (tag := userName ++ `a₂) + let h₁ ← Meta.mkFreshExprSyntheticOpaqueMVar (← Meta.mkEq f₁ f₂) + (tag := userName ++ `h₁) + let h₂ ← Meta.mkFreshExprSyntheticOpaqueMVar (← Meta.mkEq a₁ a₂) + (tag := userName ++ `h₂) let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a₁) (.app f₂ a₂)) target - let conduit ← Meta.mkFreshExprMVar conduitType - .synthetic (userName := userName ++ `conduit) + let conduit ← Meta.mkFreshExprSyntheticOpaqueMVar conduitType + (tag := userName ++ `conduit) mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongr h₁ h₂) let result := [α, f₁, f₂, a₁, a₂, h₁, h₂, conduit] return result.map (·.mvarId!) diff --git a/Pantograph/Tactic/MotivatedApply.lean b/Pantograph/Tactic/MotivatedApply.lean index 2c52f12..993d287 100644 --- a/Pantograph/Tactic/MotivatedApply.lean +++ b/Pantograph/Tactic/MotivatedApply.lean @@ -66,6 +66,7 @@ def motivatedApply (mvarId: MVarId) (recursor: Expr) : MetaM (Array Meta.Inducti mvarId.checkNotAssigned `Pantograph.Tactic.motivatedApply let recursorType ← Meta.inferType recursor let resultant ← mvarId.getType + let tag ← mvarId.getTag let info ← match getRecursorInformation recursorType with | .some info => pure info @@ -81,9 +82,9 @@ def motivatedApply (mvarId: MVarId) (recursor: Expr) : MetaM (Array Meta.Inducti let bvarIndex := info.nArgs - i - 1 let argGoal ← if bvarIndex = info.iMotive then let surrogateMotiveType ← info.surrogateMotiveType prev resultant - Meta.mkFreshExprMVar surrogateMotiveType .syntheticOpaque (userName := `motive) + Meta.mkFreshExprSyntheticOpaqueMVar surrogateMotiveType (tag := tag ++ `motive) else - Meta.mkFreshExprMVar argType .syntheticOpaque (userName := .anonymous) + Meta.mkFreshExprSyntheticOpaqueMVar argType (tag := .anonymous) let prev := prev ++ [argGoal] go (i + 1) prev termination_by info.nArgs - i @@ -91,7 +92,7 @@ def motivatedApply (mvarId: MVarId) (recursor: Expr) : MetaM (Array Meta.Inducti -- Create the conduit type which proves the result of the motive is equal to the goal let conduitType ← info.conduitType newMVars resultant - let goalConduit ← Meta.mkFreshExprMVar conduitType .natural (userName := `conduit) + let goalConduit ← Meta.mkFreshExprSyntheticOpaqueMVar conduitType (tag := `conduit) mvarId.assign $ ← Meta.mkEqMP goalConduit (mkAppN recursor newMVars) newMVars := newMVars ++ [goalConduit] diff --git a/Test/Tactic/Congruence.lean b/Test/Tactic/Congruence.lean index 836041c..180c2f4 100644 --- a/Test/Tactic/Congruence.lean +++ b/Test/Tactic/Congruence.lean @@ -25,7 +25,7 @@ def test_congr_arg_list : TestT Elab.TermElabM Unit := do let f := newGoals.get! 3 let h := newGoals.get! 4 let c := newGoals.get! 5 - let results ← f.apply (← parseSentence "List.reverse") + let results ← Meta.withAssignableSyntheticOpaque do f.apply (← parseSentence "List.reverse") addTest $ LSpec.check "apply" (results.length = 0) addTest $ LSpec.check "h" ((← exprToStr $ ← h.getType) = "?a₁ = ?a₂") addTest $ LSpec.check "conduit" ((← exprToStr $ ← c.getType) = "(?a₁.reverse = ?a₂.reverse) = (l1.reverse = l2.reverse)") -- 2.44.1