feat: Prograde tactics #83
|
@ -125,7 +125,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
|
|||
pure ( Except.ok (← goalAssign goalState args.goalId expr))
|
||||
| .none, .none, .some type, .none, .none => do
|
||||
let binderName := args.binderName?.getD ""
|
||||
pure ( Except.ok (← goalHave goalState args.goalId binderName type))
|
||||
pure ( Except.ok (← goalState.tryHave args.goalId binderName type))
|
||||
| .none, .none, .none, .some pred, .none => do
|
||||
pure ( Except.ok (← goalCalc goalState args.goalId pred))
|
||||
| .none, .none, .none, .none, .some true => do
|
||||
|
|
|
@ -2,7 +2,7 @@
|
|||
import Pantograph.Protocol
|
||||
import Pantograph.Compile.Frontend
|
||||
import Pantograph.Compile.Elab
|
||||
|
||||
import Pantograph.Compile.Parse
|
||||
|
||||
open Lean
|
||||
|
||||
|
|
|
@ -0,0 +1,14 @@
|
|||
import Lean
|
||||
|
||||
open Lean
|
||||
|
||||
namespace Pantograph.Compile
|
||||
|
||||
def parseTermM [Monad m] [MonadEnv m] (s: String): m (Except String Syntax) := do
|
||||
return Parser.runParserCategory
|
||||
(env := ← MonadEnv.getEnv)
|
||||
(catName := `term)
|
||||
(input := s)
|
||||
(fileName := "<stdin>")
|
||||
|
||||
end Pantograph.Compile
|
|
@ -5,6 +5,7 @@ All the functions starting with `try` resume their inner monadic state.
|
|||
-/
|
||||
import Pantograph.Protocol
|
||||
import Pantograph.Tactic
|
||||
import Pantograph.Compile.Parse
|
||||
import Lean
|
||||
|
||||
|
||||
|
@ -21,8 +22,6 @@ structure GoalState where
|
|||
|
||||
-- The root hole which is the search target
|
||||
root: MVarId
|
||||
-- New metavariables acquired in this state
|
||||
newMVars: SSet MVarId
|
||||
|
||||
-- Parent state metavariable source
|
||||
parentMVar?: Option MVarId
|
||||
|
@ -47,7 +46,6 @@ protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do
|
|||
return {
|
||||
root,
|
||||
savedState,
|
||||
newMVars := SSet.insert .empty root,
|
||||
parentMVar? := .none,
|
||||
}
|
||||
protected def GoalState.isConv (state: GoalState): Bool :=
|
||||
|
@ -88,15 +86,6 @@ private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tac
|
|||
Elab.Tactic.setGoals [goal]
|
||||
|
||||
|
||||
private def newMVarSet (mctxOld: @&MetavarContext) (mctxNew: @&MetavarContext): SSet MVarId :=
|
||||
mctxNew.decls.foldl (fun acc mvarId mvarDecl =>
|
||||
if let .some prevMVarDecl := mctxOld.decls.find? mvarId then
|
||||
assert! prevMVarDecl.type == mvarDecl.type
|
||||
acc
|
||||
else
|
||||
acc.insert mvarId
|
||||
) SSet.empty
|
||||
|
||||
protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState := do
|
||||
let goal ← state.savedState.tactic.goals.get? goalId
|
||||
return {
|
||||
|
@ -165,6 +154,20 @@ protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvar: MVarId)
|
|||
|
||||
--- Tactic execution functions ---
|
||||
|
||||
protected def GoalState.step (state: GoalState) (mvarId: MVarId) (tacticM: Elab.Tactic.TacticM Unit)
|
||||
: Elab.TermElabM GoalState := do
|
||||
unless (← getMCtx).decls.contains mvarId do
|
||||
throwError s!"MVarId is not in context: {mvarId.name}"
|
||||
mvarId.checkNotAssigned `GoalState.step
|
||||
let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [mvarId] }
|
||||
let nextElabState ← MonadBacktrack.saveState
|
||||
return {
|
||||
state with
|
||||
savedState := { term := nextElabState, tactic := newGoals },
|
||||
parentMVar? := .some mvarId,
|
||||
calcPrevRhs? := .none,
|
||||
}
|
||||
|
||||
/-- Response for executing a tactic -/
|
||||
inductive TacticResult where
|
||||
-- Goes to next state
|
||||
|
@ -179,35 +182,21 @@ inductive TacticResult where
|
|||
| invalidAction (message: String)
|
||||
|
||||
/-- Executes a `TacticM` monads on this `GoalState`, collecting the errors as necessary -/
|
||||
protected def GoalState.executeTactic (state: GoalState) (goalId: Nat) (tacticM: Elab.Tactic.TacticM Unit):
|
||||
protected def GoalState.tryTacticM (state: GoalState) (goalId: Nat) (tacticM: Elab.Tactic.TacticM Unit):
|
||||
Elab.TermElabM TacticResult := do
|
||||
state.restoreElabM
|
||||
let goal ← match state.savedState.tactic.goals.get? goalId with
|
||||
let mvarId ← match state.savedState.tactic.goals.get? goalId with
|
||||
| .some goal => pure $ goal
|
||||
| .none => return .indexError goalId
|
||||
goal.checkNotAssigned `GoalState.executeTactic
|
||||
try
|
||||
let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
|
||||
if (← getThe Core.State).messages.hasErrors then
|
||||
let messages := (← getThe Core.State).messages.toArray
|
||||
let errors ← (messages.map (·.data)).mapM fun md => md.toString
|
||||
return .failure errors
|
||||
let nextElabState ← MonadBacktrack.saveState
|
||||
let nextMCtx := nextElabState.meta.meta.mctx
|
||||
let prevMCtx := state.mctx
|
||||
return .success {
|
||||
state with
|
||||
savedState := { term := nextElabState, tactic := newGoals },
|
||||
newMVars := newMVarSet prevMCtx nextMCtx,
|
||||
parentMVar? := .some goal,
|
||||
calcPrevRhs? := .none,
|
||||
}
|
||||
let nextState ← state.step mvarId tacticM
|
||||
return .success nextState
|
||||
catch exception =>
|
||||
return .failure #[← exception.toMessageData.toString]
|
||||
|
||||
/-- Execute a string tactic on given state -/
|
||||
protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: String):
|
||||
Elab.TermElabM TacticResult := do
|
||||
state.restoreElabM
|
||||
let tactic ← match Parser.runParserCategory
|
||||
(env := ← MonadEnv.getEnv)
|
||||
(catName := if state.isConv then `conv else `tactic)
|
||||
|
@ -215,7 +204,7 @@ protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: Stri
|
|||
(fileName := filename) with
|
||||
| .ok stx => pure $ stx
|
||||
| .error error => return .parseError error
|
||||
state.executeTactic goalId $ Elab.Tactic.evalTactic tactic
|
||||
state.tryTacticM goalId $ Elab.Tactic.evalTactic tactic
|
||||
|
||||
protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String):
|
||||
Elab.TermElabM TacticResult := do
|
||||
|
@ -227,103 +216,21 @@ protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String
|
|||
(fileName := filename) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => return .parseError error
|
||||
state.executeTactic goalId $ Tactic.evalAssign expr
|
||||
state.tryTacticM goalId $ Tactic.evalAssign expr
|
||||
|
||||
-- Specialized Tactics
|
||||
|
||||
protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String):
|
||||
Elab.TermElabM TacticResult := do
|
||||
state.restoreElabM
|
||||
let goal ← match state.savedState.tactic.goals.get? goalId with
|
||||
| .some goal => pure goal
|
||||
| .none => return .indexError goalId
|
||||
goal.checkNotAssigned `GoalState.tryHave
|
||||
let type ← match Parser.runParserCategory
|
||||
(env := state.env)
|
||||
(catName := `term)
|
||||
(input := type)
|
||||
(fileName := filename) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => return .parseError error
|
||||
let binderName := binderName.toName
|
||||
try
|
||||
-- Implemented similarly to the intro tactic
|
||||
let nextGoals: List MVarId ← goal.withContext do
|
||||
let type ← Elab.Term.elabType (stx := type)
|
||||
let lctx ← MonadLCtx.getLCtx
|
||||
|
||||
-- The branch goal inherits the same context, but with a different type
|
||||
let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type
|
||||
|
||||
-- Create the context for the `upstream` goal
|
||||
let fvarId ← mkFreshFVarId
|
||||
let lctxUpstream := lctx.mkLocalDecl fvarId binderName type
|
||||
let fvar := mkFVar fvarId
|
||||
let mvarUpstream ←
|
||||
withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do
|
||||
Meta.withNewLocalInstances #[fvar] 0 do
|
||||
let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
|
||||
(← goal.getType) (kind := MetavarKind.synthetic) (userName := .anonymous)
|
||||
let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream
|
||||
goal.assign expr
|
||||
pure mvarUpstream
|
||||
|
||||
pure [mvarBranch.mvarId!, mvarUpstream.mvarId!]
|
||||
return .success {
|
||||
root := state.root,
|
||||
savedState := {
|
||||
term := ← MonadBacktrack.saveState,
|
||||
tactic := { goals := nextGoals }
|
||||
},
|
||||
newMVars := nextGoals.toSSet,
|
||||
parentMVar? := .some goal,
|
||||
calcPrevRhs? := .none
|
||||
}
|
||||
catch exception =>
|
||||
return .failure #[← exception.toMessageData.toString]
|
||||
protected def GoalState.tryLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String):
|
||||
Elab.TermElabM TacticResult := do
|
||||
state.restoreElabM
|
||||
let goal ← match state.savedState.tactic.goals.get? goalId with
|
||||
| .some goal => pure goal
|
||||
| .none => return .indexError goalId
|
||||
goal.checkNotAssigned `GoalState.tryLet
|
||||
let type ← match Parser.runParserCategory
|
||||
(env := state.env)
|
||||
(env := ← MonadEnv.getEnv)
|
||||
(catName := `term)
|
||||
(input := type)
|
||||
(fileName := filename) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => return .parseError error
|
||||
let binderName := binderName.toName
|
||||
try
|
||||
-- Implemented similarly to the intro tactic
|
||||
let nextGoals: List MVarId ← goal.withContext do
|
||||
let type ← Elab.Term.elabType (stx := type)
|
||||
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 upstreamType := .letE binderName type mvarBranch (← goal.getType) false
|
||||
let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
|
||||
upstreamType (kind := MetavarKind.synthetic) (userName := (← goal.getTag))
|
||||
|
||||
goal.assign mvarUpstream
|
||||
|
||||
pure [mvarBranch.mvarId!, mvarUpstream.mvarId!]
|
||||
return .success {
|
||||
root := state.root,
|
||||
savedState := {
|
||||
term := ← MonadBacktrack.saveState,
|
||||
tactic := { goals := nextGoals }
|
||||
},
|
||||
newMVars := nextGoals.toSSet,
|
||||
parentMVar? := .some goal,
|
||||
calcPrevRhs? := .none
|
||||
}
|
||||
catch exception =>
|
||||
return .failure #[← exception.toMessageData.toString]
|
||||
state.tryTacticM goalId $ Tactic.evalLet binderName.toName type
|
||||
|
||||
/-- Enter conv tactic mode -/
|
||||
protected def GoalState.conv (state: GoalState) (goalId: Nat):
|
||||
|
@ -345,12 +252,9 @@ protected def GoalState.conv (state: GoalState) (goalId: Nat):
|
|||
return (← MonadBacktrack.saveState, convMVar)
|
||||
try
|
||||
let (nextSavedState, convRhs) ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
|
||||
let prevMCtx := state.mctx
|
||||
let nextMCtx := nextSavedState.term.meta.meta.mctx
|
||||
return .success {
|
||||
root := state.root,
|
||||
savedState := nextSavedState
|
||||
newMVars := newMVarSet prevMCtx nextMCtx,
|
||||
parentMVar? := .some goal,
|
||||
convMVar? := .some (convRhs, goal),
|
||||
calcPrevRhs? := .none
|
||||
|
@ -384,12 +288,9 @@ protected def GoalState.convExit (state: GoalState):
|
|||
MonadBacktrack.saveState
|
||||
try
|
||||
let nextSavedState ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
|
||||
let nextMCtx := nextSavedState.term.meta.meta.mctx
|
||||
let prevMCtx := state.savedState.term.meta.meta.mctx
|
||||
return .success {
|
||||
root := state.root,
|
||||
savedState := nextSavedState
|
||||
newMVars := newMVarSet prevMCtx nextMCtx,
|
||||
parentMVar? := .some convGoal,
|
||||
convMVar? := .none
|
||||
calcPrevRhs? := .none
|
||||
|
@ -469,7 +370,6 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
|
|||
term := ← MonadBacktrack.saveState,
|
||||
tactic := { goals },
|
||||
},
|
||||
newMVars := goals.toSSet,
|
||||
parentMVar? := .some goal,
|
||||
calcPrevRhs?
|
||||
}
|
||||
|
@ -480,24 +380,16 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
|
|||
protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String):
|
||||
Elab.TermElabM TacticResult := do
|
||||
state.restoreElabM
|
||||
let recursor ← match Parser.runParserCategory
|
||||
(env := state.env)
|
||||
(catName := `term)
|
||||
(input := recursor)
|
||||
(fileName := filename) with
|
||||
let recursor ← match (← Compile.parseTermM recursor) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => return .parseError error
|
||||
state.executeTactic goalId (tacticM := Tactic.motivatedApply recursor)
|
||||
state.tryTacticM goalId (tacticM := Tactic.evalMotivatedApply recursor)
|
||||
protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: String):
|
||||
Elab.TermElabM TacticResult := do
|
||||
state.restoreElabM
|
||||
let recursor ← match Parser.runParserCategory
|
||||
(env := state.env)
|
||||
(catName := `term)
|
||||
(input := eq)
|
||||
(fileName := filename) with
|
||||
let eq ← match (← Compile.parseTermM eq) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => return .parseError error
|
||||
state.executeTactic goalId (tacticM := Tactic.noConfuse recursor)
|
||||
state.tryTacticM goalId (tacticM := Tactic.evalNoConfuse eq)
|
||||
|
||||
end Pantograph
|
||||
|
|
|
@ -162,8 +162,21 @@ def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): CoreM TacticRe
|
|||
def goalAssign (state: GoalState) (goalId: Nat) (expr: String): CoreM TacticResult :=
|
||||
runTermElabM <| state.tryAssign goalId expr
|
||||
@[export pantograph_goal_have_m]
|
||||
def goalHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult :=
|
||||
runTermElabM <| state.tryHave goalId binderName type
|
||||
protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult := do
|
||||
let type ← match (← Compile.parseTermM type) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => return .parseError error
|
||||
runTermElabM do
|
||||
state.restoreElabM
|
||||
state.tryTacticM goalId $ Tactic.evalHave binderName.toName type
|
||||
@[export pantograph_goal_try_define_m]
|
||||
protected def GoalState.tryDefine (state: GoalState) (goalId: Nat) (binderName: String) (expr: String): CoreM TacticResult := do
|
||||
let expr ← match (← Compile.parseTermM expr) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => return .parseError error
|
||||
runTermElabM do
|
||||
state.restoreElabM
|
||||
state.tryTacticM goalId (Tactic.evalDefine binderName.toName expr)
|
||||
@[export pantograph_goal_let_m]
|
||||
def goalLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult :=
|
||||
runTermElabM <| state.tryLet goalId binderName type
|
||||
|
@ -179,11 +192,5 @@ def goalCalc (state: GoalState) (goalId: Nat) (pred: String): CoreM TacticResult
|
|||
@[export pantograph_goal_focus]
|
||||
def goalFocus (state: GoalState) (goalId: Nat): Option GoalState :=
|
||||
state.focus goalId
|
||||
@[export pantograph_goal_motivated_apply_m]
|
||||
def goalMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): CoreM TacticResult :=
|
||||
runTermElabM <| state.tryMotivatedApply goalId recursor
|
||||
@[export pantograph_goal_no_confuse_m]
|
||||
def goalNoConfuse (state: GoalState) (goalId: Nat) (eq: String): CoreM TacticResult :=
|
||||
runTermElabM <| state.tryNoConfuse goalId eq
|
||||
|
||||
end Pantograph
|
||||
|
|
|
@ -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: Bool := false
|
||||
type?: Option Expression := .none
|
||||
value?: Option Expression := .none
|
||||
deriving Lean.ToJson
|
||||
|
|
|
@ -200,7 +200,7 @@ def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.
|
|||
|
||||
|
||||
/-- Adapted from ppGoal -/
|
||||
def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
|
||||
def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl := .none)
|
||||
: MetaM Protocol.Goal := do
|
||||
-- Options for printing; See Meta.ppGoal for details
|
||||
let showLetValues := true
|
||||
|
@ -215,11 +215,13 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
|
|||
return {
|
||||
name := ofName fvarId.name,
|
||||
userName:= ofName userName.simpMacroScopes,
|
||||
isInaccessible := userName.isInaccessibleUserName
|
||||
}
|
||||
| .ldecl _ fvarId userName _ _ _ _ => do
|
||||
return {
|
||||
name := ofName fvarId.name,
|
||||
userName := toString userName.simpMacroScopes,
|
||||
isInaccessible := userName.isInaccessibleUserName
|
||||
}
|
||||
let ppVar (localDecl : LocalDecl) : MetaM Protocol.Variable := do
|
||||
match localDecl with
|
||||
|
@ -229,7 +231,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
|
|||
return {
|
||||
name := ofName fvarId.name,
|
||||
userName:= ofName userName,
|
||||
isInaccessible? := .some userName.isInaccessibleUserName
|
||||
isInaccessible := userName.isInaccessibleUserName
|
||||
type? := .some (← serializeExpression options type)
|
||||
}
|
||||
| .ldecl _ fvarId userName type val _ _ => do
|
||||
|
@ -243,7 +245,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
|
|||
return {
|
||||
name := ofName fvarId.name,
|
||||
userName:= ofName userName,
|
||||
isInaccessible? := .some userName.isInaccessibleUserName
|
||||
isInaccessible := userName.isInaccessibleUserName
|
||||
type? := .some (← serializeExpression options type)
|
||||
value? := value?
|
||||
}
|
||||
|
@ -287,7 +289,8 @@ protected def GoalState.serializeGoals
|
|||
|
||||
/-- Print the metavariables in a readable format -/
|
||||
@[export pantograph_goal_state_diag_m]
|
||||
protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState := .none) (options: Protocol.GoalDiag := {}): MetaM String := do
|
||||
protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState := .none) (options: Protocol.GoalDiag := {}): CoreM String := do
|
||||
let metaM: MetaM String := do
|
||||
goalState.restoreMetaM
|
||||
let savedState := goalState.savedState
|
||||
let goals := savedState.tactic.goals
|
||||
|
@ -310,6 +313,7 @@ protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState :
|
|||
printMVar pref mvarId decl
|
||||
)
|
||||
pure $ result ++ "\n" ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join)
|
||||
metaM.run' {}
|
||||
where
|
||||
printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM String := mvarId.withContext do
|
||||
let resultFVars: List String ←
|
||||
|
|
|
@ -1,5 +1,5 @@
|
|||
|
||||
import Pantograph.Tactic.Assign
|
||||
import Pantograph.Tactic.Congruence
|
||||
import Pantograph.Tactic.MotivatedApply
|
||||
import Pantograph.Tactic.NoConfuse
|
||||
import Pantograph.Tactic.Prograde
|
||||
|
|
|
@ -4,15 +4,8 @@ open Lean
|
|||
|
||||
namespace Pantograph.Tactic
|
||||
|
||||
private def newMVarSet (mctxOld: @&MetavarContext) (mctxNew: @&MetavarContext): SSet MVarId :=
|
||||
mctxNew.decls.foldl (fun acc mvarId mvarDecl =>
|
||||
if let .some prevMVarDecl := mctxOld.decls.find? mvarId then
|
||||
assert! prevMVarDecl.type == mvarDecl.type
|
||||
acc
|
||||
else
|
||||
acc.insert mvarId
|
||||
) SSet.empty
|
||||
def assign (goal: MVarId) (expr: Expr): MetaM (List MVarId) := do
|
||||
/-- WARNING: This should be used with a function like `elabTermWithHoles` that properly collects the mvar information from `expr`. -/
|
||||
def assign (goal: MVarId) (expr: Expr) (nextGoals: List MVarId): MetaM (List MVarId) := do
|
||||
goal.checkNotAssigned `Pantograph.Tactic.assign
|
||||
|
||||
-- This run of the unifier is critical in resolving mvars in passing
|
||||
|
@ -20,15 +13,18 @@ def assign (goal: MVarId) (expr: Expr): MetaM (List MVarId) := do
|
|||
let goalType ← goal.getType
|
||||
unless ← Meta.isDefEq goalType exprType do
|
||||
throwError s!"{← Meta.ppExpr expr} : {← Meta.ppExpr exprType} ≠ {← Meta.ppExpr goalType}"
|
||||
|
||||
let nextGoals ← Meta.getMVars expr
|
||||
goal.assign expr
|
||||
nextGoals.toList.filterM (not <$> ·.isAssigned)
|
||||
nextGoals.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 goal ← Elab.Tactic.getMainGoal
|
||||
goal.checkNotAssigned `Pantograph.Tactic.evalAssign
|
||||
let (expr, nextGoals) ← Elab.Tactic.elabTermWithHoles stx
|
||||
(expectedType? := .some target)
|
||||
(tagSuffix := .anonymous )
|
||||
(allowNaturalHoles := true)
|
||||
goal.assign expr
|
||||
Elab.Tactic.setGoals nextGoals
|
||||
|
||||
|
||||
|
|
|
@ -4,12 +4,12 @@ open Lean
|
|||
|
||||
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
|
||||
def congruenceArg (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
|
||||
mvarId.checkNotAssigned `Pantograph.Tactic.congruenceArg
|
||||
let target ← mvarId.getType
|
||||
let .some (β, _, _) := target.eq? | throwError "Goal is not an Eq"
|
||||
let userName := (← mvarId.getDecl).userName
|
||||
|
||||
let nextGoals ← goal.withContext do
|
||||
let u ← Meta.mkFreshLevelMVar
|
||||
let α ← Meta.mkFreshExprMVar (.some $ mkSort u)
|
||||
.natural (userName := userName ++ `α)
|
||||
|
@ -21,19 +21,23 @@ def congruenceArg: Elab.Tactic.TacticM Unit := do
|
|||
.synthetic (userName := userName ++ `a₂)
|
||||
let h ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq a₁ a₂)
|
||||
.synthetic (userName := userName ++ `h)
|
||||
let conduitType ← Meta.mkEq (← Meta.mkEq (.app f a₁) (.app f a₂)) (← goal.getType)
|
||||
let conduitType ← Meta.mkEq (← Meta.mkEq (.app f a₁) (.app f a₂)) target
|
||||
let conduit ← Meta.mkFreshExprMVar conduitType
|
||||
.synthetic (userName := userName ++ `conduit)
|
||||
goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrArg f h)
|
||||
return [α, a₁, a₂, f, h, conduit]
|
||||
Elab.Tactic.setGoals <| nextGoals.map (·.mvarId!)
|
||||
mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrArg f h)
|
||||
let result := [α, a₁, a₂, f, h, conduit]
|
||||
return result.map (·.mvarId!)
|
||||
|
||||
def congruenceFun: Elab.Tactic.TacticM Unit := do
|
||||
def evalCongruenceArg: 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 nextGoals ← congruenceArg goal
|
||||
Elab.Tactic.setGoals nextGoals
|
||||
|
||||
let nextGoals ← goal.withContext do
|
||||
def congruenceFun (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
|
||||
mvarId.checkNotAssigned `Pantograph.Tactic.congruenceFun
|
||||
let target ← mvarId.getType
|
||||
let .some (β, _, _) := 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 ++ `α)
|
||||
|
@ -46,19 +50,23 @@ def congruenceFun: Elab.Tactic.TacticM Unit := do
|
|||
.synthetic (userName := userName ++ `a)
|
||||
let h ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq f₁ f₂)
|
||||
.synthetic (userName := userName ++ `h)
|
||||
let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a) (.app f₂ a)) (← goal.getType)
|
||||
let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a) (.app f₂ a)) target
|
||||
let conduit ← Meta.mkFreshExprMVar conduitType
|
||||
.synthetic (userName := userName ++ `conduit)
|
||||
goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrFun h a)
|
||||
return [α, f₁, f₂, h, a, conduit]
|
||||
Elab.Tactic.setGoals <| nextGoals.map (·.mvarId!)
|
||||
mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrFun h a)
|
||||
let result := [α, f₁, f₂, h, a, conduit]
|
||||
return result.map (·.mvarId!)
|
||||
|
||||
def congruence: Elab.Tactic.TacticM Unit := do
|
||||
def evalCongruenceFun: 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 nextGoals ← congruenceFun goal
|
||||
Elab.Tactic.setGoals nextGoals
|
||||
|
||||
let nextGoals ← goal.withContext do
|
||||
def congruence (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
|
||||
mvarId.checkNotAssigned `Pantograph.Tactic.congruence
|
||||
let target ← mvarId.getType
|
||||
let .some (β, _, _) := 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 ++ `α)
|
||||
|
@ -75,11 +83,16 @@ def congruence: Elab.Tactic.TacticM Unit := do
|
|||
.synthetic (userName := userName ++ `h₁)
|
||||
let h₂ ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq a₁ a₂)
|
||||
.synthetic (userName := userName ++ `h₂)
|
||||
let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a₁) (.app f₂ a₂)) (← goal.getType)
|
||||
let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a₁) (.app f₂ a₂)) target
|
||||
let conduit ← Meta.mkFreshExprMVar conduitType
|
||||
.synthetic (userName := userName ++ `conduit)
|
||||
goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongr h₁ h₂)
|
||||
return [α, f₁, f₂, a₁, a₂, h₁, h₂, conduit]
|
||||
Elab.Tactic.setGoals <| nextGoals.map (·.mvarId!)
|
||||
mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongr h₁ h₂)
|
||||
let result := [α, f₁, f₂, a₁, a₂, h₁, h₂, conduit]
|
||||
return result.map (·.mvarId!)
|
||||
|
||||
def evalCongruence: Elab.Tactic.TacticM Unit := do
|
||||
let goal ← Elab.Tactic.getMainGoal
|
||||
let nextGoals ← congruence goal
|
||||
Elab.Tactic.setGoals nextGoals
|
||||
|
||||
end Pantograph.Tactic
|
||||
|
|
|
@ -62,13 +62,10 @@ def collectMotiveArguments (forallBody: Expr): SSet Nat :=
|
|||
| _ => SSet.empty
|
||||
|
||||
/-- Applies a symbol of the type `∀ (motive: α → Sort u) (a: α)..., (motive α)` -/
|
||||
def motivatedApply: Elab.Tactic.Tactic := λ stx => do
|
||||
let goal ← Elab.Tactic.getMainGoal
|
||||
let nextGoals: List MVarId ← goal.withContext do
|
||||
let recursor ← Elab.Term.elabTerm (stx := stx) .none
|
||||
def motivatedApply (mvarId: MVarId) (recursor: Expr) : MetaM (Array Meta.InductionSubgoal) := mvarId.withContext do
|
||||
mvarId.checkNotAssigned `Pantograph.Tactic.motivatedApply
|
||||
let recursorType ← Meta.inferType recursor
|
||||
|
||||
let resultant ← goal.getType
|
||||
let resultant ← mvarId.getType
|
||||
|
||||
let info ← match getRecursorInformation recursorType with
|
||||
| .some info => pure info
|
||||
|
@ -95,11 +92,14 @@ def motivatedApply: Elab.Tactic.Tactic := λ stx => do
|
|||
-- 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)
|
||||
goal.assign $ ← Meta.mkEqMP goalConduit (mkAppN recursor newMVars)
|
||||
mvarId.assign $ ← Meta.mkEqMP goalConduit (mkAppN recursor newMVars)
|
||||
newMVars := newMVars ++ [goalConduit]
|
||||
|
||||
let nextGoals := newMVars.toList.map (·.mvarId!)
|
||||
pure nextGoals
|
||||
Elab.Tactic.setGoals nextGoals
|
||||
return newMVars.map (λ mvar => { mvarId := mvar.mvarId!})
|
||||
|
||||
def evalMotivatedApply : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
|
||||
let recursor ← Elab.Term.elabTerm (stx := stx) .none
|
||||
let nextGoals ← motivatedApply (← Elab.Tactic.getMainGoal) recursor
|
||||
Elab.Tactic.setGoals $ nextGoals.toList.map (·.mvarId)
|
||||
|
||||
end Pantograph.Tactic
|
||||
|
|
|
@ -4,15 +4,19 @@ open Lean
|
|||
|
||||
namespace Pantograph.Tactic
|
||||
|
||||
def noConfuse: Elab.Tactic.Tactic := λ stx => do
|
||||
let goal ← Elab.Tactic.getMainGoal
|
||||
goal.withContext do
|
||||
let absurd ← Elab.Term.elabTerm (stx := stx) .none
|
||||
let noConfusion ← Meta.mkNoConfusion (target := ← goal.getType) (h := absurd)
|
||||
def noConfuse (mvarId: MVarId) (h: Expr): MetaM Unit := mvarId.withContext do
|
||||
mvarId.checkNotAssigned `Pantograph.Tactic.noConfuse
|
||||
let target ← mvarId.getType
|
||||
let noConfusion ← Meta.mkNoConfusion (target := target) (h := h)
|
||||
|
||||
unless ← Meta.isDefEq (← Meta.inferType noConfusion) (← goal.getType) do
|
||||
throwError "invalid noConfuse call: The resultant type {← Meta.ppExpr $ ← Meta.inferType noConfusion} cannot be unified with {← Meta.ppExpr $ ← goal.getType}"
|
||||
goal.assign noConfusion
|
||||
unless ← Meta.isDefEq (← Meta.inferType noConfusion) target do
|
||||
throwError "invalid noConfuse call: The resultant type {← Meta.ppExpr $ ← Meta.inferType noConfusion} cannot be unified with {← Meta.ppExpr target}"
|
||||
mvarId.assign noConfusion
|
||||
|
||||
def evalNoConfuse: Elab.Tactic.Tactic := λ stx => do
|
||||
let goal ← Elab.Tactic.getMainGoal
|
||||
let h ← goal.withContext $ Elab.Term.elabTerm (stx := stx) .none
|
||||
noConfuse goal h
|
||||
Elab.Tactic.setGoals []
|
||||
|
||||
end Pantograph.Tactic
|
||||
|
|
|
@ -0,0 +1,87 @@
|
|||
/- Prograde (forward) reasoning tactics -/
|
||||
|
||||
import Lean
|
||||
open Lean
|
||||
|
||||
namespace Pantograph.Tactic
|
||||
|
||||
/-- Introduces a fvar to the current mvar -/
|
||||
def define (mvarId: MVarId) (binderName: Name) (expr: Expr): MetaM (FVarId × MVarId) := mvarId.withContext do
|
||||
mvarId.checkNotAssigned `Pantograph.Tactic.define
|
||||
let type ← Meta.inferType expr
|
||||
|
||||
Meta.withLetDecl binderName type expr λ fvar => do
|
||||
let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
|
||||
(← mvarId.getType) (kind := MetavarKind.synthetic) (userName := .anonymous)
|
||||
mvarId.assign mvarUpstream
|
||||
pure (fvar.fvarId!, mvarUpstream.mvarId!)
|
||||
|
||||
def evalDefine (binderName: Name) (expr: Syntax): Elab.Tactic.TacticM Unit := do
|
||||
let goal ← Elab.Tactic.getMainGoal
|
||||
let expr ← goal.withContext $ Elab.Term.elabTerm (stx := expr) (expectedType? := .none)
|
||||
let (_, mvarId) ← define goal binderName expr
|
||||
Elab.Tactic.setGoals [mvarId]
|
||||
|
||||
structure BranchResult where
|
||||
fvarId?: Option FVarId := .none
|
||||
branch: MVarId
|
||||
main: MVarId
|
||||
|
||||
def «have» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResult := mvarId.withContext do
|
||||
mvarId.checkNotAssigned `Pantograph.Tactic.have
|
||||
let lctx ← MonadLCtx.getLCtx
|
||||
-- The branch goal inherits the same context, but with a different type
|
||||
let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type
|
||||
|
||||
-- Create the context for the `upstream` goal
|
||||
let fvarId ← mkFreshFVarId
|
||||
let lctxUpstream := lctx.mkLocalDecl fvarId binderName type
|
||||
let mvarUpstream ←
|
||||
withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do
|
||||
Meta.withNewLocalInstances #[.fvar fvarId] 0 do
|
||||
let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
|
||||
(← mvarId.getType) (kind := MetavarKind.synthetic) (userName := ← mvarId.getTag)
|
||||
--let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream
|
||||
mvarId.assign mvarUpstream
|
||||
pure mvarUpstream
|
||||
|
||||
return {
|
||||
fvarId? := .some fvarId,
|
||||
branch := mvarBranch.mvarId!,
|
||||
main := mvarUpstream.mvarId!,
|
||||
}
|
||||
|
||||
def evalHave (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do
|
||||
let goal ← Elab.Tactic.getMainGoal
|
||||
let nextGoals: List MVarId ← goal.withContext do
|
||||
let type ← Elab.Term.elabType (stx := type)
|
||||
let result ← «have» goal binderName type
|
||||
pure [result.branch, result.main]
|
||||
Elab.Tactic.setGoals nextGoals
|
||||
|
||||
def «let» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResult := mvarId.withContext do
|
||||
mvarId.checkNotAssigned `Pantograph.Tactic.let
|
||||
let lctx ← MonadLCtx.getLCtx
|
||||
|
||||
-- The branch goal inherits the same context, but with a different type
|
||||
let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type (userName := binderName)
|
||||
|
||||
assert! ¬ type.hasLooseBVars
|
||||
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 {
|
||||
branch := mvarBranch.mvarId!,
|
||||
main := mvarUpstream.mvarId!,
|
||||
}
|
||||
|
||||
def evalLet (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do
|
||||
let goal ← Elab.Tactic.getMainGoal
|
||||
let type ← goal.withContext $ Elab.Term.elabType (stx := type)
|
||||
let result ← «let» goal binderName type
|
||||
Elab.Tactic.setGoals [result.branch, result.main]
|
||||
|
||||
end Pantograph.Tactic
|
|
@ -1,6 +1,7 @@
|
|||
import Pantograph.Goal
|
||||
import Pantograph.Library
|
||||
import Pantograph.Protocol
|
||||
import Pantograph.Condensed
|
||||
import Lean
|
||||
import LSpec
|
||||
|
||||
|
@ -10,12 +11,7 @@ namespace Pantograph
|
|||
|
||||
deriving instance Repr for Expr
|
||||
-- Use strict equality check for expressions
|
||||
--instance : BEq Expr := ⟨Expr.equal⟩
|
||||
instance (priority := 80) (x y : Expr) : LSpec.Testable (x.equal y) :=
|
||||
if h : Expr.equal x y then
|
||||
.isTrue h
|
||||
else
|
||||
.isFalse h $ s!"Expected to be equalaaa: '{x.dbgToString}' and '{y.dbgToString}'"
|
||||
instance : BEq Expr := ⟨Expr.equal⟩
|
||||
|
||||
def uniq (n: Nat): Name := .num (.str .anonymous "_uniq") n
|
||||
|
||||
|
@ -25,6 +21,7 @@ def Goal.devolatilizeVars (goal: Goal): Goal :=
|
|||
{
|
||||
goal with
|
||||
vars := goal.vars.map removeInternalAux,
|
||||
|
||||
}
|
||||
where removeInternalAux (v: Variable): Variable :=
|
||||
{
|
||||
|
@ -47,6 +44,24 @@ deriving instance DecidableEq, Repr for InteractionError
|
|||
deriving instance DecidableEq, Repr for Option
|
||||
end Protocol
|
||||
|
||||
namespace Condensed
|
||||
|
||||
deriving instance BEq, Repr for LocalDecl
|
||||
deriving instance BEq, Repr for Goal
|
||||
|
||||
protected def LocalDecl.devolatilize (decl: LocalDecl): LocalDecl :=
|
||||
{
|
||||
decl with fvarId := { name := .anonymous }
|
||||
}
|
||||
protected def Goal.devolatilize (goal: Goal): Goal :=
|
||||
{
|
||||
goal with
|
||||
mvarId := { name := .anonymous },
|
||||
context := goal.context.map LocalDecl.devolatilize
|
||||
}
|
||||
|
||||
end Condensed
|
||||
|
||||
def TacticResult.toString : TacticResult → String
|
||||
| .success state => s!".success ({state.goals.length} goals)"
|
||||
| .failure messages =>
|
||||
|
@ -73,11 +88,13 @@ def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq) (options: Array
|
|||
def runMetaMSeq (env: Environment) (metaM: MetaM LSpec.TestSeq): IO LSpec.TestSeq :=
|
||||
runCoreMSeq env metaM.run'
|
||||
def runTermElabMInMeta { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α :=
|
||||
termElabM.run' (ctx := Pantograph.Condensed.elabContext)
|
||||
termElabM.run' (ctx := Condensed.elabContext)
|
||||
def runTermElabMSeq (env: Environment) (termElabM: Elab.TermElabM LSpec.TestSeq): IO LSpec.TestSeq :=
|
||||
runMetaMSeq env $ termElabM.run' (ctx := Condensed.elabContext)
|
||||
|
||||
def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e
|
||||
|
||||
def parseSentence (s: String): MetaM Expr := do
|
||||
def parseSentence (s: String): Elab.TermElabM Expr := do
|
||||
let recursor ← match Parser.runParserCategory
|
||||
(env := ← MonadEnv.getEnv)
|
||||
(catName := `term)
|
||||
|
@ -85,7 +102,7 @@ def parseSentence (s: String): MetaM Expr := do
|
|||
(fileName := filename) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => throwError "Failed to parse: {error}"
|
||||
runTermElabMInMeta $ Elab.Term.elabTerm (stx := recursor) .none
|
||||
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] }
|
||||
|
@ -95,6 +112,35 @@ def mvarUserNameAndType (mvarId: MVarId): MetaM (Name × String) := do
|
|||
let t ← exprToStr (← mvarId.getType)
|
||||
return (name, t)
|
||||
|
||||
|
||||
-- Monadic testing
|
||||
|
||||
abbrev TestT := StateT LSpec.TestSeq
|
||||
|
||||
def addTest [Monad m] (test: LSpec.TestSeq): TestT m Unit := do
|
||||
set $ (← get) ++ test
|
||||
|
||||
def runTest [Monad m] (t: TestT m Unit): m LSpec.TestSeq :=
|
||||
Prod.snd <$> t.run LSpec.TestSeq.done
|
||||
|
||||
def runTestTermElabM (env: Environment) (t: TestT Elab.TermElabM Unit):
|
||||
IO LSpec.TestSeq :=
|
||||
runTermElabMSeq env $ runTest t
|
||||
|
||||
def cdeclOf (userName: Name) (type: Expr): Condensed.LocalDecl :=
|
||||
{ userName, type }
|
||||
|
||||
def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none):
|
||||
Protocol.Goal :=
|
||||
{
|
||||
userName?,
|
||||
target := { pp? := .some target},
|
||||
vars := (nameType.map fun x => ({
|
||||
userName := x.fst,
|
||||
type? := .some { pp? := .some x.snd },
|
||||
})).toArray
|
||||
}
|
||||
|
||||
end Test
|
||||
|
||||
end Pantograph
|
||||
|
|
|
@ -85,14 +85,14 @@ def test_tactic : IO LSpec.TestSeq :=
|
|||
let goal1: Protocol.Goal := {
|
||||
name := "_uniq.11",
|
||||
target := { pp? := .some "∀ (q : Prop), x ∨ q → q ∨ x" },
|
||||
vars := #[{ name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
|
||||
vars := #[{ name := "_uniq.10", userName := "x", type? := .some { pp? := .some "Prop" }}],
|
||||
}
|
||||
let goal2: Protocol.Goal := {
|
||||
name := "_uniq.17",
|
||||
target := { pp? := .some "x ∨ y → y ∨ x" },
|
||||
vars := #[
|
||||
{ name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }},
|
||||
{ name := "_uniq.16", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}
|
||||
{ name := "_uniq.10", userName := "x", type? := .some { pp? := .some "Prop" }},
|
||||
{ name := "_uniq.16", userName := "y", type? := .some { pp? := .some "Prop" }}
|
||||
],
|
||||
}
|
||||
subroutine_runner [
|
||||
|
|
|
@ -52,6 +52,7 @@ def main (args: List String) := do
|
|||
("Tactic/Congruence", Tactic.Congruence.suite env_default),
|
||||
("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default),
|
||||
("Tactic/No Confuse", Tactic.NoConfuse.suite env_default),
|
||||
("Tactic/Prograde", Tactic.Prograde.suite env_default),
|
||||
]
|
||||
let tests: List (String × IO LSpec.TestSeq) := suites.foldl (λ acc (name, suite) => acc ++ (addPrefix name suite)) []
|
||||
LSpec.lspecIO (← runTestGroup name_filter tests)
|
||||
|
|
|
@ -60,7 +60,6 @@ def buildGoal (nameType: List (String × String)) (target: String) (userName?: O
|
|||
vars := (nameType.map fun x => ({
|
||||
userName := x.fst,
|
||||
type? := .some { pp? := .some x.snd },
|
||||
isInaccessible? := .some false
|
||||
})).toArray
|
||||
}
|
||||
def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do
|
||||
|
@ -198,15 +197,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
|
||||
|
|
159
Test/Proofs.lean
159
Test/Proofs.lean
|
@ -58,7 +58,6 @@ def buildNamedGoal (name: String) (nameType: List (String × String)) (target: S
|
|||
vars := (nameType.map fun x => ({
|
||||
userName := x.fst,
|
||||
type? := .some { pp? := .some x.snd },
|
||||
isInaccessible? := .some false
|
||||
})).toArray
|
||||
}
|
||||
def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none):
|
||||
|
@ -69,7 +68,6 @@ def buildGoal (nameType: List (String × String)) (target: String) (userName?: O
|
|||
vars := (nameType.map fun x => ({
|
||||
userName := x.fst,
|
||||
type? := .some { pp? := .some x.snd },
|
||||
isInaccessible? := .some false
|
||||
})).toArray
|
||||
}
|
||||
def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do
|
||||
|
@ -175,7 +173,6 @@ 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)
|
||||
})).toArray
|
||||
}
|
||||
|
||||
|
@ -256,9 +253,9 @@ def test_or_comm: TestM Unit := do
|
|||
name := state1g0,
|
||||
target := { pp? := .some "q ∨ p" },
|
||||
vars := #[
|
||||
{ name := fvP, userName := "p", type? := .some { pp? := .some "Prop" }, isInaccessible? := .some false },
|
||||
{ name := fvQ, userName := "q", type? := .some { pp? := .some "Prop" }, isInaccessible? := .some false },
|
||||
{ name := fvH, userName := "h", type? := .some { pp? := .some "p ∨ q" }, isInaccessible? := .some false }
|
||||
{ name := fvP, userName := "p", type? := .some { pp? := .some "Prop" } },
|
||||
{ name := fvQ, userName := "q", type? := .some { pp? := .some "Prop" } },
|
||||
{ name := fvH, userName := "h", type? := .some { pp? := .some "p ∨ q" } }
|
||||
]
|
||||
}])
|
||||
addTest $ LSpec.check "(1 parent)" state1.parentExpr?.isSome
|
||||
|
@ -351,75 +348,12 @@ def test_or_comm: TestM Unit := do
|
|||
userName? := .some caseName,
|
||||
target := { pp? := .some "q ∨ p" },
|
||||
vars := #[
|
||||
{ userName := "p", type? := .some typeProp, isInaccessible? := .some false },
|
||||
{ userName := "q", type? := .some typeProp, isInaccessible? := .some false },
|
||||
{ userName := "h✝", type? := .some { pp? := .some varName }, isInaccessible? := .some true }
|
||||
{ userName := "p", type? := .some typeProp },
|
||||
{ userName := "q", type? := .some typeProp },
|
||||
{ userName := "h✝", type? := .some { pp? := .some varName }, isInaccessible := true }
|
||||
]
|
||||
}
|
||||
|
||||
def test_have: TestM Unit := do
|
||||
let state? ← startProof (.expr "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))")
|
||||
let state0 ← match state? with
|
||||
| .some state => pure state
|
||||
| .none => do
|
||||
addTest $ assertUnreachable "Goal could not parse"
|
||||
return ()
|
||||
let tactic := "intro p q 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) =
|
||||
#[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "(p ∨ q) ∨ p ∨ q"])
|
||||
|
||||
let expr := "Or.inl (Or.inl h)"
|
||||
let state2 ← match ← state1.tryAssign (goalId := 0) (expr := expr) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check s!":= {expr}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
|
||||
#[])
|
||||
|
||||
let haveBind := "y"
|
||||
let haveType := "p ∨ q"
|
||||
let state2 ← match ← state1.tryHave (goalId := 0) (binderName := haveBind) (type := haveType) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check s!"have {haveBind}: {haveType}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
|
||||
#[
|
||||
buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "p ∨ q",
|
||||
buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p"), ("y", "p ∨ q")] "(p ∨ q) ∨ p ∨ q"
|
||||
])
|
||||
|
||||
let expr := "Or.inl h"
|
||||
let state3 ← match ← state2.tryAssign (goalId := 0) (expr := expr) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check s!":= {expr}" ((← state3.serializeGoals (options := ← read)).map (·.devolatilize) =
|
||||
#[])
|
||||
|
||||
let state2b ← match state3.continue state2 with
|
||||
| .ok state => pure state
|
||||
| .error e => do
|
||||
addTest $ assertUnreachable e
|
||||
return ()
|
||||
let expr := "Or.inl y"
|
||||
let state4 ← match ← state2b.tryAssign (goalId := 0) (expr := expr) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check s!":= {expr}" ((← state4.serializeGoals (options := ← read)).map (·.devolatilize) =
|
||||
#[])
|
||||
|
||||
addTest $ LSpec.check "(4 root)" state4.rootExpr?.isSome
|
||||
|
||||
example : ∀ (a b c1 c2: Nat), (b + a) + c1 = (b + a) + c2 → (a + b) + c1 = (b + a) + c2 := by
|
||||
intro a b c1 c2 h
|
||||
conv =>
|
||||
|
@ -607,83 +541,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
|
||||
|
@ -843,7 +700,6 @@ def test_nat_zero_add_alt: TestM Unit := do
|
|||
name := fvN,
|
||||
userName := "n",
|
||||
type? := .some { pp? := .some "Nat", sexp? := .some "(:c Nat)" },
|
||||
isInaccessible? := .some false
|
||||
}],
|
||||
}
|
||||
])
|
||||
|
@ -856,11 +712,8 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
|
|||
("Nat.add_comm delta", test_delta_variable),
|
||||
("arithmetic", test_arith),
|
||||
("Or.comm", test_or_comm),
|
||||
("have", test_have),
|
||||
("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),
|
||||
]
|
||||
|
|
|
@ -1,3 +1,4 @@
|
|||
import Test.Tactic.Congruence
|
||||
import Test.Tactic.MotivatedApply
|
||||
import Test.Tactic.NoConfuse
|
||||
import Test.Tactic.Prograde
|
||||
|
|
|
@ -7,16 +7,13 @@ open Pantograph
|
|||
|
||||
namespace Pantograph.Test.Tactic.Congruence
|
||||
|
||||
def test_congr_arg_list (env: Environment): IO LSpec.TestSeq :=
|
||||
def test_congr_arg_list : TestT Elab.TermElabM Unit := do
|
||||
let expr := "λ {α} (l1 l2 : List α) (h: l1 = l2) => l1.reverse = l2.reverse"
|
||||
runMetaMSeq env do
|
||||
let expr ← parseSentence expr
|
||||
Meta.lambdaTelescope expr $ λ _ body => do
|
||||
let mut tests := LSpec.TestSeq.done
|
||||
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
|
||||
let (newGoals, test) ← runTermElabMInMeta do
|
||||
let newGoals ← runTacticOnMVar Tactic.congruenceArg target.mvarId!
|
||||
let test := LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
|
||||
let newGoals ← runTacticOnMVar Tactic.evalCongruenceArg target.mvarId!
|
||||
addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
|
||||
[
|
||||
(`α, "Sort ?u.30"),
|
||||
(`a₁, "?α"),
|
||||
|
@ -25,26 +22,20 @@ def test_congr_arg_list (env: Environment): IO LSpec.TestSeq :=
|
|||
(`h, "?a₁ = ?a₂"),
|
||||
(`conduit, "(?f ?a₁ = ?f ?a₂) = (l1.reverse = l2.reverse)"),
|
||||
])
|
||||
return (newGoals, test)
|
||||
tests := tests ++ test
|
||||
let f := newGoals.get! 3
|
||||
let h := newGoals.get! 4
|
||||
let c := newGoals.get! 5
|
||||
let results ← f.apply (← parseSentence "List.reverse")
|
||||
tests := tests ++ (LSpec.check "apply" (results.length = 0))
|
||||
tests := tests ++ (LSpec.check "h" ((← exprToStr $ ← h.getType) = "?a₁ = ?a₂"))
|
||||
tests := tests ++ (LSpec.check "conduit" ((← exprToStr $ ← c.getType) = "(?a₁.reverse = ?a₂.reverse) = (l1.reverse = l2.reverse)"))
|
||||
return tests
|
||||
def test_congr_arg (env: Environment): IO LSpec.TestSeq :=
|
||||
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)")
|
||||
def test_congr_arg : TestT Elab.TermElabM Unit := do
|
||||
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)) =
|
||||
let newGoals ← runTacticOnMVar Tactic.evalCongruenceArg target.mvarId!
|
||||
addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
|
||||
[
|
||||
(`α, "Sort ?u.70"),
|
||||
(`a₁, "?α"),
|
||||
|
@ -53,18 +44,13 @@ def test_congr_arg (env: Environment): IO LSpec.TestSeq :=
|
|||
(`h, "?a₁ = ?a₂"),
|
||||
(`conduit, "(?f ?a₁ = ?f ?a₂) = (n * n = m * m)"),
|
||||
])
|
||||
tests := tests ++ test
|
||||
return tests
|
||||
def test_congr_fun (env: Environment): IO LSpec.TestSeq :=
|
||||
def test_congr_fun : TestT Elab.TermElabM Unit := do
|
||||
let expr := "λ (n m: Nat) => (n + m) + (n + m) = (n + m) * 2"
|
||||
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.congruenceFun target.mvarId!
|
||||
pure $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
|
||||
let newGoals ← runTacticOnMVar Tactic.evalCongruenceFun target.mvarId!
|
||||
addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
|
||||
[
|
||||
(`α, "Sort ?u.159"),
|
||||
(`f₁, "?α → Nat"),
|
||||
|
@ -73,18 +59,13 @@ def test_congr_fun (env: Environment): IO LSpec.TestSeq :=
|
|||
(`a, "?α"),
|
||||
(`conduit, "(?f₁ ?a = ?f₂ ?a) = (n + m + (n + m) = (n + m) * 2)"),
|
||||
])
|
||||
tests := tests ++ test
|
||||
return tests
|
||||
def test_congr (env: Environment): IO LSpec.TestSeq :=
|
||||
def test_congr : TestT Elab.TermElabM Unit := do
|
||||
let expr := "λ (a b: Nat) => a = b"
|
||||
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.congruence target.mvarId!
|
||||
pure $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
|
||||
let newGoals ← runTacticOnMVar Tactic.evalCongruence target.mvarId!
|
||||
addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
|
||||
[
|
||||
(`α, "Sort ?u.10"),
|
||||
(`f₁, "?α → Nat"),
|
||||
|
@ -95,15 +76,13 @@ def test_congr (env: Environment): IO LSpec.TestSeq :=
|
|||
(`h₂, "?a₁ = ?a₂"),
|
||||
(`conduit, "(?f₁ ?a₁ = ?f₂ ?a₂) = (a = b)"),
|
||||
])
|
||||
tests := tests ++ test
|
||||
return tests
|
||||
|
||||
def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
|
||||
[
|
||||
("congrArg List.reverse", test_congr_arg_list env),
|
||||
("congrArg", test_congr_arg env),
|
||||
("congrFun", test_congr_fun env),
|
||||
("congr", test_congr env),
|
||||
]
|
||||
("congrArg List.reverse", test_congr_arg_list),
|
||||
("congrArg", test_congr_arg),
|
||||
("congrFun", test_congr_fun),
|
||||
("congr", test_congr),
|
||||
] |>.map (λ (name, t) => (name, runTestTermElabM env t))
|
||||
|
||||
end Pantograph.Test.Tactic.Congruence
|
||||
|
|
|
@ -7,25 +7,21 @@ open Pantograph
|
|||
|
||||
namespace Pantograph.Test.Tactic.MotivatedApply
|
||||
|
||||
def test_type_extract (env: Environment): IO LSpec.TestSeq :=
|
||||
runMetaMSeq env do
|
||||
let mut tests := LSpec.TestSeq.done
|
||||
def test_type_extract : TestT Elab.TermElabM Unit := do
|
||||
let recursor ← parseSentence "@Nat.brecOn"
|
||||
let recursorType ← Meta.inferType recursor
|
||||
tests := tests ++ LSpec.check "recursorType" ("{motive : Nat → Sort ?u.1} → (t : Nat) → ((t : Nat) → Nat.below t → motive t) → motive t" =
|
||||
addTest $ 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
|
||||
| .some info => pure info
|
||||
| .none => throwError "Failed to extract recursor info"
|
||||
tests := tests ++ LSpec.check "iMotive" (info.iMotive = 2)
|
||||
addTest $ LSpec.check "iMotive" (info.iMotive = 2)
|
||||
let motiveType := info.getMotiveType
|
||||
tests := tests ++ LSpec.check "motiveType" ("Nat → Sort ?u.1" =
|
||||
addTest $ LSpec.check "motiveType" ("Nat → Sort ?u.1" =
|
||||
(← exprToStr motiveType))
|
||||
return tests
|
||||
|
||||
def test_nat_brec_on (env: Environment): IO LSpec.TestSeq :=
|
||||
def test_nat_brec_on : TestT Elab.TermElabM Unit := do
|
||||
let expr := "λ (n t: Nat) => n + 0 = n"
|
||||
runMetaMSeq env do
|
||||
let expr ← parseSentence expr
|
||||
Meta.lambdaTelescope expr $ λ _ body => do
|
||||
let recursor ← match Parser.runParserCategory
|
||||
|
@ -35,25 +31,21 @@ def test_nat_brec_on (env: Environment): IO LSpec.TestSeq :=
|
|||
(fileName := filename) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => throwError "Failed to parse: {error}"
|
||||
let mut tests := LSpec.TestSeq.done
|
||||
-- Apply the tactic
|
||||
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
|
||||
let tactic := Tactic.motivatedApply recursor
|
||||
let test ← runTermElabMInMeta do
|
||||
let tactic := Tactic.evalMotivatedApply recursor
|
||||
let newGoals ← runTacticOnMVar tactic target.mvarId!
|
||||
pure $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
|
||||
let test := LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
|
||||
[
|
||||
"Nat → Prop",
|
||||
"Nat",
|
||||
"∀ (t : Nat), Nat.below t → ?motive t",
|
||||
"?motive ?m.67 = (n + 0 = n)",
|
||||
])
|
||||
tests := tests ++ test
|
||||
return tests
|
||||
addTest test
|
||||
|
||||
def test_list_brec_on (env: Environment): IO LSpec.TestSeq :=
|
||||
def test_list_brec_on : TestT Elab.TermElabM Unit := do
|
||||
let expr := "λ {α : Type} (l: List α) => l ++ [] = [] ++ l"
|
||||
runMetaMSeq env do
|
||||
let expr ← parseSentence expr
|
||||
Meta.lambdaTelescope expr $ λ _ body => do
|
||||
let recursor ← match Parser.runParserCategory
|
||||
|
@ -63,13 +55,11 @@ def test_list_brec_on (env: Environment): IO LSpec.TestSeq :=
|
|||
(fileName := filename) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => throwError "Failed to parse: {error}"
|
||||
let mut tests := LSpec.TestSeq.done
|
||||
-- Apply the tactic
|
||||
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
|
||||
let tactic := Tactic.motivatedApply recursor
|
||||
let test ← runTermElabMInMeta do
|
||||
let tactic := Tactic.evalMotivatedApply recursor
|
||||
let newGoals ← runTacticOnMVar tactic target.mvarId!
|
||||
pure $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
|
||||
addTest $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
|
||||
[
|
||||
"Type ?u.90",
|
||||
"List ?m.92 → Prop",
|
||||
|
@ -77,12 +67,9 @@ def test_list_brec_on (env: Environment): IO LSpec.TestSeq :=
|
|||
"∀ (t : List ?m.92), List.below t → ?motive t",
|
||||
"?motive ?m.94 = (l ++ [] = [] ++ l)",
|
||||
])
|
||||
tests := tests ++ test
|
||||
return tests
|
||||
|
||||
def test_partial_motive_instantiation (env: Environment): IO LSpec.TestSeq := do
|
||||
def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
|
||||
let expr := "λ (n t: Nat) => n + 0 = n"
|
||||
runMetaMSeq env $ runTermElabMInMeta do
|
||||
let recursor ← match Parser.runParserCategory
|
||||
(env := ← MonadEnv.getEnv)
|
||||
(catName := `term)
|
||||
|
@ -92,13 +79,12 @@ def test_partial_motive_instantiation (env: Environment): IO LSpec.TestSeq := do
|
|||
| .error error => throwError "Failed to parse: {error}"
|
||||
let expr ← parseSentence 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 tactic := Tactic.evalMotivatedApply recursor
|
||||
let newGoals ← runTacticOnMVar tactic target.mvarId!
|
||||
let majorId := 67
|
||||
tests := tests ++ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
|
||||
addTest $ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
|
||||
[
|
||||
"Nat → Prop",
|
||||
"Nat",
|
||||
|
@ -106,25 +92,22 @@ def test_partial_motive_instantiation (env: Environment): IO LSpec.TestSeq := do
|
|||
s!"?motive ?m.{majorId} = (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}"))
|
||||
addTest $ (LSpec.check "goal name" (major.name.toString = s!"_uniq.{majorId}"))
|
||||
|
||||
-- Assign motive to `λ x => x + _`
|
||||
let motive_assign ← parseSentence "λ (x: Nat) => @Nat.add x + 0 = _"
|
||||
motive.assign motive_assign
|
||||
|
||||
let test ← conduit.withContext do
|
||||
addTest $ ← 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)")
|
||||
tests := tests ++ test
|
||||
|
||||
return tests
|
||||
|
||||
def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
|
||||
[
|
||||
("type_extract", test_type_extract env),
|
||||
("Nat.brecOn", test_nat_brec_on env),
|
||||
("List.brecOn", test_list_brec_on env),
|
||||
("Nat.brecOn partial motive instantiation", test_partial_motive_instantiation env),
|
||||
]
|
||||
("type_extract", test_type_extract),
|
||||
("Nat.brecOn", test_nat_brec_on),
|
||||
("List.brecOn", test_list_brec_on),
|
||||
("Nat.brecOn partial motive instantiation", test_partial_motive_instantiation),
|
||||
] |>.map (λ (name, t) => (name, runTestTermElabM env t))
|
||||
|
||||
end Pantograph.Test.Tactic.MotivatedApply
|
||||
|
|
|
@ -7,9 +7,8 @@ open Pantograph
|
|||
|
||||
namespace Pantograph.Test.Tactic.NoConfuse
|
||||
|
||||
def test_nat (env: Environment): IO LSpec.TestSeq :=
|
||||
def test_nat : TestT Elab.TermElabM Unit := do
|
||||
let expr := "λ (n: Nat) (h: 0 = n + 1) => False"
|
||||
runMetaMSeq env do
|
||||
let expr ← parseSentence expr
|
||||
Meta.lambdaTelescope expr $ λ _ body => do
|
||||
let recursor ← match Parser.runParserCategory
|
||||
|
@ -19,20 +18,14 @@ def test_nat (env: Environment): IO LSpec.TestSeq :=
|
|||
(fileName := filename) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => throwError "Failed to parse: {error}"
|
||||
let mut tests := LSpec.TestSeq.done
|
||||
-- Apply the tactic
|
||||
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
|
||||
let tactic := Tactic.noConfuse recursor
|
||||
let test ← runTermElabMInMeta do
|
||||
let tactic := Tactic.evalNoConfuse recursor
|
||||
let newGoals ← runTacticOnMVar tactic target.mvarId!
|
||||
pure $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
|
||||
[])
|
||||
tests := tests ++ test
|
||||
return tests
|
||||
addTest $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = [])
|
||||
|
||||
def test_nat_fail (env: Environment): IO LSpec.TestSeq :=
|
||||
def test_nat_fail : TestT Elab.TermElabM Unit := do
|
||||
let expr := "λ (n: Nat) (h: n = n) => False"
|
||||
runMetaMSeq env do
|
||||
let expr ← parseSentence expr
|
||||
Meta.lambdaTelescope expr $ λ _ body => do
|
||||
let recursor ← match Parser.runParserCategory
|
||||
|
@ -42,21 +35,17 @@ def test_nat_fail (env: Environment): IO LSpec.TestSeq :=
|
|||
(fileName := filename) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => throwError "Failed to parse: {error}"
|
||||
let mut tests := LSpec.TestSeq.done
|
||||
-- Apply the tactic
|
||||
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
|
||||
try
|
||||
let tactic := Tactic.noConfuse recursor
|
||||
let _ ← runTermElabMInMeta $ runTacticOnMVar tactic target.mvarId!
|
||||
tests := tests ++ assertUnreachable "Tactic should fail"
|
||||
let tactic := Tactic.evalNoConfuse recursor
|
||||
let _ ← runTacticOnMVar tactic target.mvarId!
|
||||
addTest $ assertUnreachable "Tactic should fail"
|
||||
catch _ =>
|
||||
tests := tests ++ LSpec.check "Tactic should fail" true
|
||||
return tests
|
||||
return tests
|
||||
addTest $ LSpec.check "Tactic should fail" true
|
||||
|
||||
def test_list (env: Environment): IO LSpec.TestSeq :=
|
||||
def test_list : TestT Elab.TermElabM Unit := do
|
||||
let expr := "λ (l: List Nat) (h: [] = 1 :: l) => False"
|
||||
runMetaMSeq env do
|
||||
let expr ← parseSentence expr
|
||||
Meta.lambdaTelescope expr $ λ _ body => do
|
||||
let recursor ← match Parser.runParserCategory
|
||||
|
@ -66,22 +55,18 @@ def test_list (env: Environment): IO LSpec.TestSeq :=
|
|||
(fileName := filename) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => throwError "Failed to parse: {error}"
|
||||
let mut tests := LSpec.TestSeq.done
|
||||
-- Apply the tactic
|
||||
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
|
||||
let tactic := Tactic.noConfuse recursor
|
||||
let test ← runTermElabMInMeta do
|
||||
let tactic := Tactic.evalNoConfuse recursor
|
||||
let newGoals ← runTacticOnMVar tactic target.mvarId!
|
||||
pure $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
|
||||
[])
|
||||
tests := tests ++ test
|
||||
return tests
|
||||
addTest $ LSpec.check "goals"
|
||||
((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = [])
|
||||
|
||||
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),
|
||||
("Nat fail", test_nat_fail),
|
||||
("List", test_list),
|
||||
] |>.map (λ (name, t) => (name, runTestTermElabM env t))
|
||||
|
||||
end Pantograph.Test.Tactic.NoConfuse
|
||||
|
|
|
@ -0,0 +1,266 @@
|
|||
import LSpec
|
||||
import Lean
|
||||
import Test.Common
|
||||
|
||||
open Lean
|
||||
open Pantograph
|
||||
|
||||
namespace Pantograph.Test.Tactic.Prograde
|
||||
|
||||
def test_eval : TestT Elab.TermElabM Unit := do
|
||||
let expr := "forall (p q : Prop) (h: p), And (Or p q) (Or p q)"
|
||||
let expr ← parseSentence expr
|
||||
Meta.forallTelescope expr $ λ _ body => do
|
||||
let e ← match Parser.runParserCategory
|
||||
(env := ← MonadEnv.getEnv)
|
||||
(catName := `term)
|
||||
(input := "Or.inl h")
|
||||
(fileName := filename) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => throwError "Failed to parse: {error}"
|
||||
-- Apply the tactic
|
||||
let goal ← Meta.mkFreshExprSyntheticOpaqueMVar body
|
||||
let target: Expr := mkAnd
|
||||
(mkOr (.fvar ⟨uniq 8⟩) (.fvar ⟨uniq 9⟩))
|
||||
(mkOr (.fvar ⟨uniq 8⟩) (.fvar ⟨uniq 9⟩))
|
||||
let h := .fvar ⟨uniq 8⟩
|
||||
addTest $ LSpec.test "goals before" ((← toCondensedGoal goal.mvarId!).devolatilize == {
|
||||
context := #[
|
||||
cdeclOf `p (.sort 0),
|
||||
cdeclOf `q (.sort 0),
|
||||
cdeclOf `h h
|
||||
],
|
||||
target,
|
||||
})
|
||||
let tactic := Tactic.evalDefine `h2 e
|
||||
let m := .mvar ⟨uniq 13⟩
|
||||
let [newGoal] ← runTacticOnMVar tactic goal.mvarId! | panic! "Incorrect goal number"
|
||||
addTest $ LSpec.test "goals after" ((← toCondensedGoal newGoal).devolatilize == {
|
||||
context := #[
|
||||
cdeclOf `p (.sort 0),
|
||||
cdeclOf `q (.sort 0),
|
||||
cdeclOf `h h,
|
||||
{
|
||||
userName := `h2,
|
||||
type := mkOr h m,
|
||||
value? := .some $ mkApp3 (mkConst `Or.inl) h m (.fvar ⟨uniq 10⟩)
|
||||
}
|
||||
],
|
||||
target,
|
||||
})
|
||||
addTest $ LSpec.test "assign" ((← getExprMVarAssignment? goal.mvarId!) == .some (.mvar newGoal))
|
||||
|
||||
def test_proof_eval : TestT Elab.TermElabM Unit := do
|
||||
let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))"
|
||||
let state0 ← GoalState.create rootExpr
|
||||
let tactic := "intro p q 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) =
|
||||
#[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "(p ∨ q) ∨ p ∨ q"])
|
||||
|
||||
let expr := "Or.inl (Or.inl h)"
|
||||
let state2 ← match ← state1.tryAssign (goalId := 0) (expr := expr) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check s!":= {expr}" ((← state2.serializeGoals).map (·.devolatilize) =
|
||||
#[])
|
||||
|
||||
let evalBind := "y"
|
||||
let evalExpr := "Or.inl h"
|
||||
let state2 ← match ← state1.tryDefine (goalId := 0) (binderName := evalBind) (expr := evalExpr) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check s!"eval {evalBind} := {evalExpr}" ((← state2.serializeGoals).map (·.devolatilize) =
|
||||
#[{
|
||||
target := { pp? := .some "(p ∨ q) ∨ p ∨ q"},
|
||||
vars := #[
|
||||
{ userName := "p", type? := .some { pp? := .some "Prop" } },
|
||||
{ userName := "q", type? := .some { pp? := .some "Prop" } },
|
||||
{ userName := "h", type? := .some { pp? := .some "p" } },
|
||||
{ userName := "y",
|
||||
type? := .some { pp? := .some "p ∨ ?m.25" },
|
||||
value? := .some { pp? := .some "Or.inl h" },
|
||||
}
|
||||
]
|
||||
}])
|
||||
|
||||
let expr := "Or.inl y"
|
||||
let state3 ← match ← state2.tryAssign (goalId := 0) (expr := expr) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check s!":= {expr}" ((← state3.serializeGoals).map (·.devolatilize) =
|
||||
#[])
|
||||
|
||||
addTest $ LSpec.check "(3 root)" state3.rootExpr?.isSome
|
||||
|
||||
def test_proof_have : TestT Elab.TermElabM Unit := do
|
||||
let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))"
|
||||
let state0 ← GoalState.create rootExpr
|
||||
let tactic := "intro p q 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) =
|
||||
#[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "(p ∨ q) ∨ p ∨ q"])
|
||||
|
||||
let expr := "Or.inl (Or.inl h)"
|
||||
let state2 ← match ← state1.tryAssign (goalId := 0) (expr := expr) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check s!":= {expr}" ((← state2.serializeGoals).map (·.devolatilize) =
|
||||
#[])
|
||||
|
||||
let haveBind := "y"
|
||||
let haveType := "p ∨ q"
|
||||
let state2 ← match ← state1.tryHave (goalId := 0) (binderName := haveBind) (type := haveType) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check s!"have {haveBind}: {haveType}" ((← state2.serializeGoals).map (·.devolatilize) =
|
||||
#[
|
||||
buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "p ∨ q",
|
||||
buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p"), ("y", "p ∨ q")] "(p ∨ q) ∨ p ∨ q"
|
||||
])
|
||||
|
||||
let expr := "Or.inl h"
|
||||
let state3 ← match ← state2.tryAssign (goalId := 0) (expr := expr) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check s!":= {expr}" ((← state3.serializeGoals).map (·.devolatilize) =
|
||||
#[])
|
||||
|
||||
let state2b ← match state3.continue state2 with
|
||||
| .ok state => pure state
|
||||
| .error e => do
|
||||
addTest $ assertUnreachable e
|
||||
return ()
|
||||
let expr := "Or.inl y"
|
||||
let state4 ← match ← state2b.tryAssign (goalId := 0) (expr := expr) with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check s!":= {expr}" ((← state4.serializeGoals).map (·.devolatilize) =
|
||||
#[])
|
||||
|
||||
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
|
|
@ -91,16 +91,16 @@
|
|||
"lspec": {
|
||||
"flake": false,
|
||||
"locked": {
|
||||
"lastModified": 1701971219,
|
||||
"narHash": "sha256-HYDRzkT2UaLDrqKNWesh9C4LJNt0JpW0u68wYVj4Byw=",
|
||||
"lastModified": 1722857503,
|
||||
"narHash": "sha256-F9uaymiw1wTCLrJm4n1Bpk3J8jW6poedQzvnnQlZ6Kw=",
|
||||
"owner": "lurk-lab",
|
||||
"repo": "LSpec",
|
||||
"rev": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
|
||||
"rev": "8a51034d049c6a229d88dd62f490778a377eec06",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "lurk-lab",
|
||||
"ref": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
|
||||
"ref": "8a51034d049c6a229d88dd62f490778a377eec06",
|
||||
"repo": "LSpec",
|
||||
"type": "github"
|
||||
}
|
||||
|
|
|
@ -9,7 +9,7 @@
|
|||
url = "github:leanprover/lean4?ref=v4.10.0-rc1";
|
||||
};
|
||||
lspec = {
|
||||
url = "github:lurk-lab/LSpec?ref=3388be5a1d1390594a74ec469fd54a5d84ff6114";
|
||||
url = "github:lurk-lab/LSpec?ref=8a51034d049c6a229d88dd62f490778a377eec06";
|
||||
flake = false;
|
||||
};
|
||||
};
|
||||
|
@ -63,9 +63,11 @@
|
|||
packages = {
|
||||
inherit (leanPkgs) lean lean-all;
|
||||
inherit (project) sharedLib executable;
|
||||
inherit project leanPkgs;
|
||||
default = project.executable;
|
||||
};
|
||||
legacyPackages = {
|
||||
inherit project leanPkgs;
|
||||
};
|
||||
checks = {
|
||||
test = pkgs.runCommand "test" {
|
||||
buildInputs = [ test.executable leanPkgs.lean-all ];
|
||||
|
|
Loading…
Reference in New Issue