Parameterized-coinduction tactics

The elaborators, macros and syntax that drive parameterized-coinduction proofs (pinit, pcofix, pfold, punfold, pcases, pleft/pright, pmon, ptop, ...). These act on goals phrased with the parameterized least fixed point plfp and its accumulation principle plfp_acc from PacoDefs.

def Lean.MVarId.introFact (mvarId : MVarId) (fact : Expr) : MetaM MVarId

introduce a new fact, given the witness for that fact

Equations

• One or more equations did not get rendered due to their size.

def Lean.MVarId.introFactWithNewGoal (mvarId : MVarId) (factType : Expr) : MetaM (MVarId × MVarId)

Introduce a new fact, and a new goal to prove that fact the new goal is the first return value.

Equations

• One or more equations did not get rendered due to their size.

def Lean4Itree.tacticPinit : Lean.ParserDescr

Initialise a parameterized-coinduction proof: mark the context and unfold the goal's lfp_monotone fixed point so the Paco combinators can act on it.

Equations

• Lean4Itree.tacticPinit = Lean.ParserDescr.node `Lean4Itree.tacticPinit 1024 (Lean.ParserDescr.nonReservedSymbol "pinit" false)

def Lean4Itree.tacticPcofixIntroAcc : Lean.ParserDescr

Introduce the plfp_acc accumulation hypothesis for the current goal, threading the goal's complete-lattice instance and monotonicity proof.

Equations

• Lean4Itree.tacticPcofixIntroAcc = Lean.ParserDescr.node `Lean4Itree.tacticPcofixIntroAcc 1024 (Lean.ParserDescr.nonReservedSymbol "pcofixIntroAcc" false)

def Lean4Itree.tacticPcofixWrap : Lean.ParserDescr

Repackage the coinduction goal into the existential relation expected by the accumulation hypothesis, producing the obligation, converter and main subgoals.

Equations

• Lean4Itree.tacticPcofixWrap = Lean.ParserDescr.node `Lean4Itree.tacticPcofixWrap 1024 (Lean.ParserDescr.nonReservedSymbol "pcofixWrap" false)

def Lean4Itree.tacticDestructLastAnd : Lean.ParserDescr

Split the most recently introduced hypothesis, which must be a conjunction, into its two components and clear the original.

Equations

• Lean4Itree.tacticDestructLastAnd = Lean.ParserDescr.node `Lean4Itree.tacticDestructLastAnd 1024 (Lean.ParserDescr.nonReservedSymbol "destructLastAnd" false)

def Lean4Itree.tacticPcofix_ : Lean.ParserDescr

The Paco coinduction tactic: starts a parameterized-coinduction proof and introduces the coinduction hypothesis under the name cih.

Equations

• One or more equations did not get rendered due to their size.

def Lean4Itree.tacticPfold : Lean.ParserDescr

Unfold the parameterized least fixed point once in the goal.

Equations

• Lean4Itree.tacticPfold = Lean.ParserDescr.node `Lean4Itree.tacticPfold 1024 (Lean.ParserDescr.nonReservedSymbol "pfold" false)

def Lean4Itree.tacticPunfoldAt_ : Lean.ParserDescr

Unfold the parameterized least fixed point once in a hypothesis.

Equations

• One or more equations did not get rendered due to their size.

def Lean4Itree.tacticPinitAt_ : Lean.ParserDescr

Initialise a parameterized-coinduction proof from a fixed-point hypothesis h.

Equations

• One or more equations did not get rendered due to their size.

def Lean4Itree.tacticPclearbotAt_ : Lean.ParserDescr

Clear the residual ⊤ₚ meet from a uplfp hypothesis, leaving the plain parameterized fixed point.

Equations

• One or more equations did not get rendered due to their size.

def Lean4Itree.tacticPsplitPrepare : Lean.ParserDescr

Introduce the disjunction lemma uplfp_goal for the current uplfp goal, threading the goal's complete-lattice instance.

Equations

• Lean4Itree.tacticPsplitPrepare = Lean.ParserDescr.node `Lean4Itree.tacticPsplitPrepare 1024 (Lean.ParserDescr.nonReservedSymbol "psplitPrepare" false)

def Lean4Itree.tacticPleft : Lean.ParserDescr

Discharge a uplfp goal by choosing its left (r) disjunct.

Equations

• Lean4Itree.tacticPleft = Lean.ParserDescr.node `Lean4Itree.tacticPleft 1024 (Lean.ParserDescr.nonReservedSymbol "pleft" false)

def Lean4Itree.tacticPright : Lean.ParserDescr

Discharge a uplfp goal by choosing its right (plfp) disjunct.

Equations

• Lean4Itree.tacticPright = Lean.ParserDescr.node `Lean4Itree.tacticPright 1024 (Lean.ParserDescr.nonReservedSymbol "pright" false)

def Lean4Itree.tacticPcasesPrepareAt_ : Lean.ParserDescr

Prepare a uplfp hypothesis for case analysis by exposing the underlying disjunction r ∨ plfp f r.

Equations

• One or more equations did not get rendered due to their size.

def Lean4Itree.tacticPcasesDoAt_ : Lean.ParserDescr

Apply the disjunction prepared by pcasesPrepare to the hypothesis h.

Equations

• One or more equations did not get rendered due to their size.

def Lean4Itree.tacticPcasesAt_ : Lean.ParserDescr

Rewrite a uplfp f r hypothesis into the disjunction r ∨ plfp f r.

Equations

• One or more equations did not get rendered due to their size.

def Lean4Itree.tacticPmon : Lean.ParserDescr

Reduce a plfp goal using monotonicity of the parameterized least fixed point.

Equations

• Lean4Itree.tacticPmon = Lean.ParserDescr.node `Lean4Itree.tacticPmon 1024 (Lean.ParserDescr.nonReservedSymbol "pmon" false)

def Lean4Itree.tacticPtop : Lean.ParserDescr

Close a goal of the form x ⊑ ⊤ₚ using the top-element specification.

Equations

• Lean4Itree.tacticPtop = Lean.ParserDescr.node `Lean4Itree.tacticPtop 1024 (Lean.ParserDescr.nonReservedSymbol "ptop" false)