aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 15 Pull Requests 3 Packages Projects Releases Wiki Activity

test: Use synthetic tactic to generate aux lemmas

This commit is contained in:
Leni Aniva 2025-06-20 12:00:25 -07:00
parent b3f88f5d54
commit 9d9f5dee88
Signed by: aniva
GPG Key ID: D5F96287843E8DFB
2 changed files with 32 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
Test/Common.lean
View File

@ -183,6 +183,26 @@ def buildGoal (nameType: List (String × String)) (target: String) (userName?: O
})).toArray
}
namespace Tactic
/-- Create an aux lemma and assigns it to `mvarId`, which is circuitous, but
exercises the aux lemma generator. -/
def assignWithAuxLemma (type value : Expr) : Elab.Tactic.TacticM Unit := do
let type ← instantiateMVars type
let value ← instantiateMVars value
if type.hasExprMVar then
throwError "Type has expression mvar"
if value.hasExprMVar then
throwError "value has expression mvar"
let goal ← Elab.Tactic.getMainGoal
goal.withContext do
let name ← Meta.mkAuxLemma [] type value
unless ← Meta.isDefEq type (← goal.getType) do
throwError "Type provided is incorrect"
goal.assign (.const name [])
end Tactic
end Test
end Pantograph

25
Test/Serial.lean
View File

@ -74,22 +74,21 @@ def test_goal_state_simple : TestM Unit := do
def test_pickling_env_extensions : TestM Unit := do
let coreSrc : Core.State := { env := ← getEnv }
let p := mkIdent `p
let h := mkIdent `h
let ((), _) ← runCoreM coreSrc $ transformTestT runTermElabMInCore do
let .ok e ← elabTerm (← `(term|2 ≤ 5)) .none | unreachable!
let .ok e ← elabTerm (← `(term|(2: Nat) ≤ 3 ∧ (3: Nat) ≤ 5)) .none | unreachable!
let state ← GoalState.create e
let .success state _ ← state.tacticOn' 0 (← `(tactic|apply Nat.le_trans)) | unreachable!
let .success state' _ ← state.tacticOn' 2 (← `(tactic|exact 3)) | unreachable!
let state := state'.immediateResume state
let .success state1 _ ← state.tacticOn' 1 (← `(tactic|simp)) | unreachable!
let parentExpr := state1.parentExpr?.get!
IO.println s!"{parentExpr}"
checkTrue "has aux lemma" $ parentExpr.getUsedConstants.any λ name => name.isAuxLemma
let .success state _ ← state.tacticOn' 0 (← `(tactic|apply And.intro)) | unreachable!
let state1 := state1.immediateResume state
let .success stateT _ ← state.tacticOn' 0 (← `(tactic|simp)) | unreachable!
let rootExpr:= stateT.rootExpr?.get!
IO.println s!"root is {rootExpr}"
checkTrue "has aux lemma" $ rootExpr.getUsedConstants.any λ name => name.isAuxLemma
let goal := state.goals[0]!
let (type, value) ← goal.withContext do
let .ok type ← elabTerm (← `(term|(2: Nat) ≤ 3)) (.some $ .sort 0) | unreachable!
let .ok value ← elabTerm (← `(term|sorry)) (.some type) | unreachable!
pure (type, value)
let .success state1 _ ← state.tryTacticM goal (Tactic.assignWithAuxLemma type value) | unreachable!
let parentExpr := state1.parentExpr?.get!
checkTrue "has aux lemma" $ parentExpr.getUsedConstants.any λ name => name.isAuxLemma
return ()
structure Test where