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

fix: Tactics should produce .syntheticOpaque goals #100

Open
aniva wants to merge 1 commits from goal/tactic into dev
pull from: goal/tactic
merge into: aniva:dev
Conversation 1 Commits 1 Files Changed 3 +45 -44
3 changed files with 45 additions and 44 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit 5e99237e09 - Show all commits

80
Pantograph/Tactic/Congruence.lean
View File

@ -11,19 +11,19 @@ def congruenceArg (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
let userName := (← mvarId.getDecl).userName let userName := (← mvarId.getDecl).userName
let u ← Meta.mkFreshLevelMVar let u ← Meta.mkFreshLevelMVar
let α ← Meta.mkFreshExprMVar (.some $ mkSort u) let α ← Meta.mkFreshExprSyntheticOpaqueMVar (mkSort u)
.natural (userName := userName ++ `α) (tag := userName ++ `α)
let f ← Meta.mkFreshExprMVar (.some <| .forallE .anonymous α β .default) let f ← Meta.mkFreshExprSyntheticOpaqueMVar (.forallE .anonymous α β .default)
.synthetic (userName := userName ++ `f) (tag := userName ++ `f)
let a₁ ← Meta.mkFreshExprMVar (.some α) let a₁ ← Meta.mkFreshExprSyntheticOpaqueMVar α
.synthetic (userName := userName ++ `a₁) (tag := userName ++ `a₁)
let a₂ ← Meta.mkFreshExprMVar (.some α) let a₂ ← Meta.mkFreshExprSyntheticOpaqueMVar α
.synthetic (userName := userName ++ `a₂) (tag := userName ++ `a₂)
let h ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq a₁ a₂) let h ← Meta.mkFreshExprSyntheticOpaqueMVar (← Meta.mkEq a₁ a₂)
.synthetic (userName := userName ++ `h) (tag := userName ++ `h)
let conduitType ← Meta.mkEq (← Meta.mkEq (.app f a₁) (.app f a₂)) target let conduitType ← Meta.mkEq (← Meta.mkEq (.app f a₁) (.app f a₂)) target
let conduit ← Meta.mkFreshExprMVar conduitType let conduit ← Meta.mkFreshExprSyntheticOpaqueMVar conduitType
.synthetic (userName := userName ++ `conduit) (tag := userName ++ `conduit)
mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrArg f h) mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrArg f h)
let result := [α, a₁, a₂, f, h, conduit] let result := [α, a₁, a₂, f, h, conduit]
return result.map (·.mvarId!) 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 .some (β, _, _) := (← instantiateMVars target).eq? | throwError "Goal is not an Eq"
let userName := (← mvarId.getDecl).userName let userName := (← mvarId.getDecl).userName
let u ← Meta.mkFreshLevelMVar let u ← Meta.mkFreshLevelMVar
let α ← Meta.mkFreshExprMVar (.some $ mkSort u) let α ← Meta.mkFreshExprSyntheticOpaqueMVar (mkSort u)
.natural (userName := userName ++ `α) (tag := userName ++ `α)
let fType := .forallE .anonymous α β .default let fType := .forallE .anonymous α β .default
let f₁ ← Meta.mkFreshExprMVar (.some fType) let f₁ ← Meta.mkFreshExprSyntheticOpaqueMVar fType
.synthetic (userName := userName ++ `f₁) (tag := userName ++ `f₁)
let f₂ ← Meta.mkFreshExprMVar (.some fType) let f₂ ← Meta.mkFreshExprSyntheticOpaqueMVar fType
.synthetic (userName := userName ++ `f₂) (tag := userName ++ `f₂)
let a ← Meta.mkFreshExprMVar (.some α) let a ← Meta.mkFreshExprSyntheticOpaqueMVar α
.synthetic (userName := userName ++ `a) (tag := userName ++ `a)
let h ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq f₁ f₂) let h ← Meta.mkFreshExprSyntheticOpaqueMVar (← Meta.mkEq f₁ f₂)
.synthetic (userName := userName ++ `h) (tag := userName ++ `h)
let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a) (.app f₂ a)) target let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a) (.app f₂ a)) target
let conduit ← Meta.mkFreshExprMVar conduitType let conduit ← Meta.mkFreshExprSyntheticOpaqueMVar conduitType
.synthetic (userName := userName ++ `conduit) (tag := userName ++ `conduit)
mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrFun h a) mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrFun h a)
let result := [α, f₁, f₂, h, a, conduit] let result := [α, f₁, f₂, h, a, conduit]
return result.map (·.mvarId!) 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 .some (β, _, _) := (← instantiateMVars target).eq? | throwError "Goal is not an Eq"
let userName := (← mvarId.getDecl).userName let userName := (← mvarId.getDecl).userName
let u ← Meta.mkFreshLevelMVar let u ← Meta.mkFreshLevelMVar
let α ← Meta.mkFreshExprMVar (.some $ mkSort u) let α ← Meta.mkFreshExprSyntheticOpaqueMVar (mkSort u)
.natural (userName := userName ++ `α) (tag := userName ++ `α)
let fType := .forallE .anonymous α β .default let fType := .forallE .anonymous α β .default
let f₁ ← Meta.mkFreshExprMVar (.some fType) let f₁ ← Meta.mkFreshExprSyntheticOpaqueMVar fType
.synthetic (userName := userName ++ `f₁) (tag := userName ++ `f₁)
let f₂ ← Meta.mkFreshExprMVar (.some fType) let f₂ ← Meta.mkFreshExprSyntheticOpaqueMVar fType
.synthetic (userName := userName ++ `f₂) (tag := userName ++ `f₂)
let a₁ ← Meta.mkFreshExprMVar (.some α) let a₁ ← Meta.mkFreshExprSyntheticOpaqueMVar α
.synthetic (userName := userName ++ `a₁) (tag := userName ++ `a₁)
let a₂ ← Meta.mkFreshExprMVar (.some α) let a₂ ← Meta.mkFreshExprSyntheticOpaqueMVar α
.synthetic (userName := userName ++ `a₂) (tag := userName ++ `a₂)
let h₁ ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq f₁ f₂) let h₁ ← Meta.mkFreshExprSyntheticOpaqueMVar (← Meta.mkEq f₁ f₂)
.synthetic (userName := userName ++ `h₁) (tag := userName ++ `h₁)
let h₂ ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq a₁ a₂) let h₂ ← Meta.mkFreshExprSyntheticOpaqueMVar (← Meta.mkEq a₁ a₂)
.synthetic (userName := userName ++ `h₂) (tag := userName ++ `h₂)
let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a₁) (.app f₂ a₂)) target let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a₁) (.app f₂ a₂)) target
let conduit ← Meta.mkFreshExprMVar conduitType let conduit ← Meta.mkFreshExprSyntheticOpaqueMVar conduitType
.synthetic (userName := userName ++ `conduit) (tag := userName ++ `conduit)
mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongr h₁ h₂) mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongr h₁ h₂)
let result := [α, f₁, f₂, a₁, a₂, h₁, h₂, conduit] let result := [α, f₁, f₂, a₁, a₂, h₁, h₂, conduit]
return result.map (·.mvarId!) return result.map (·.mvarId!)

7
Pantograph/Tactic/MotivatedApply.lean
View File

@ -66,6 +66,7 @@ def motivatedApply (mvarId: MVarId) (recursor: Expr) : MetaM (Array Meta.Inducti
mvarId.checkNotAssigned `Pantograph.Tactic.motivatedApply mvarId.checkNotAssigned `Pantograph.Tactic.motivatedApply
let recursorType ← Meta.inferType recursor let recursorType ← Meta.inferType recursor
let resultant ← mvarId.getType let resultant ← mvarId.getType
let tag ← mvarId.getTag
let info ← match getRecursorInformation recursorType with let info ← match getRecursorInformation recursorType with
| .some info => pure info | .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 bvarIndex := info.nArgs - i - 1
let argGoal ← if bvarIndex = info.iMotive then let argGoal ← if bvarIndex = info.iMotive then
let surrogateMotiveType ← info.surrogateMotiveType prev resultant let surrogateMotiveType ← info.surrogateMotiveType prev resultant
Meta.mkFreshExprMVar surrogateMotiveType .syntheticOpaque (userName := `motive) Meta.mkFreshExprSyntheticOpaqueMVar surrogateMotiveType (tag := tag ++ `motive)
else else
Meta.mkFreshExprMVar argType .syntheticOpaque (userName := .anonymous) Meta.mkFreshExprSyntheticOpaqueMVar argType (tag := .anonymous)
let prev := prev ++ [argGoal] let prev := prev ++ [argGoal]
go (i + 1) prev go (i + 1) prev
termination_by info.nArgs - i 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 -- Create the conduit type which proves the result of the motive is equal to the goal
let conduitType ← info.conduitType newMVars resultant 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) mvarId.assign $ ← Meta.mkEqMP goalConduit (mkAppN recursor newMVars)
newMVars := newMVars ++ [goalConduit] newMVars := newMVars ++ [goalConduit]

2
Test/Tactic/Congruence.lean
View File

@ -25,7 +25,7 @@ def test_congr_arg_list : TestT Elab.TermElabM Unit := do
let f := newGoals.get! 3 let f := newGoals.get! 3
let h := newGoals.get! 4 let h := newGoals.get! 4
let c := newGoals.get! 5 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 "apply" (results.length = 0)
addTest $ LSpec.check "h" ((← exprToStr $ ← h.getType) = "?a₁ = ?a₂") addTest $ LSpec.check "h" ((← exprToStr $ ← h.getType) = "?a₁ = ?a₂")
addTest $ LSpec.check "conduit" ((← exprToStr $ ← c.getType) = "(?a₁.reverse = ?a₂.reverse) = (l1.reverse = l2.reverse)") addTest $ LSpec.check "conduit" ((← exprToStr $ ← c.getType) = "(?a₁.reverse = ?a₂.reverse) = (l1.reverse = l2.reverse)")