inductive Duper.ProverM.VarRemovalRes : Type

The inductive return type of removeVanishedVarsHelper

• NotVacuous (res : Clause × RuleM.Proof) : VarRemovalRes
• PotentiallyVacuous (res : Clause × RuleM.Proof) : VarRemovalRes
• NoChangeNotVacuous : VarRemovalRes
• NoChangePotentiallyVacuous : VarRemovalRes

def Duper.ProverM.getNonemptyType (c : MClause) : Option Lean.Expr

Equations

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

def Duper.ProverM.mkRemoveVanishedVarsProof (premises : List Lean.Expr) (parents : List RuleM.ProofParent) (transferExprs : Array Lean.Expr) (c : Clause) : Lean.MetaM Lean.Expr

Equations

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

def Duper.ProverM.mkDeriveNewNonemptyTypeProof1 (premises : List Lean.Expr) (parents : List RuleM.ProofParent) (transferExprs : Array Lean.Expr) (c : Clause) : Lean.MetaM Lean.Expr

mkDeriveNewNonemptyTypeProof1 expects to receive one parent of the form Nonempty (t1 → t2) = True where t1 is a type in verifiedInhabitedTypes (and is therefore a type whose inhabitation status can be confirmed by Lean.Meta.findInstance).

Note: Right now, mkDeriveNewNonemptyTypeProof1 does not support lemmas of the form True = Nonempty t, and I think this is fine because Duper should never generate clauses of that form. However, if for some reason this ever becomes a problem, it should be straightforward to extend mkDeriveNewNonemptyTypeProof1 to support that case.

Equations

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

def Duper.ProverM.mkDeriveNewNonemptyTypeProof2 (premises : List Lean.Expr) (parents : List RuleM.ProofParent) (transferExprs : Array Lean.Expr) (c : Clause) : Lean.MetaM Lean.Expr

mkDeriveNewNonemptyTypeProof2 expects to receive two parents, first a clause that says Nonempty (t1 → t2) = True and second a clause that says Nonempty t1 = True.

Note: Right now, mkDeriveNewNonemptyTypeProof2 does not support lemmas of the form True = Nonempty t, and I think this is fine because Duper should never generate clauses of that form. However, if for some reason this ever becomes a problem, it should be straightforward to extend mkDeriveNewNonemptyTypeProof2 to support that case.

Equations

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

def Duper.ProverM.mkDeriveNewNonemptyTypeProof3 (premises : List Lean.Expr) (parents : List RuleM.ProofParent) (transferExprs : Array Lean.Expr) (c : Clause) : Lean.MetaM Lean.Expr

mkDeriveNewNonemptyTypeProof3 expects to receive one parent of the form Nonempty (t1 × t2) = True and yields a proof of Nonempty t1 = True.

Note: Right now, mkDeriveNewNonemptyTypeProof3 does not support lemmas of the form True = Nonempty t, and I think this is fine because Duper should never generate clauses of that form. However, if for some reason this ever becomes a problem, it should be straightforward to extend mkDeriveNewNonemptyTypeProof2 to support that case.

Equations

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

def Duper.ProverM.mkDeriveNewNonemptyTypeProof4 (premises : List Lean.Expr) (parents : List RuleM.ProofParent) (transferExprs : Array Lean.Expr) (c : Clause) : Lean.MetaM Lean.Expr

mkDeriveNewNonemptyTypeProof4 expects to receive one parent of the form Nonempty (t1 × t2) = True and yields a proof of Nonempty t2 = True.

Note: Right now, mkDeriveNewNonemptyTypeProof4 does not support lemmas of the form True = Nonempty t, and I think this is fine because Duper should never generate clauses of that form. However, if for some reason this ever becomes a problem, it should be straightforward to extend mkDeriveNewNonemptyTypeProof2 to support that case.

Equations

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

def Duper.ProverM.mkDeriveNewNonemptyTypeProof5 (premises : List Lean.Expr) (parents : List RuleM.ProofParent) (transferExprs : Array Lean.Expr) (c : Clause) : Lean.MetaM Lean.Expr

mkDeriveNewNonemptyTypeProof5 expects to receive one parent of the form Nonempty (PProd t1 t2) = True and yields a proof of Nonempty t1 = True.

Note: Right now, mkDeriveNewNonemptyTypeProof5 does not support lemmas of the form True = Nonempty t, and I think this is fine because Duper should never generate clauses of that form. However, if for some reason this ever becomes a problem, it should be straightforward to extend mkDeriveNewNonemptyTypeProof2 to support that case.

Equations

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

def Duper.ProverM.mkDeriveNewNonemptyTypeProof6 (premises : List Lean.Expr) (parents : List RuleM.ProofParent) (transferExprs : Array Lean.Expr) (c : Clause) : Lean.MetaM Lean.Expr

mkDeriveNewNonemptyTypeProof6 expects to receive one parent of the form Nonempty (PProd t1 t2) = True and yields a proof of Nonempty t2 = True.

Note: Right now, mkDeriveNewNonemptyTypeProof6 does not support lemmas of the form True = Nonempty t, and I think this is fine because Duper should never generate clauses of that form. However, if for some reason this ever becomes a problem, it should be straightforward to extend mkDeriveNewNonemptyTypeProof2 to support that case.

Equations

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

def Duper.ProverM.mkDeriveNewNonemptyTypeProof7 (premises : List Lean.Expr) (parents : List RuleM.ProofParent) (transferExprs : Array Lean.Expr) (c : Clause) : Lean.MetaM Lean.Expr

mkDeriveNewNonemptyTypeProof7 expects to receive one parent of the form Nonempty p = True where p : Prop. mkDeriveNewNonemptyTypeProof6 yields a proof that p = True.

Note: Right now, mkDeriveNewNonemptyTypeProof7 does not support lemmas of the form True = Nonempty t, and I think this is fine because Duper should never generate clauses of that form. However, if for some reason this ever becomes a problem, it should be straightforward to extend mkDeriveNewNonemptyTypeProof2 to support that case.

Equations

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

partial def Duper.ProverM.deriveNonemptyFrom (abstractedType t : AbstractMVars.AbstractMVarsResult) : Lean.MetaM Bool

Determines if Nonempty abstractedType can be derived specifically from Nonempty t

def Duper.ProverM.deriveNonempty (abstractedType : AbstractMVars.AbstractMVarsResult) (verifiedNonemptyTypes : abstractedMVarAndClauseList) : Lean.MetaM (Option Clause)

Determines if Nonempty abstractedType can be derived from any type in verifiedNonemptyTypes

Equations

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

def Duper.ProverM.removeVanishedVarsHelper (c : Clause) (verifiedInhabitedTypes : abstractedMVarList) (verifiedNonemptyTypes : abstractedMVarAndClauseList) (potentiallyUninhabitedTypes : abstractedMVarList) : RuleM.RuleM (VarRemovalRes × abstractedMVarList × abstractedMVarList)

Attempts to remove the vanished variables that appear in c, updating verifiedInhabitedTypes and potentiallyUninhabitedTypes as it encounters types whose inhabitation status has not previously been checked.

Equations

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

def Duper.ProverM.removeVanishedVars (givenClause : Clause) : ProverM (Option (Clause × Bool))

Iterates through c's bVarTypes and removes each bVarType whose bvar does not appear in c. If removeVanishedVars encounters a bVarType that has not been verified to be inhabited, then it returns the updated clause and false to indicate that the clause should not be used to simplify away any other clauses. Otherwise, removeVanishedVars returns the updated clause and true. The only case where removeVanishedVars will return none is if it generates a clause that has already been simplified away (and therefore does not need to be re-evaluated).

Note: removeVanishedVars is not written as a forward simplification rule (even though it functions similarly) because it uniquely interacts with ProverM's verifiedInhabitedTypes and potentiallyUninhabitedTypes.

Equations

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

def Duper.ProverM.registerNewInhabitedTypesHelper (givenClause : Clause) : RuleM.RuleM (Option AbstractMVars.AbstractMVarsResult)

If givenClause is of the form Nonempty t = True or True = Nonempty t, then returns (← abstractMVars t). If givenClause has the form ∀ x1 : t1, ∀ x2 : t2, ... Nonempty t = True, then registerNewInhabitedTypesHelper returns (← abstractMVars (t1 → t2 → ... → t))

Equations

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

def Duper.ProverM.clauseHasAbstractedT (c : Clause) (abstractedT : AbstractMVars.AbstractMVarsResult) : RuleM.RuleM Bool

Returns true if any of c's bVarTypes match abstractedT or have the form α1 → α2 → ... abstractedT. If this is the case, then said clause should be returned to the passive set (and removed from the set of potentially vacuous clauses) so that it can be re-evaluated.

Equations

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

def Duper.ProverM.deriveNewNonemptyTypesHelper (abstractedT : AbstractMVars.AbstractMVarsResult) (givenClause : Clause) : ProverM Unit

Derives new Nonempty types from the combination of the new Nonempty type abstractedT and current verifiedInhabitedTypes and verifiedNonemptyTypes. Specifically, deriveNewNonemptyTypes exhaustively applies the rule:

• If any type in verifiedNonemptyTypes has the form t1 → t2 and abstractedT matches t1, then derive Nonempty t2

Equations

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

def Duper.ProverM.deriveNewNonemptyTypes (abstractedT : AbstractMVars.AbstractMVarsResult) (givenClause : Clause) : ProverM Unit

Derives new Nonempty types from the combination of the new Nonempty type abstractedT and current verifiedInhabitedTypes and verifiedNonemptyTypes. Specifically, deriveNewNonemptyTypes exhaustively applies three rules:

• If abstracted.expr has the form t1 × t2 (where × denotes either Prod or PProd) then derive Nonempty t1 and Nonempty t2
• If abstractedT.expr has the form t1 → t2 and t1 is Inhabited or Nonempty, then derive Nonempty t2
• If any type in verifiedNonemptyTypes has the form t1 → t2 and abstractedT matches t1, then derive Nonempty t2

Jointly, these rules keep verifiedNonemptyTypes saturated with respect to application in the long run. Temporarily, verifiedNonemptyTypes can have a state where α α → β are both in verifiedNonemptyTypes but β is not, but this will only occur after deriveNewNonemptyTypes returns if either Nonempty α or Nonempty (α → β) was generated by deriveNewNonemptyTypes. Since deriveNewNonemptyTypes adds clauses it generates to the passive set (using addNewToPassive rather than addNewClause), these clauses that it generates will quickly be selected and sent to registerNewNonemptyTypes which will cause Nonempty β to be generated.

Equations

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

def Duper.ProverM.registerNewNonemptyTypes (givenClause : Clause) : ProverM Unit

If givenClause has the form Nonempty t = True or True = Nonempty t, then add t to verifiedInhabitedTypes and add givenClause to inhabitedTypeWitnesses. Additionally, from the new Nonempty type fact, this function derives (and produces clauses for) any additional derivable Nonempty types. Finally, registerNewNonemptyTypes re-evaluates the set of potentially vacuous clauses to see if any clauses previously considered potentially vacuous can now be proven to not be potentially vacuous.

Equations

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