Documentation

Duper.Rules.BoolSimp

inductive Duper.BoolSimpRule :

Rules 1 through 15 are from Leo-III. Rules 16 through 22 and 25 through 27 are from "Superposition with First-Class Booleans and Inprocessing Clausification." Rules 23, 24, and 28 were made just for duper. Rules with the b suffix operate on Bool, rules without the b suffix operate on Prop.

Instances For

instance Duper.instReprBoolSimpRule :

Repr BoolSimpRule

Equations

Duper.instReprBoolSimpRule = { reprPrec := Duper.reprBoolSimpRule✝ }

def Duper.BoolSimpRule.format (boolSimpRule : BoolSimpRule) :

Lean.MessageData

Equations

Duper.BoolSimpRule.rule1.format = Lean.toMessageData "rule1"
Duper.BoolSimpRule.rule1b.format = Lean.toMessageData "rule1b"
Duper.BoolSimpRule.rule2.format = Lean.toMessageData "rule2"
Duper.BoolSimpRule.rule2b.format = Lean.toMessageData "rule2b"
Duper.BoolSimpRule.rule2Sym.format = Lean.toMessageData "rule2Sym"
Duper.BoolSimpRule.rule2bSym.format = Lean.toMessageData "rule2bSym"
Duper.BoolSimpRule.rule3.format = Lean.toMessageData "rule3"
Duper.BoolSimpRule.rule3b.format = Lean.toMessageData "rule3b"
Duper.BoolSimpRule.rule3Sym.format = Lean.toMessageData "rule3Sym"
Duper.BoolSimpRule.rule3bSym.format = Lean.toMessageData "rule3bSym"
Duper.BoolSimpRule.rule4.format = Lean.toMessageData "rule4"
Duper.BoolSimpRule.rule4b.format = Lean.toMessageData "rule4b"
Duper.BoolSimpRule.rule4Sym.format = Lean.toMessageData "rule4Sym"
Duper.BoolSimpRule.rule4bSym.format = Lean.toMessageData "rule4bSym"
Duper.BoolSimpRule.rule5.format = Lean.toMessageData "rule5"
Duper.BoolSimpRule.rule5b.format = Lean.toMessageData "rule5b"
Duper.BoolSimpRule.rule6.format = Lean.toMessageData "rule6"
Duper.BoolSimpRule.rule6b.format = Lean.toMessageData "rule6b"
Duper.BoolSimpRule.rule6Sym.format = Lean.toMessageData "rule6Sym"
Duper.BoolSimpRule.rule6bSym.format = Lean.toMessageData "rule6bSym"
Duper.BoolSimpRule.rule7.format = Lean.toMessageData "rule7"
Duper.BoolSimpRule.rule7b.format = Lean.toMessageData "rule7b"
Duper.BoolSimpRule.rule8.format = Lean.toMessageData "rule8"
Duper.BoolSimpRule.rule8b.format = Lean.toMessageData "rule8b"
Duper.BoolSimpRule.rule9.format = Lean.toMessageData "rule9"
Duper.BoolSimpRule.rule9b.format = Lean.toMessageData "rule9b"
Duper.BoolSimpRule.rule9Sym.format = Lean.toMessageData "rule9Sym"
Duper.BoolSimpRule.rule9bSym.format = Lean.toMessageData "rule9bSym"
Duper.BoolSimpRule.rule10.format = Lean.toMessageData "rule10"
Duper.BoolSimpRule.rule10b.format = Lean.toMessageData "rule10b"
Duper.BoolSimpRule.rule10Sym.format = Lean.toMessageData "rule10Sym"
Duper.BoolSimpRule.rule10bSym.format = Lean.toMessageData "rule10bSym"
Duper.BoolSimpRule.rule11.format = Lean.toMessageData "rule11"
Duper.BoolSimpRule.rule11b.format = Lean.toMessageData "rule11b"
Duper.BoolSimpRule.rule11Sym.format = Lean.toMessageData "rule11Sym"
Duper.BoolSimpRule.rule11bSym.format = Lean.toMessageData "rule11bSym"
Duper.BoolSimpRule.rule12.format = Lean.toMessageData "rule12"
Duper.BoolSimpRule.rule12b.format = Lean.toMessageData "rule12b"
Duper.BoolSimpRule.rule13.format = Lean.toMessageData "rule13"
Duper.BoolSimpRule.rule13b.format = Lean.toMessageData "rule13b"
Duper.BoolSimpRule.rule13Sym.format = Lean.toMessageData "rule13Sym"
Duper.BoolSimpRule.rule13bSym.format = Lean.toMessageData "rule13bSym"
Duper.BoolSimpRule.rule14.format = Lean.toMessageData "rule14"
Duper.BoolSimpRule.rule14b.format = Lean.toMessageData "rule14b"
Duper.BoolSimpRule.rule15.format = Lean.toMessageData "rule15"
Duper.BoolSimpRule.rule15b.format = Lean.toMessageData "rule15b"
Duper.BoolSimpRule.rule16.format = Lean.toMessageData "rule16"
Duper.BoolSimpRule.rule17.format = Lean.toMessageData "rule17"
Duper.BoolSimpRule.rule18.format = Lean.toMessageData "rule18"
Duper.BoolSimpRule.rule19.format = Lean.toMessageData "rule19"
Duper.BoolSimpRule.rule20.format = Lean.toMessageData "rule20"
Duper.BoolSimpRule.rule21.format = Lean.toMessageData "rule21"
Duper.BoolSimpRule.rule22.format = Lean.toMessageData "rule22"
Duper.BoolSimpRule.rule23.format = Lean.toMessageData "rule23"
Duper.BoolSimpRule.rule23b.format = Lean.toMessageData "rule23b"
Duper.BoolSimpRule.rule24.format = Lean.toMessageData "rule24"
Duper.BoolSimpRule.rule24b.format = Lean.toMessageData "rule24b"
Duper.BoolSimpRule.rule25.format = Lean.toMessageData "rule25"
Duper.BoolSimpRule.rule26.format = Lean.toMessageData "rule26"
Duper.BoolSimpRule.rule27.format = Lean.toMessageData "rule27"
Duper.BoolSimpRule.rule28.format = Lean.toMessageData "rule28"

Instances For

instance Duper.instToMessageDataBoolSimpRule :

Lean.ToMessageData BoolSimpRule

Equations

Duper.instToMessageDataBoolSimpRule = { toMessageData := Duper.BoolSimpRule.format }

theorem Duper.rule1Theorem (p : Prop) :

(p ∨ p) = p

theorem Duper.rule1bTheorem (b : Bool) :

(b || b) = b

theorem Duper.rule2Theorem (p : Prop) :

(¬p ∨ p) = True

theorem Duper.rule2bTheorem (b : Bool) :

(!b || b) = true

theorem Duper.rule2SymTheorem (p : Prop) :

(p ∨ ¬p) = True

theorem Duper.rule2bSymTheorem (b : Bool) :

(b || !b) = true

theorem Duper.rule3Theorem (p : Prop) :

(p ∨ True) = True

theorem Duper.rule3bTheorem (b : Bool) :

(b || true) = true

theorem Duper.rule3SymTheorem (p : Prop) :

(True ∨ p) = True

theorem Duper.rule3bSymTheorem (b : Bool) :

(true || b) = true

theorem Duper.rule4Theorem (p : Prop) :

(p ∨ False) = p

theorem Duper.rule4bTheorem (b : Bool) :

(b || false) = b

theorem Duper.rule4SymTheorem (p : Prop) :

(False ∨ p) = p

theorem Duper.rule4bSymTheorem (b : Bool) :

(false || b) = b

theorem Duper.rule5Theorem {α : Sort u_1} (p : α) :

(p = p) = True

theorem Duper.rule5bTheorem (b : Bool) :

(b == b) = true

theorem Duper.rule6Theorem (p : Prop) :

(p = True) = p

theorem Duper.rule6bTheorem (b : Bool) :

(b == true) = b

theorem Duper.rule6SymTheorem (p : Prop) :

(True = p) = p

theorem Duper.rule6bSymTheorem (b : Bool) :

(true == b) = b

theorem Duper.rule7Theorem :

(¬False) = True

theorem Duper.rule7bTheorem :

(!false) = true

theorem Duper.rule8Theorem (p : Prop) :

(p ∧ p) = p

theorem Duper.rule8bTheorem (b : Bool) :

(b && b) = b

theorem Duper.rule9Theorem (p : Prop) :

(¬p ∧ p) = False

theorem Duper.rule9bTheorem (b : Bool) :

(!b && b) = false

theorem Duper.rule9SymTheorem (p : Prop) :

(p ∧ ¬p) = False

theorem Duper.rule9bSymTheorem (b : Bool) :

(b && !b) = false

theorem Duper.rule10Theorem (p : Prop) :

(p ∧ True) = p

theorem Duper.rule10bTheorem (b : Bool) :

(b && true) = b

theorem Duper.rule10SymTheorem (p : Prop) :

(True ∧ p) = p

theorem Duper.rule10bSymTheorem (b : Bool) :

(true && b) = b

theorem Duper.rule11Theorem (p : Prop) :

(p ∧ False) = False

theorem Duper.rule11bTheorem (b : Bool) :

(b && false) = false

theorem Duper.rule11SymTheorem (p : Prop) :

(False ∧ p) = False

theorem Duper.rule11bSymTheorem (b : Bool) :

(false && b) = false

theorem Duper.rule12Theorem {α : Sort u_1} (p : α) :

(p ≠ p) = False

theorem Duper.rule12bTheorem (b : Bool) :

(b != b) = false

theorem Duper.rule13Theorem (p : Prop) :

(p = False) = ¬p

theorem Duper.rule13bTheorem (b : Bool) :

(b == false) = !b

theorem Duper.rule13SymTheorem (p : Prop) :

(False = p) = ¬p

theorem Duper.rule13bSymTheorem (b : Bool) :

(false == b) = !b

theorem Duper.rule14Theorem :

(¬True) = False

theorem Duper.rule14bTheorem :

(!true) = false

theorem Duper.rule15Theorem (p : Prop) :

(¬¬p) = p

theorem Duper.rule15bTheorem (b : Bool) :

(!!b) = b

theorem Duper.rule16Theorem (p : Prop) :

(True → p) = p

theorem Duper.rule17Theorem (p : Prop) :

(False → p) = True

theorem Duper.rule18Theorem (p : Prop) :

(p → False) = ¬p

theorem Duper.rule19Theorem (α : Sort u_1) :

(∀ (x : α), True) = True

theorem Duper.rule20Theorem (p : Prop) :

(p → ¬p) = ¬p

theorem Duper.rule21Theorem (p : Prop) :

(¬p → p) = p

theorem Duper.rule22Theorem (p : Prop) :

(p → p) = True

theorem Duper.rule23Theorem (f : Prop → Prop) :

(∀ (p : Prop), f p) = (f True ∧ f False)

theorem Duper.rule23bTheorem (f : Bool → Prop) :

(∀ (b : Bool), f b) = (f true ∧ f false)

theorem Duper.rule24Theorem (f : Prop → Prop) :

(∃ (p : Prop ), f p) = (f True ∨ f False)

theorem Duper.rule24bTheorem (f : Bool → Prop) :

(∃ (b : Bool ), f b) = (f true ∨ f false)

theorem Duper.rule28Theorem (p1 p2 : Prop) :

(p1 ↔ p2) = (p1 = p2)

partial def Duper.mkRule25Theorem (e : Lean.Expr) (counter i j : Nat) :

Lean.MetaM Lean.Expr

partial def Duper.getDisjunctiveGoals (e : Lean.Expr) (goals : 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 disjunction (e1a ∨ e1b) will be considered e1 (and the disjunction e1 will not be broken down further). This decision is made to reflect the form of the disjunction assumed by ProofReconstruction.lean's orIntro

partial def Duper.mkRule26Theorem (e : Lean.Expr) (counter i j : Nat) :

Lean.MetaM Lean.Expr

def Duper.mkRule27Theorem (e : Lean.Expr) (i j : Nat) :

Lean.MetaM Lean.Expr

Equations

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

Instances For

def Duper.applyRule1 (e : Lean.Expr) :

Option Lean.Expr

s ∨ s ↦ s

Equations

Duper.applyRule1 (((Lean.Expr.const `Or us).app e1).app e2) = if (e1 == e2) = true then some e1 else none
Duper.applyRule1 e = none

Instances For

def Duper.applyRule1b (e : Lean.Expr) :

Option Lean.Expr

s || s ↦ s

Equations

Duper.applyRule1b (((Lean.Expr.const `Bool.or us).app e1).app e2) = if (e1 == e2) = true then some e1 else none
Duper.applyRule1b e = none

Instances For

def Duper.applyRule2 (e : Lean.Expr) :

Option Lean.Expr

¬s ∨ s ↦ True

Equations

Duper.applyRule2 (((Lean.Expr.const `Or us).app e1).app e2) = if (e1 == (Lean.Expr.const `Not []).app e2) = true then some (Lean.mkConst `True) else none
Duper.applyRule2 e = none

Instances For

def Duper.applyRule2b (e : Lean.Expr) :

Option Lean.Expr

!s || s ↦ true

Equations

Duper.applyRule2b (((Lean.Expr.const `Bool.or us).app e1).app e2) = if (e1 == (Lean.Expr.const `Bool.not []).app e2) = true then some (Lean.mkConst `Bool.true) else none
Duper.applyRule2b e = none

Instances For

def Duper.applyRule2Sym (e : Lean.Expr) :

Option Lean.Expr

s ∨ ¬s ↦ True

Equations

Duper.applyRule2Sym (((Lean.Expr.const `Or us).app e1).app e2) = if (e2 == (Lean.Expr.const `Not []).app e1) = true then some (Lean.mkConst `True) else none
Duper.applyRule2Sym e = none

Instances For

def Duper.applyRule2bSym (e : Lean.Expr) :

Option Lean.Expr

s || !s ↦ true

Equations

Duper.applyRule2bSym (((Lean.Expr.const `Bool.or us).app e1).app e2) = if (e2 == (Lean.Expr.const `Bool.not []).app e1) = true then some (Lean.mkConst `Bool.true) else none
Duper.applyRule2bSym e = none

Instances For

def Duper.applyRule3 (e : Lean.Expr) :

Option Lean.Expr

s ∨ True ↦ True

Equations

Duper.applyRule3 (((Lean.Expr.const `Or us).app e1).app e2) = if (e2 == Lean.mkConst `True) = true then some (Lean.mkConst `True) else none
Duper.applyRule3 e = none

Instances For

def Duper.applyRule3b (e : Lean.Expr) :

Option Lean.Expr

s || true ↦ true

Equations

Duper.applyRule3b (((Lean.Expr.const `Bool.or us).app e1).app e2) = if (e2 == Lean.mkConst `Bool.true) = true then some (Lean.mkConst `Bool.true) else none
Duper.applyRule3b e = none

Instances For

def Duper.applyRule3Sym (e : Lean.Expr) :

Option Lean.Expr

True ∨ s ↦ True

Equations

Duper.applyRule3Sym (((Lean.Expr.const `Or us).app e1).app e2) = if (e1 == Lean.mkConst `True) = true then some (Lean.mkConst `True) else none
Duper.applyRule3Sym e = none

Instances For

def Duper.applyRule3bSym (e : Lean.Expr) :

Option Lean.Expr

true || s ↦ true

Equations

Duper.applyRule3bSym (((Lean.Expr.const `Bool.or us).app e1).app e2) = if (e1 == Lean.mkConst `Bool.true) = true then some (Lean.mkConst `Bool.true) else none
Duper.applyRule3bSym e = none

Instances For

def Duper.applyRule4 (e : Lean.Expr) :

Option Lean.Expr

s ∨ False ↦ s

Equations

Duper.applyRule4 (((Lean.Expr.const `Or us).app e1).app e2) = if (e2 == Lean.mkConst `False) = true then some e1 else none
Duper.applyRule4 e = none

Instances For

def Duper.applyRule4b (e : Lean.Expr) :

Option Lean.Expr

s || false ↦ s

Equations

Duper.applyRule4b (((Lean.Expr.const `Bool.or us).app e1).app e2) = if (e2 == Lean.mkConst `Bool.false) = true then some e1 else none
Duper.applyRule4b e = none

Instances For

def Duper.applyRule4Sym (e : Lean.Expr) :

Option Lean.Expr

False ∨ s ↦ s

Equations

Duper.applyRule4Sym (((Lean.Expr.const `Or us).app e1).app e2) = if (e1 == Lean.mkConst `False) = true then some e2 else none
Duper.applyRule4Sym e = none

Instances For

def Duper.applyRule4bSym (e : Lean.Expr) :

Option Lean.Expr

false || s ↦ s

Equations

Duper.applyRule4bSym (((Lean.Expr.const `Bool.or us).app e1).app e2) = if (e1 == Lean.mkConst `Bool.false) = true then some e2 else none
Duper.applyRule4bSym e = none

Instances For

def Duper.applyRule5 (e : Lean.Expr) :

Option Lean.Expr

s = s ↦ True

Equations

Duper.applyRule5 ((((Lean.Expr.const `Eq us).app arg).app e1).app e2) = if (e1 == e2) = true then some (Lean.mkConst `True) else none
Duper.applyRule5 e = none

Instances For

def Duper.applyRule5b (e : Lean.Expr) :

Option Lean.Expr

s == s ↦ true

Equations

Duper.applyRule5b (((((Lean.Expr.const `BEq.beq us).app arg).app arg_1).app e1).app e2) = if (e1 == e2) = true then some (Lean.mkConst `Bool.true) else none
Duper.applyRule5b e = none

Instances For

def Duper.applyRule6 (e : Lean.Expr) :

Option Lean.Expr

s = True ↦ s

Equations

Duper.applyRule6 ((((Lean.Expr.const `Eq us).app arg).app e1).app e2) = if (e2 == Lean.mkConst `True) = true then some e1 else none
Duper.applyRule6 e = none

Instances For

def Duper.applyRule6b (e : Lean.Expr) :

Option Lean.Expr

s == true ↦ s

Equations

Duper.applyRule6b (((((Lean.Expr.const `BEq.beq us).app arg).app arg_1).app e1).app e2) = if (e2 == Lean.mkConst `Bool.true) = true then some e1 else none
Duper.applyRule6b e = none

Instances For

def Duper.applyRule6Sym (e : Lean.Expr) :

Option Lean.Expr

True = s ↦ s

Equations

Duper.applyRule6Sym ((((Lean.Expr.const `Eq us).app arg).app e1).app e2) = if (e1 == Lean.mkConst `True) = true then some e2 else none
Duper.applyRule6Sym e = none

Instances For

def Duper.applyRule6bSym (e : Lean.Expr) :

Option Lean.Expr

true == s ↦ s

Equations

Duper.applyRule6bSym (((((Lean.Expr.const `BEq.beq us).app arg).app arg_1).app e1).app e2) = if (e1 == Lean.mkConst `Bool.true) = true then some e2 else none
Duper.applyRule6bSym e = none

Instances For

def Duper.applyRule7 (e : Lean.Expr) :

Option Lean.Expr

Not False ↦ True

Equations

Duper.applyRule7 ((Lean.Expr.const `Not us).app (Lean.Expr.const `False us_1)) = some (Lean.mkConst `True)
Duper.applyRule7 e = none

Instances For

def Duper.applyRule7b (e : Lean.Expr) :

Option Lean.Expr

!false ↦ True

Equations

Duper.applyRule7b ((Lean.Expr.const `Bool.not us).app (Lean.Expr.const `Bool.false us_1)) = some (Lean.mkConst `Bool.true)
Duper.applyRule7b e = none

Instances For

def Duper.applyRule8 (e : Lean.Expr) :

Option Lean.Expr

s ∧ s ↦ s

Equations

Duper.applyRule8 (((Lean.Expr.const `And us).app e1).app e2) = if (e1 == e2) = true then some e1 else none
Duper.applyRule8 e = none

Instances For

def Duper.applyRule8b (e : Lean.Expr) :

Option Lean.Expr

s && s ↦ s

Equations

Duper.applyRule8b (((Lean.Expr.const `Bool.and us).app e1).app e2) = if (e1 == e2) = true then some e1 else none
Duper.applyRule8b e = none

Instances For

def Duper.applyRule9 (e : Lean.Expr) :

Option Lean.Expr

¬s ∧ s ↦ False

Equations

Duper.applyRule9 (((Lean.Expr.const `And us).app e1).app e2) = if (e1 == (Lean.Expr.const `Not []).app e2) = true then some (Lean.mkConst `False) else none
Duper.applyRule9 e = none

Instances For

def Duper.applyRule9b (e : Lean.Expr) :

Option Lean.Expr

!s && s ↦ false

Equations

Duper.applyRule9b (((Lean.Expr.const `Bool.and us).app e1).app e2) = if (e1 == (Lean.Expr.const `Bool.not []).app e2) = true then some (Lean.mkConst `Bool.false) else none
Duper.applyRule9b e = none

Instances For

def Duper.applyRule9Sym (e : Lean.Expr) :

Option Lean.Expr

s ∧ ¬s ↦ False

Equations

Duper.applyRule9Sym (((Lean.Expr.const `And us).app e1).app e2) = if (e2 == (Lean.Expr.const `Not []).app e1) = true then some (Lean.mkConst `False) else none
Duper.applyRule9Sym e = none

Instances For

def Duper.applyRule9bSym (e : Lean.Expr) :

Option Lean.Expr

s && !s ↦ false

Equations

Duper.applyRule9bSym (((Lean.Expr.const `Bool.and us).app e1).app e2) = if (e2 == (Lean.Expr.const `Bool.not []).app e1) = true then some (Lean.mkConst `Bool.false) else none
Duper.applyRule9bSym e = none

Instances For

def Duper.applyRule10 (e : Lean.Expr) :

Option Lean.Expr

s ∧ True ↦ s

Equations

Duper.applyRule10 (((Lean.Expr.const `And us).app e1).app e2) = if (e2 == Lean.mkConst `True) = true then some e1 else none
Duper.applyRule10 e = none

Instances For

def Duper.applyRule10b (e : Lean.Expr) :

Option Lean.Expr

s && true ↦ s

Equations

Duper.applyRule10b (((Lean.Expr.const `Bool.and us).app e1).app e2) = if (e2 == Lean.mkConst `Bool.true) = true then some e1 else none
Duper.applyRule10b e = none

Instances For

def Duper.applyRule10Sym (e : Lean.Expr) :

Option Lean.Expr

True ∧ s ↦ s

Equations

Duper.applyRule10Sym (((Lean.Expr.const `And us).app e1).app e2) = if (e1 == Lean.mkConst `True) = true then some e2 else none
Duper.applyRule10Sym e = none

Instances For

def Duper.applyRule10bSym (e : Lean.Expr) :

Option Lean.Expr

true && s ↦ s

Equations

Duper.applyRule10bSym (((Lean.Expr.const `Bool.and us).app e1).app e2) = if (e1 == Lean.mkConst `Bool.true) = true then some e2 else none
Duper.applyRule10bSym e = none

Instances For

def Duper.applyRule11 (e : Lean.Expr) :

Option Lean.Expr

s ∧ False ↦ False

Equations

Duper.applyRule11 (((Lean.Expr.const `And us).app e1).app e2) = if (e2 == Lean.mkConst `False) = true then some (Lean.mkConst `False) else none
Duper.applyRule11 e = none

Instances For

def Duper.applyRule11b (e : Lean.Expr) :

Option Lean.Expr

s && false ↦ false

Equations

Duper.applyRule11b (((Lean.Expr.const `Bool.and us).app e1).app e2) = if (e2 == Lean.mkConst `Bool.false) = true then some (Lean.mkConst `Bool.false) else none
Duper.applyRule11b e = none

Instances For

def Duper.applyRule11Sym (e : Lean.Expr) :

Option Lean.Expr

False ∧ s ↦ False

Equations

Duper.applyRule11Sym (((Lean.Expr.const `And us).app e1).app e2) = if (e1 == Lean.mkConst `False) = true then some (Lean.mkConst `False) else none
Duper.applyRule11Sym e = none

Instances For

def Duper.applyRule11bSym (e : Lean.Expr) :

Option Lean.Expr

false && s ↦ false

Equations

Duper.applyRule11bSym (((Lean.Expr.const `Bool.and us).app e1).app e2) = if (e1 == Lean.mkConst `Bool.false) = true then some (Lean.mkConst `Bool.false) else none
Duper.applyRule11bSym e = none

Instances For

def Duper.applyRule12 (e : Lean.Expr) :

Option Lean.Expr

s ≠ s ↦ False

Equations

Duper.applyRule12 ((((Lean.Expr.const `Ne us).app arg).app e1).app e2) = if (e1 == e2) = true then some (Lean.mkConst `False) else none
Duper.applyRule12 e = none

Instances For

def Duper.applyRule12b (e : Lean.Expr) :

Option Lean.Expr

s != s ↦ False

Equations

Duper.applyRule12b (((((Lean.Expr.const `bne us).app arg).app arg_1).app e1).app e2) = if (e1 == e2) = true then some (Lean.mkConst `Bool.false) else none
Duper.applyRule12b e = none

Instances For

def Duper.applyRule13 (e : Lean.Expr) :

Option Lean.Expr

s = False ↦ ¬s

Equations

Duper.applyRule13 ((((Lean.Expr.const `Eq us).app arg).app e1).app e2) = if (e2 == Lean.mkConst `False) = true then some (Lean.mkApp (Lean.mkConst `Not) e1) else none
Duper.applyRule13 e = none

Instances For

def Duper.applyRule13b (e : Lean.Expr) :

Option Lean.Expr

s == false ↦ !s

Equations

Duper.applyRule13b (((((Lean.Expr.const `BEq.beq us).app arg).app arg_1).app e1).app e2) = if (e2 == Lean.mkConst `Bool.false) = true then some (Lean.mkApp (Lean.mkConst `Bool.not) e1) else none
Duper.applyRule13b e = none

Instances For

def Duper.applyRule13Sym (e : Lean.Expr) :

Option Lean.Expr

False = s ↦ ¬s

Equations

Duper.applyRule13Sym ((((Lean.Expr.const `Eq us).app arg).app e1).app e2) = if (e1 == Lean.mkConst `False) = true then some (Lean.mkApp (Lean.mkConst `Not) e2) else none
Duper.applyRule13Sym e = none

Instances For

def Duper.applyRule13bSym (e : Lean.Expr) :

Option Lean.Expr

false == s ↦ !s

Equations

Duper.applyRule13bSym (((((Lean.Expr.const `BEq.beq us).app arg).app arg_1).app e1).app e2) = if (e1 == Lean.mkConst `Bool.false) = true then some (Lean.mkApp (Lean.mkConst `Bool.not) e2) else none
Duper.applyRule13bSym e = none

Instances For

def Duper.applyRule14 (e : Lean.Expr) :

Option Lean.Expr

Not True ↦ False

Equations

Duper.applyRule14 ((Lean.Expr.const `Not us).app (Lean.Expr.const `True us_1)) = some (Lean.mkConst `False)
Duper.applyRule14 e = none

Instances For

def Duper.applyRule14b (e : Lean.Expr) :

Option Lean.Expr

!true ↦ false

Equations

Duper.applyRule14b ((Lean.Expr.const `Bool.not us).app (Lean.Expr.const `Bool.true us_1)) = some (Lean.mkConst `Bool.false)
Duper.applyRule14b e = none

Instances For

def Duper.applyRule15 (e : Lean.Expr) :

Option Lean.Expr

¬¬s ↦ s

Equations

Duper.applyRule15 ((Lean.Expr.const `Not us).app ((Lean.Expr.const `Not us_1).app e')) = some e'
Duper.applyRule15 e = none

Instances For

def Duper.applyRule15b (e : Lean.Expr) :

Option Lean.Expr

!!s ↦ s

Equations

Duper.applyRule15b ((Lean.Expr.const `Bool.not us).app ((Lean.Expr.const `Bool.not us_1).app e')) = some e'
Duper.applyRule15b e = none

Instances For

def Duper.applyRule16 (e : Lean.Expr) :

Option Lean.Expr

True → s ↦ s

Equations

Duper.applyRule16 (Lean.Expr.forallE binderName t b binderInfo) = if (t == Lean.mkConst `True) = true then some b else none
Duper.applyRule16 e = none

Instances For

def Duper.applyRule17 (e : Lean.Expr) :

Option Lean.Expr

False → s ↦ True

Equations

Duper.applyRule17 (Lean.Expr.forallE binderName t b binderInfo) = if (t == Lean.mkConst `False) = true then some (Lean.mkConst `True) else none
Duper.applyRule17 e = none

Instances For

def Duper.applyRule18 (e : Lean.Expr) :

RuleM.RuleM (Option Lean.Expr)

s → False ↦ ¬s

Equations

One or more equations did not get rendered due to their size.
Duper.applyRule18 e = pure none

Instances For

def Duper.applyRule19 (e : Lean.Expr) :

Option Lean.Expr

s → True ↦ True (we generalize this to (∀ _ : α, True) ↦ True)

Equations

Duper.applyRule19 (Lean.Expr.forallE binderName t b binderInfo) = if (b == Lean.mkConst `True) = true then some (Lean.mkConst `True) else none
Duper.applyRule19 e = none

Instances For

def Duper.applyRule20 (e : Lean.Expr) :

Option Lean.Expr

s → ¬s ↦ ¬s

Equations

Duper.applyRule20 (Lean.Expr.forallE binderName t b binderInfo) = if (b == (Lean.Expr.const `Not []).app t) = true then some b else none
Duper.applyRule20 e = none

Instances For

def Duper.applyRule21 (e : Lean.Expr) :

Option Lean.Expr

¬s → s ↦ s

Equations

Duper.applyRule21 (Lean.Expr.forallE binderName t b binderInfo) = if (t == (Lean.Expr.const `Not []).app b) = true then some b else none
Duper.applyRule21 e = none

Instances For

def Duper.applyRule22 (e : Lean.Expr) :

RuleM.RuleM (Option Lean.Expr)

s → s ↦ True

Equations

One or more equations did not get rendered due to their size.
Duper.applyRule22 e = pure none

Instances For

def Duper.applyRule23 (e : Lean.Expr) :

RuleM.RuleM (Option Lean.Expr)

∀ p : Prop, f(p) ↦ f(True) ∧ f(False)

Equations

One or more equations did not get rendered due to their size.
Duper.applyRule23 e = pure none

Instances For

def Duper.applyRule23b (e : Lean.Expr) :

RuleM.RuleM (Option Lean.Expr)

∀ b : Bool, f(b) ↦ f true ∧ f false (assuming f : Bool → Prop)

Equations

One or more equations did not get rendered due to their size.
Duper.applyRule23b e = pure none

Instances For

def Duper.applyRule24 (e : Lean.Expr) :

RuleM.RuleM (Option Lean.Expr)

∃ p : Prop, f(p) ↦ f True ∨ f False

Equations

One or more equations did not get rendered due to their size.
Duper.applyRule24 e = pure none

Instances For

def Duper.applyRule24b (e : Lean.Expr) :

RuleM.RuleM (Option Lean.Expr)

∃ b : Bool, f(b) ↦ f true ∨ f false (assuming f : Bool → Prop)

Equations

One or more equations did not get rendered due to their size.
Duper.applyRule24b e = pure none

Instances For

partial def Duper.applyRule25Helper (e : Lean.Expr) (hyps : Array Lean.Expr) :

RuleM.RuleM (Option (Nat × Nat))

def Duper.applyRule25 (e : Lean.Expr) :

RuleM.RuleM (Option (Nat × Nat))

(s1 → s2 → ... → sn → v) ↦ True if there exists i and j such that si = ¬sj Since this rule will require a more involved proof reconstruction, rather than returning the resulting expression as in previous applyRule functions, we return the two indices of the hypotheses that directly contradict each other. Specifically, if si = ¬sj, then we return some (i, j).

Equations

Duper.applyRule25 e = Duper.applyRule25Helper e #[]

Instances For

partial def Duper.applyRule26Helper (e : Lean.Expr) (hyps : Array Lean.Expr) :

RuleM.RuleM (Option (Nat × Nat))

def Duper.applyRule26 (e : Lean.Expr) :

RuleM.RuleM (Option (Nat × Nat))

(s1 → s2 → ... → sn → v1 ∨ ... ∨ vm) ↦ True if there exists i and j such that si = vj Since this rule will require a more involved proof reconstruction, rather than returning the resulting expression as in previous applyRule functions, we return the index of the hypothesis si and the index of the conclusion vj. Specifically, if si = vj, then we return some (i, j)

Equations

Duper.applyRule26 e = Duper.applyRule26Helper e #[]

Instances For

def Duper.applyRule27 (e : Lean.Expr) :

RuleM.RuleM (Option (Nat × Nat))

(s1 ∧ s2 ∧ ... ∧ sn → v1 ∨ ... ∨ vm) ↦ True if there exists i and j such that si = vj Since this rule will require a more involved proof reconstruction, rather than returning the resulting expression as in previous applyRule functions, we return the index of the hypothesis si and the inddex of the conclusion vj. Specifically, if si = vj, then we return some (i, j)

Equations

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

Instances For

def Duper.applyRule28 (e : Lean.Expr) :

Option Lean.Expr

s1 ↔ s2 ↦ s1 = s2

Equations

Duper.applyRule28 (((Lean.Expr.const `Iff us).app e1).app e2) = some (Lean.mkApp3 (Lean.mkConst `Eq [Lean.levelOne ]) (Lean.mkSort Lean.levelZero) e1 e2)
Duper.applyRule28 e = none

Instances For

def Duper.getBoolSimpRuleTheorem (boolSimpRule : BoolSimpRule) (originalExp : Lean.Expr) (ijOpt : Option (Nat × Nat)) :

Lean.MetaM Lean.Expr

Returns the rule theorem corresponding to boolSimpRule with the first argument applied.

Note that this function assumes that boolSimpRule has already been shown to be applicable to originalExp so this is not rechecked (e.g. for rule1, this function does not check that the two propositions in the disjunction are actually equal, it assumes that this is the case from the fact that rule1 was applied)

Equations

One or more equations did not get rendered due to their size.
Duper.getBoolSimpRuleTheorem Duper.BoolSimpRule.rule25 originalExp (some (i, j)) = do let __do_lift ← Duper.mkRule25Theorem originalExp 0 i j Lean.Meta.mkAppM `eq_true #[__do_lift]
Duper.getBoolSimpRuleTheorem Duper.BoolSimpRule.rule25 originalExp none = Lean.throwError (Lean.toMessageData "rule25 requires indices that were not passed into getBoolSimpRuleTheorem")
Duper.getBoolSimpRuleTheorem Duper.BoolSimpRule.rule26 originalExp (some (i, j)) = do let __do_lift ← Duper.mkRule26Theorem originalExp 0 i j Lean.Meta.mkAppM `eq_true #[__do_lift]
Duper.getBoolSimpRuleTheorem Duper.BoolSimpRule.rule26 originalExp none = Lean.throwError (Lean.toMessageData "rule26 requires indices that were not passed into getBoolSimpRuleTheorem")
Duper.getBoolSimpRuleTheorem Duper.BoolSimpRule.rule27 originalExp (some (i, j)) = do let __do_lift ← Duper.mkRule27Theorem originalExp i j Lean.Meta.mkAppM `eq_true #[__do_lift]
Duper.getBoolSimpRuleTheorem Duper.BoolSimpRule.rule27 originalExp none = Lean.throwError (Lean.toMessageData "rule27 requires indices that were not passed into getBoolSimpRuleTheorem")

Instances For

def Duper.boolSimpRuleOperatesOnBool (boolSimpRule : BoolSimpRule) :

Some boolSimpRules (those with b suffixes) operates on Bool rather than Prop. mkBoolSimpProp needs to know whether boolSimpRule is one such rule in order to pass the correct type into congrArg

Equations

Instances For

def Duper.mkBoolSimpProof (substPos : ClausePos) (boolSimpRule : BoolSimpRule) (ijOpt : Option (Nat × Nat)) (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.

Instances For

def Duper.applyRulesList1 :

List ((Lean.Expr → Option Lean.Expr) × BoolSimpRule)

The list of rules that do not require the RuleM monad

Equations

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

Instances For

def Duper.applyRulesList2 :

List ((Lean.Expr → RuleM.RuleM (Option Lean.Expr)) × BoolSimpRule)

The list of rules that do require the RuleM monad

Equations

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

Instances For

def Duper.applyRulesList3 :

List ((Lean.Expr → RuleM.RuleM (Option (Nat × Nat))) × BoolSimpRule)

The list of rules for which indices must be returned

Equations

Duper.applyRulesList3 = [(Duper.applyRule25 , Duper.BoolSimpRule.rule25 ), (Duper.applyRule26 , Duper.BoolSimpRule.rule26 ), (Duper.applyRule27 , Duper.BoolSimpRule.rule27 )]

Instances For

def Duper.applyBoolSimpRules (e : Lean.Expr) :

RuleM.RuleM (Option (Lean.Expr × BoolSimpRule))

Equations

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

Instances For

def Duper.applyBoolSimpRulesWithIndices (e : Lean.Expr) :

RuleM.RuleM (Option ((Nat × Nat) × BoolSimpRule))

Equations

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

Instances For

def Duper.boolSimp :

Implements various Prop-related simplifications as described in "Superposition with First-Class Booleans and Inprocessing Clausification" and "Extensional Paramodulation for Higher-Order Logic and its Effective Implementation Leo-III"

Equations

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

Instances For