feat: Prograde tactics #83
|
@ -51,7 +51,7 @@ structure Variable where
|
|||
/-- The name displayed to the user -/
|
||||
userName: String
|
||||
/-- Does the name contain a dagger -/
|
||||
isInaccessible?: Option Bool := .none
|
||||
isInaccessible?: Option Bool := .some false
|
||||
type?: Option Expression := .none
|
||||
value?: Option Expression := .none
|
||||
deriving Lean.ToJson
|
||||
|
|
|
@ -215,11 +215,13 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
|
|||
return {
|
||||
name := ofName fvarId.name,
|
||||
userName:= ofName userName.simpMacroScopes,
|
||||
isInaccessible? := .some userName.isInaccessibleUserName
|
||||
}
|
||||
| .ldecl _ fvarId userName _ _ _ _ => do
|
||||
return {
|
||||
name := ofName fvarId.name,
|
||||
userName := toString userName.simpMacroScopes,
|
||||
isInaccessible? := .some userName.isInaccessibleUserName
|
||||
}
|
||||
let ppVar (localDecl : LocalDecl) : MetaM Protocol.Variable := do
|
||||
match localDecl with
|
||||
|
|
|
@ -19,9 +19,12 @@ def assign (goal: MVarId) (expr: Expr): MetaM (List MVarId) := do
|
|||
nextGoals.toList.filterM (not <$> ·.isAssigned)
|
||||
|
||||
def evalAssign : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
|
||||
let goalType ← Elab.Tactic.getMainTarget
|
||||
let expr ← Elab.Term.elabTermAndSynthesize (stx := stx) (expectedType? := .some goalType)
|
||||
let nextGoals ← assign (← Elab.Tactic.getMainGoal) expr
|
||||
let target ← Elab.Tactic.getMainTarget
|
||||
let (expr, nextGoals) ← Elab.Tactic.elabTermWithHoles stx
|
||||
(expectedType? := .some target)
|
||||
(tagSuffix := .anonymous )
|
||||
(allowNaturalHoles := true)
|
||||
(← Elab.Tactic.getMainGoal).assign expr
|
||||
Elab.Tactic.setGoals nextGoals
|
||||
|
||||
|
||||
|
|
|
@ -64,13 +64,14 @@ def «let» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResult
|
|||
let lctx ← MonadLCtx.getLCtx
|
||||
|
||||
-- The branch goal inherits the same context, but with a different type
|
||||
let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type
|
||||
let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type (userName := binderName)
|
||||
|
||||
assert! ¬ type.hasLooseBVars
|
||||
let upstreamType := .letE binderName type mvarBranch (← mvarId.getType) false
|
||||
let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
|
||||
upstreamType (kind := MetavarKind.synthetic) (userName := ← mvarId.getTag)
|
||||
mvarId.assign mvarUpstream
|
||||
let mvarUpstream ← Meta.withLetDecl binderName type mvarBranch $ λ fvar => do
|
||||
let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
|
||||
(type := ← mvarId.getType) (kind := MetavarKind.synthetic) (userName := ← mvarId.getTag)
|
||||
mvarId.assign $ .letE binderName type fvar mvarUpstream (nonDep := false)
|
||||
pure mvarUpstream
|
||||
|
||||
return {
|
||||
main := mvarUpstream.mvarId!,
|
||||
|
|
|
@ -198,15 +198,16 @@ def test_proposition_generation: TestM Unit := do
|
|||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) =
|
||||
#[.some "∀ (x : Nat), ?m.29 x"])
|
||||
#[.some "?m.29 x"])
|
||||
addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone
|
||||
|
||||
let state3 ← match ← state2.tryAssign (goalId := 0) (expr := "fun x => Eq.refl x") with
|
||||
let assign := "Eq.refl x"
|
||||
let state3 ← match ← state2.tryAssign (goalId := 0) (expr := assign) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check ":= Eq.refl" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) =
|
||||
addTest $ LSpec.check s!":= {assign}" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) =
|
||||
#[])
|
||||
|
||||
addTest $ LSpec.test "(3 root)" state3.rootExpr?.isSome
|
||||
|
|
|
@ -175,7 +175,7 @@ def test_delta_variable: TestM Unit := do
|
|||
vars := (nameType.map fun x => ({
|
||||
userName := x.fst,
|
||||
type? := x.snd.map (λ type => { pp? := type }),
|
||||
isInaccessible? := x.snd.map (λ _ => false)
|
||||
isInaccessible? := .some false,
|
||||
})).toArray
|
||||
}
|
||||
|
||||
|
@ -544,83 +544,6 @@ def test_calc: TestM Unit := do
|
|||
("h1", "a + b = b + c"), ("h2", "b + c = c + d")] ++ free
|
||||
buildGoal free target userName?
|
||||
|
||||
def test_let (specialized: Bool): TestM Unit := do
|
||||
let state? ← startProof (.expr "∀ (a: Nat) (p: Prop), p → p ∨ ¬p")
|
||||
let state0 ← match state? with
|
||||
| .some state => pure state
|
||||
| .none => do
|
||||
addTest $ assertUnreachable "Goal could not parse"
|
||||
return ()
|
||||
let tactic := "intro a p h"
|
||||
let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
|
||||
#[interiorGoal [] "p ∨ ¬p"])
|
||||
|
||||
|
||||
let letType := "Nat"
|
||||
let expr := s!"let b: {letType} := _; _"
|
||||
let result2 ← match specialized with
|
||||
| true => state1.tryLet (goalId := 0) (binderName := "b") (type := letType)
|
||||
| false => state1.tryAssign (goalId := 0) (expr := expr)
|
||||
let state2 ← match result2 with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
let serializedState2 ← state2.serializeGoals (options := ← read)
|
||||
addTest $ LSpec.check expr (serializedState2.map (·.devolatilize) =
|
||||
#[
|
||||
interiorGoal [] letType,
|
||||
interiorGoal [] "let b := ?m.20;\np ∨ ¬p"
|
||||
])
|
||||
-- Check that the goal mvar ids match up
|
||||
addTest $ LSpec.check "(mvarId)" ((serializedState2.map (·.name) |>.get! 0) = "_uniq.20")
|
||||
|
||||
let tactic := "exact a"
|
||||
let state3 ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check tactic ((← state3.serializeGoals (options := ← read)).map (·.devolatilize) = #[])
|
||||
|
||||
let state3r ← match state3.continue state2 with
|
||||
| .error msg => do
|
||||
addTest $ assertUnreachable $ msg
|
||||
return ()
|
||||
| .ok state => pure state
|
||||
addTest $ LSpec.check "(continue)" ((← state3r.serializeGoals (options := ← read)).map (·.devolatilize) =
|
||||
#[interiorGoal [] "let b := a;\np ∨ ¬p"])
|
||||
|
||||
let tactic := "exact h"
|
||||
match ← state3r.tryTactic (goalId := 0) (tactic := tactic) with
|
||||
| .failure #[message] =>
|
||||
addTest $ LSpec.check tactic (message = "type mismatch\n h\nhas type\n p : Prop\nbut is expected to have type\n let b := a;\n p ∨ ¬p : Prop")
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
||||
let tactic := "intro b"
|
||||
let state4 ← match ← state3r.tryTactic (goalId := 0) (tactic := tactic) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
let tactic := "exact Or.inl h"
|
||||
let state5 ← match ← state4.tryTactic (goalId := 0) (tactic := tactic) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.test "(5 root)" state5.rootExpr?.isSome
|
||||
where
|
||||
interiorGoal (free: List (String × String)) (target: String) (userName?: Option String := .none) :=
|
||||
let free := [("a", "Nat"), ("p", "Prop"), ("h", "p")] ++ free
|
||||
buildGoal free target userName?
|
||||
|
||||
def test_nat_zero_add: TestM Unit := do
|
||||
let state? ← startProof (.expr "∀ (n: Nat), n + 0 = n")
|
||||
let state0 ← match state? with
|
||||
|
@ -795,8 +718,6 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
|
|||
("Or.comm", test_or_comm),
|
||||
("conv", test_conv),
|
||||
("calc", test_calc),
|
||||
("let via assign", test_let false),
|
||||
("let via tryLet", test_let true),
|
||||
("Nat.zero_add", test_nat_zero_add),
|
||||
("Nat.zero_add alt", test_nat_zero_add_alt),
|
||||
]
|
||||
|
|
|
@ -162,12 +162,105 @@ def test_proof_have : TestT Elab.TermElabM Unit := do
|
|||
|
||||
addTest $ LSpec.check "(4 root)" state4.rootExpr?.isSome
|
||||
|
||||
def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
|
||||
let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))"
|
||||
let state0 ← GoalState.create rootExpr
|
||||
let tactic := "intro a p h"
|
||||
let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check tactic ((← state1.serializeGoals).map (·.devolatilize) =
|
||||
#[{
|
||||
target := { pp? := .some mainTarget },
|
||||
vars := interiorVars,
|
||||
}])
|
||||
|
||||
let letType := "Nat"
|
||||
let expr := s!"let b: {letType} := _; _"
|
||||
let result2 ← match specialized with
|
||||
| true => state1.tryLet (goalId := 0) (binderName := "b") (type := letType)
|
||||
| false => state1.tryAssign (goalId := 0) (expr := expr)
|
||||
let state2 ← match result2 with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
let serializedState2 ← state2.serializeGoals
|
||||
let letBindName := if specialized then "b" else "_1"
|
||||
addTest $ LSpec.check expr (serializedState2.map (·.devolatilize) =
|
||||
#[{
|
||||
target := { pp? := .some letType },
|
||||
vars := interiorVars,
|
||||
userName? := .some letBindName
|
||||
},
|
||||
{
|
||||
target := { pp? := .some mainTarget },
|
||||
vars := interiorVars ++ #[{
|
||||
userName := "b",
|
||||
type? := .some { pp? := .some letType },
|
||||
value? := .some { pp? := .some s!"?{letBindName}" },
|
||||
}],
|
||||
userName? := if specialized then .none else .some "_2",
|
||||
}
|
||||
])
|
||||
|
||||
let tactic := "exact 1"
|
||||
let state3 ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check tactic ((← state3.serializeGoals).map (·.devolatilize) = #[])
|
||||
|
||||
let state3r ← match state3.continue state2 with
|
||||
| .error msg => do
|
||||
addTest $ assertUnreachable $ msg
|
||||
return ()
|
||||
| .ok state => pure state
|
||||
addTest $ LSpec.check "(continue)" ((← state3r.serializeGoals).map (·.devolatilize) =
|
||||
#[
|
||||
{
|
||||
target := { pp? := .some mainTarget },
|
||||
vars := interiorVars ++ #[{
|
||||
userName := "b",
|
||||
type? := .some { pp? := .some "Nat" },
|
||||
value? := .some { pp? := .some "1" },
|
||||
}],
|
||||
userName? := if specialized then .none else .some "_2",
|
||||
}
|
||||
])
|
||||
|
||||
let tactic := "exact h"
|
||||
match ← state3r.tryTactic (goalId := 0) (tactic := tactic) with
|
||||
| .failure #[message] =>
|
||||
addTest $ LSpec.check tactic (message = s!"type mismatch\n h\nhas type\n a : Prop\nbut is expected to have type\n {mainTarget} : Prop")
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
|
||||
let tactic := "exact Or.inl (Or.inl h)"
|
||||
let state4 ← match ← state3r.tryTactic (goalId := 0) (tactic := tactic) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.test "(4 root)" state4.rootExpr?.isSome
|
||||
where
|
||||
mainTarget := "(a ∨ p) ∨ a ∨ p"
|
||||
interiorVars: Array Protocol.Variable := #[
|
||||
{ userName := "a", type? := .some { pp? := .some "Prop" }, },
|
||||
{ userName := "p", type? := .some { pp? := .some "Prop" }, },
|
||||
{ userName := "h", type? := .some { pp? := .some "a" }, }
|
||||
]
|
||||
|
||||
def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
|
||||
[
|
||||
("eval", test_eval),
|
||||
("Proof eval", test_proof_eval),
|
||||
("Proof have", test_proof_have),
|
||||
("let via assign", test_let false),
|
||||
("let via tryLet", test_let true),
|
||||
] |>.map (λ (name, t) => (name, runTestTermElabM env t))
|
||||
|
||||
end Pantograph.Test.Tactic.Prograde
|
||||
|
|
Loading…
Reference in New Issue