def Duper.instantiatePremises (parents : List RuleM.ProofParent) (premises : List Lean.Expr) (xs transferExprs : Array Lean.Expr) : Lean.MetaM (List (Array Lit) × List Lean.Expr × Array Lean.Expr)

Equations

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

def Duper.orCases (lits caseProofs : Array Lean.Expr) : Lean.MetaM Lean.Expr

Construct a proof of lits[0] ∨ ... ∨ lits[n] → target, given proofs (casesProofs) of lits[i] → target

Equations

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

def Duper.orIntro (lits : Array Lean.Expr) (i : Nat) (proof : Lean.Expr) : Lean.MetaM Lean.Expr

Construct a proof of lits[0] ∨ ... ∨ lits[n], given a proof of lits[i]

Equations

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

def Duper.orSubclause (lits : Array Lean.Expr) (i : Nat) (proof : Lean.Expr) : Lean.MetaM Lean.Expr

Construct a proof of lits[0] ∨ ... ∨ lits[n], given a proof of the subclause consisting of the last i literals

Equations

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

def Duper.andBuild (l : List Lean.Expr) : Lean.MetaM Lean.Expr

Given a list l of propositions, constructs the proposition l[0] ∧ ... ∧ l[n]

Equations

• Duper.andBuild [] = Lean.throwError (Lean.toMessageData "Cannot build an empty conjunction")
• Duper.andBuild [l1] = pure l1
• Duper.andBuild (l1 :: restL) = do let __do_lift ← Duper.andBuild restL pure (Lean.mkApp2 (Lean.mkConst `And) l1 __do_lift)

def Duper.andGet (l : List Lean.Expr) (i : Nat) (proof : Lean.Expr) : Lean.MetaM Lean.Expr

Given a proof of a conjunction with n conjuncts, constructs a proof of i-th conjunct

Equations

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

partial def Duper.getConjunctiveHypothesesHelper (e : Lean.Expr) (hyps : Array Lean.Expr := #[]) : Array Lean.Expr

Assuming e has the form e1 ∧ e2 ∧ ... ∧ en, returns an array #[e1, e2, ... en]. Note: If e has the form (e1a ∧ e1b) ∧ e2 ∧ ... ∧ en, then the conjunction (e1a ∧ e1b) will be considered e1 (and the conjunction e1 will not be broken down further). This decision is made to reflect the form of the conjunction assumed by andGet

def Duper.getConjunctiveHypotheses (e : Lean.Expr) : List Lean.Expr

Assuming e has the form e1 ∧ e2 ∧ ... ∧ en, returns a list [e1, e2, ... en]. Note: If e has the form (e1a ∧ e1b) ∧ e2 ∧ ... ∧ en, then the conjunction (e1a ∧ e1b) will be considered e1 (and the conjunction e1 will not be broken down further). This decision is made to reflect the form of the conjunction assumed by andGet

Equations

• Duper.getConjunctiveHypotheses e = (Duper.getConjunctiveHypothesesHelper e).toList

theorem Duper.not_and_or (p q : Prop) : ¬(p ∧ q) ↔ ¬p ∨ ¬q

partial def Duper.notAndDistribute (e prf : Lean.Expr) : Lean.MetaM Lean.Expr

Given a proof prf of type e which has the form ¬(p1 ∧ p2 ∧ ... pn), constructs a proof of ¬p1 ∨ ¬p2 ∨ ... ¬pn