inductive Inference.Stat : Type

• var : ℕ → Stat
• not : Stat → Stat
• imp : Stat → Stat → Stat

@[instance_reducible]

instance Inference.instInhabitedStat : Inhabited Stat

Equations

• Inference.instInhabitedStat = { default := Inference.instInhabitedStat.default }

@[instance_reducible]

instance Inference.instDecidableEqStat : DecidableEq Stat

Equations

• Inference.instDecidableEqStat = Inference.instDecidableEqStat.decEq

def Inference.instDecidableEqStat.decEq (x✝ x✝¹ : Stat) : Decidable (x✝ = x✝¹)

Equations

• Inference.instDecidableEqStat.decEq (Inference.Stat.var a) (Inference.Stat.var b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Inference.instDecidableEqStat.decEq (Inference.Stat.var a) a_1.not = isFalse ⋯
• Inference.instDecidableEqStat.decEq (Inference.Stat.var a) (a_1.imp a_2) = isFalse ⋯
• Inference.instDecidableEqStat.decEq a.not (Inference.Stat.var a_1) = isFalse ⋯
• Inference.instDecidableEqStat.decEq a.not b.not = if h : a = b then h ▸ have inst := Inference.instDecidableEqStat.decEq a a; isTrue ⋯ else isFalse ⋯
• Inference.instDecidableEqStat.decEq a.not (a_1.imp a_2) = isFalse ⋯
• Inference.instDecidableEqStat.decEq (a.imp a_1) (Inference.Stat.var a_2) = isFalse ⋯
• Inference.instDecidableEqStat.decEq (a.imp a_1) a_2.not = isFalse ⋯
• Inference.instDecidableEqStat.decEq (a.imp a_1) (b.imp b_1) = if h : a = b then h ▸ have inst := Inference.instDecidableEqStat.decEq a a; have inst := Inference.instDecidableEqStat.decEq a_1 b_1; if h : a_1 = b_1 then h ▸ have inst := Inference.instDecidableEqStat.decEq a_1 a_1; isTrue ⋯ else isFalse ⋯ else isFalse ⋯

inductive Inference.ProofD : Type

• ax₁ : Stat → Stat → ProofD
• ax₂ : Stat → Stat → Stat → ProofD
• ax₃ : Stat → Stat → ProofD
• mp : ProofD → ProofD → ProofD

@[instance_reducible]

instance Inference.instInhabitedProofD : Inhabited ProofD

Equations

• Inference.instInhabitedProofD = { default := Inference.instInhabitedProofD.default }

@[instance_reducible]

instance Inference.instDecidableEqProofD : DecidableEq ProofD

Equations

• Inference.instDecidableEqProofD = Inference.instDecidableEqProofD.decEq

def Inference.instDecidableEqProofD.decEq (x✝ x✝¹ : ProofD) : Decidable (x✝ = x✝¹)

Equations

• Inference.instDecidableEqProofD.decEq (Inference.ProofD.ax₁ a a_1) (Inference.ProofD.ax₁ b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• Inference.instDecidableEqProofD.decEq (Inference.ProofD.ax₁ a a_1) (Inference.ProofD.ax₂ a_2 a_3 a_4) = isFalse ⋯
• Inference.instDecidableEqProofD.decEq (Inference.ProofD.ax₁ a a_1) (Inference.ProofD.ax₃ a_2 a_3) = isFalse ⋯
• Inference.instDecidableEqProofD.decEq (Inference.ProofD.ax₁ a a_1) (a_2.mp a_3) = isFalse ⋯
• Inference.instDecidableEqProofD.decEq (Inference.ProofD.ax₂ a a_1 a_2) (Inference.ProofD.ax₁ a_3 a_4) = isFalse ⋯
• Inference.instDecidableEqProofD.decEq (Inference.ProofD.ax₂ a a_1 a_2) (Inference.ProofD.ax₂ b b_1 b_2) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ if h : a_2 = b_2 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯ else isFalse ⋯
• Inference.instDecidableEqProofD.decEq (Inference.ProofD.ax₂ a a_1 a_2) (Inference.ProofD.ax₃ a_3 a_4) = isFalse ⋯
• Inference.instDecidableEqProofD.decEq (Inference.ProofD.ax₂ a a_1 a_2) (a_3.mp a_4) = isFalse ⋯
• Inference.instDecidableEqProofD.decEq (Inference.ProofD.ax₃ a a_1) (Inference.ProofD.ax₁ a_2 a_3) = isFalse ⋯
• Inference.instDecidableEqProofD.decEq (Inference.ProofD.ax₃ a a_1) (Inference.ProofD.ax₂ a_2 a_3 a_4) = isFalse ⋯
• Inference.instDecidableEqProofD.decEq (Inference.ProofD.ax₃ a a_1) (Inference.ProofD.ax₃ b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• Inference.instDecidableEqProofD.decEq (Inference.ProofD.ax₃ a a_1) (a_2.mp a_3) = isFalse ⋯
• Inference.instDecidableEqProofD.decEq (a.mp a_1) (Inference.ProofD.ax₁ a_2 a_3) = isFalse ⋯
• Inference.instDecidableEqProofD.decEq (a.mp a_1) (Inference.ProofD.ax₂ a_2 a_3 a_4) = isFalse ⋯
• Inference.instDecidableEqProofD.decEq (a.mp a_1) (Inference.ProofD.ax₃ a_2 a_3) = isFalse ⋯
• Inference.instDecidableEqProofD.decEq (a.mp a_1) (b.mp b_1) = if h : a = b then h ▸ have inst := Inference.instDecidableEqProofD.decEq a a; have inst := Inference.instDecidableEqProofD.decEq a_1 b_1; if h : a_1 = b_1 then h ▸ have inst := Inference.instDecidableEqProofD.decEq a_1 a_1; isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Inference.ProofD.stat (p : ProofD) : Option Stat

Equations

• (Inference.ProofD.ax₁ P Q).stat = some (P.imp (Q.imp P))
• (Inference.ProofD.ax₂ P Q R).stat = some ((P.imp (Q.imp R)).imp ((P.imp Q).imp (P.imp R)))
• (Inference.ProofD.ax₃ P Q).stat = some ((P.not.imp Q.not).imp (Q.imp P))
• (p₁.mp p₂).stat = do let __do_lift ← p₁.stat let __do_lift_1 ← p₂.stat match __do_lift, __do_lift_1 with | P.imp Q, P' => do guard (P = P') some Q | x, x_1 => none

class Inference.ProofD.WF (p : ProofD) : Prop

• h : ∃ (s : Stat), p.stat = some s

structure Inference.Proof (e : Stat) : Prop

• h : ∃ (p : ProofD), p.stat = some e

theorem Inference.ax₁ (P Q : Stat) : Proof (P.imp (Q.imp P))

theorem Inference.ax₂ (P Q R : Stat) : Proof ((P.imp (Q.imp R)).imp ((P.imp Q).imp (P.imp R)))

theorem Inference.ax₃ (P Q : Stat) : Proof ((P.not.imp Q.not).imp (Q.imp P))

theorem Inference.mp {P Q : Stat} (h₁ : Proof (P.imp Q)) (h₂ : Proof P) : Proof Q

theorem Inference.mp' {P Q : Stat} (h₁ : Proof P) (h₂ : Proof (P.imp Q)) : Proof Q

@[simp]

theorem Inference.imp_refl : Proof ((Stat.var 0).imp (Stat.var 0))

def Inference.Stat.subst (s : Stat) (i : ℕ) (s' : Stat) : Stat

Equations

• (Inference.Stat.var j).subst i s' = if j = i then s' else Inference.Stat.var j
• e.not.subst i s' = (e.subst i s').not
• (a.imp b).subst i s' = (a.subst i s').imp (b.subst i s')

def Inference.ProofD.subst (p : ProofD) (i : ℕ) (s : Stat) : ProofD

Equations

• (Inference.ProofD.ax₁ P Q).subst i s = Inference.ProofD.ax₁ (P.subst i s) (Q.subst i s)
• (Inference.ProofD.ax₂ P Q R).subst i s = Inference.ProofD.ax₂ (P.subst i s) (Q.subst i s) (R.subst i s)
• (Inference.ProofD.ax₃ P Q).subst i s = Inference.ProofD.ax₃ (P.subst i s) (Q.subst i s)
• (p₁.mp p₂).subst i s = (p₁.subst i s).mp (p₂.subst i s)

theorem Inference.stat_mp_eq_some_iff {p₁ p₂ : ProofD} {s : Stat} : (p₁.mp p₂).stat = some s ↔ ∃ (P : Stat), p₁.stat = some (P.imp s) ∧ p₂.stat = some P

theorem Inference.ProofD.stat_subst_eq_some_of {s s' : Stat} {i : ℕ} {p : ProofD} (h : p.stat = some s) : (p.subst i s').stat = some (s.subst i s')

theorem Inference.Proof.subst_of {s s' : Stat} {i : ℕ} (h : Proof s) : Proof (s.subst i s')

noncomputable def Inference.ProofD.shortest (p : ProofD) : ProofD

Equations

• p.shortest = Classical.epsilon fun (p₁ : Inference.ProofD) => p₁.stat = p.stat ∧ ∀ (p₂ : Inference.ProofD), p₂.stat = p.stat → sizeOf p₁ ≤ sizeOf p₂

theorem Inference.ProofD.shortest_spec {p : ProofD} : p.shortest.stat = p.stat ∧ ∀ (p' : ProofD), p'.stat = p.stat → sizeOf p.shortest ≤ sizeOf p'

@[simp]

theorem Inference.ProofD.stat_shortest {p : ProofD} : p.shortest.stat = p.stat

theorem Inference.Proof.exi_shortest {s : Stat} {h : Proof s} : ∃ (p₁ : ProofD), p₁.stat = some s ∧ ∀ (p₂ : ProofD), p₂.stat = some s → sizeOf p₁ ≤ sizeOf p₂

theorem Inference.Proof.exi_wf {s : Stat} {h : Proof s} : ∃ (p : ProofD), p.WF ∧ p.stat = some s

def Inference.Stat.eval (s : Stat) (f : ℕ → Bool) : Bool

Equations

• (Inference.Stat.var j).eval f = f j
• e.not.eval f = !e.eval f
• (a.imp b).eval f = decide ((!a.eval f) = true ∨ b.eval f = true)

def Inference.Stat.Tauto (s : Stat) : Prop

Equations

• s.Tauto = ∀ (f : ℕ → Bool), s.eval f = true

theorem Inference.tauto_of_proof {s : Stat} (h : Proof s) : s.Tauto

@[simp]

theorem Inference.not_proof_var {i : ℕ} : ¬Proof (Stat.var i)

@[simp]

theorem Inference.not_proof_not_var {i : ℕ} : ¬Proof (Stat.var i).not

def Inference.Stat.true : Stat

Equations

• Inference.Stat.true = (Inference.Stat.var 0).imp (Inference.Stat.var 0)

def Inference.Stat.false : Stat

Equations

• Inference.Stat.false = Inference.Stat.true.not

@[simp]

theorem Inference.proof_true : Proof Stat.true

@[simp]

theorem Inference.tauto_true : Stat.true.Tauto