Compare commits
1 Commits
dev
...
goal/tacti
Author | SHA1 | Date |
---|---|---|
Leni Aniva | 5e99237e09 |
|
@ -28,7 +28,7 @@ structure Options where
|
|||
-- See `pp.implementationDetailHyps`
|
||||
printImplementationDetailHyps: Bool := false
|
||||
-- If this is set to `true`, goals will never go dormant, so you don't have to manage resumption
|
||||
automaticMode: Bool := true
|
||||
automaticMode: Bool := false
|
||||
deriving Lean.ToJson
|
||||
|
||||
abbrev OptionsT := ReaderT Options
|
||||
|
|
|
@ -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!)
|
||||
|
|
|
@ -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]
|
||||
|
||||
|
|
10
README.md
10
README.md
|
@ -91,10 +91,9 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
|
|||
* `options.set { key: value, ... }`: Set one or more options (not Lean options; those
|
||||
have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean`
|
||||
|
||||
One particular option for interest for machine learning researchers is the
|
||||
automatic mode (flag: `"automaticMode"`). By default it is turned on, with
|
||||
all goals automatically resuming. This makes Pantograph act like a gym,
|
||||
with no resumption necessary to manage your goals.
|
||||
One particular option for interest for machine learning researchers is the automatic mode.
|
||||
`options.set { "automaticMode": true }`. This makes Pantograph act like
|
||||
LeanDojo, with no resumption necessary to manage your goals.
|
||||
* `options.print`: Display the current set of options
|
||||
* `goal.start {["name": <name>], ["expr": <expr>], ["levels": [<levels>]], ["copyFrom": <symbol>]}`:
|
||||
Start a new proof from a given expression or symbol
|
||||
|
@ -143,9 +142,6 @@ ulimit -s unlimited
|
|||
with `Pantograph` which mirrors the REPL commands above. It is recommended to
|
||||
call Pantograph via this FFI since it provides a tremendous speed up.
|
||||
|
||||
Note that there isn't a 1-1 correspondence between executable (REPL) commands
|
||||
and library functions.
|
||||
|
||||
## Developing
|
||||
|
||||
A Lean development shell is provided in the Nix flake.
|
||||
|
|
|
@ -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)")
|
||||
|
|
Loading…
Reference in New Issue