Documentation

Foundation.Propositional.Decidable

@[simp]

theorem LO.Propositional.NNFormula.ne_neg {α : Type u_1} (φ : NNFormula α) :

∼φ ≠ φ

inductive LO.Propositional.NNFormula.IsAtomic {α : Type u_1} :

NNFormula α → Prop

atom {α : Type u_1} (a : α) : (NNFormula.atom a).IsAtomic
natom {α : Type u_1} (a : α) : (NNFormula.natom a).IsAtomic

Instances For

LO.Propositional.NNFormula.instDecidablePredIsAtomic

@[simp]

theorem LO.Propositional.NNFormula.IsAtomic.not_cons_verum {α : Type u_1} :

@[simp]

theorem LO.Propositional.NNFormula.IsAtomic.not_cons_falsum {α : Type u_1} :

@[simp]

theorem LO.Propositional.NNFormula.IsAtomic.not_cons_and {α : Type u_1} {φ ψ : NNFormula α} :

¬(φ ⋏ ψ).IsAtomic

@[simp]

theorem LO.Propositional.NNFormula.IsAtomic.not_cons_or {α : Type u_1} {φ ψ : NNFormula α} :

¬(φ ⋎ ψ).IsAtomic

instance LO.Propositional.NNFormula.instDecidablePredIsAtomic {α : Type u_1} :

DecidablePred IsAtomic

Equations

def LO.Propositional.NNFormula.weight {α : Type u_1} :

NNFormula α → ℕ

Equations

(LO.Propositional.NNFormula.atom a).weight = 0
(LO.Propositional.NNFormula.natom a).weight = 0
LO.Propositional.NNFormula.verum.weight = 1
LO.Propositional.NNFormula.falsum.weight = 1
(a.and a_1).weight = a.weight + a_1.weight + 1
(a.or a_1).weight = a.weight + a_1.weight + 1

@[simp]

theorem LO.Propositional.NNFormula.weight_atom {α : Type u_1} (a : α) :

(atom a).complexity = 0

@[simp]

theorem LO.Propositional.NNFormula.weight_natom {α : Type u_1} (a : α) :

(natom a).complexity = 0

@[simp]

theorem LO.Propositional.NNFormula.weight_verum {α : Type u_1} :

@[simp]

theorem LO.Propositional.NNFormula.weight_falsum {α : Type u_1} :

@[simp]

theorem LO.Propositional.NNFormula.weight_and {α : Type u_1} (φ ψ : NNFormula α) :

(φ ⋏ ψ).weight = φ.weight + ψ.weight + 1

@[simp]

theorem LO.Propositional.NNFormula.weight_or {α : Type u_1} (φ ψ : NNFormula α) :

(φ ⋎ ψ).weight = φ.weight + ψ.weight + 1

def LO.Propositional.Sequent.weight {α : Type u_1} (Γ : Sequent α) :

Equations

Γ.weight = (List.map LO.Propositional.NNFormula.weight Γ).sum

@[simp]

theorem LO.Propositional.Sequent.weight_nil {α : Type u_1} :

@[simp]

theorem LO.Propositional.Sequent.weight_cons {α : Type u_1} (φ : NNFormula α) (Γ : Sequent α) :

weight (φ :: Γ) = φ.weight + Γ.weight

@[simp]

theorem LO.Propositional.Sequent.weight_append {α : Type u_1} (Γ Δ : Sequent α) :

(Γ ++ Δ).weight = Γ.weight + Δ.weight

theorem LO.Propositional.Sequent.weight_le_weight_of_mem {α : Type u_1} {φ : NNFormula α} {Γ : Sequent α} (h : φ ∈ Γ) :

φ.weight ≤ Γ.weight

theorem LO.Propositional.Sequent.weight_remove {α : Type u_1} [DecidableEq α] (Γ : Sequent α) (φ : NNFormula α) :

weight (List.remove φ Γ) = Γ.weight - List.count φ Γ * φ.weight

theorem LO.Propositional.Sequent.weight_remove_le_of_mem {α : Type u_1} [DecidableEq α] {φ : NNFormula α} {Γ : Sequent α} (h : φ ∈ Γ) :

weight (List.remove φ Γ) ≤ Γ.weight - φ.weight

def LO.Propositional.Sequent.IsAtomic {α : Type u_1} (Γ : Sequent α) :

Equations

Γ.IsAtomic = ∀ φ ∈ Γ, φ.IsAtomic

Instances For

LO.Propositional.Sequent.instDecidablePredIsAtomic

@[simp]

theorem LO.Propositional.Sequent.IsAtomic.nil {α : Type u_1} :

instance LO.Propositional.Sequent.instDecidablePredIsAtomic {α : Type u_1} :

DecidablePred IsAtomic

Equations

LO.Propositional.Sequent.instDecidablePredIsAtomic = List.decidableBAll LO.Propositional.NNFormula.IsAtomic

@[simp]

theorem LO.Propositional.Sequent.IsAtomic.cons_atom_iff {α : Type u_1} {Γ : Sequent α} {φ : NNFormula α} :

IsAtomic (φ :: Γ) ↔ φ.IsAtomic ∧ Γ.IsAtomic

def LO.Propositional.Sequent.chooseNonAtomic {α : Type u_1} (Γ : Sequent α) (H : ¬Γ.IsAtomic) :

Equations

Γ.chooseNonAtomic H = List.choose (fun (φ : LO.Propositional.NNFormula α) => ¬φ.IsAtomic) Γ ⋯

@[simp]

theorem LO.Propositional.Sequent.chooseNonAtomic_mem {α : Type u_1} {Γ : Sequent α} (h : ¬Γ.IsAtomic) :

Γ.chooseNonAtomic h ∈ Γ

@[simp]

theorem LO.Propositional.Sequent.chooseNonAtomic_property {α : Type u_1} (Γ : Sequent α) (h : ¬Γ.IsAtomic) :

¬(Γ.chooseNonAtomic h).IsAtomic

@[reducible, inline]

abbrev LO.Propositional.Sequents (α : Type u_2) :

Type u_2

Equations

LO.Propositional.Sequents α = List (LO.Propositional.Sequent α)

def LO.Propositional.Sequents.weight {α : Type u_1} (S : Sequents α) :

Equations

S.weight = Option.casesOn (List.map LO.Propositional.Sequent.weight S).max? 0 Nat.succ

@[simp]

theorem LO.Propositional.Sequents.weight_nil {α : Type u_1} :

@[simp]

theorem LO.Propositional.Sequents.weight_eq_zero_iff_eq_nil {α : Type u_1} {S : Sequents α} :

S.weight = 0 ↔ S = []

theorem LO.Propositional.Sequents.weight_eq_succ_iff {α : Type u_1} {n : ℕ} {S : Sequents α} :

S.weight = n + 1 ↔ ∃ Γ ∈ S, Γ.weight = n ∧ ∀ Δ ∈ S, Δ.weight ≤ n

theorem LO.Propositional.Sequents.weight_eq_of_mem_max {α : Type u_1} {S : Sequents α} {m : ℕ} (hm : m ∈ (List.map Sequent.weight S).max?) :

S.weight = m + 1

theorem LO.Propositional.Sequents.weight_lt_weight_of {α : Type u_1} {S₁ S₂ : Sequents α} {Γ : Sequent α} (hΓ : Γ ∈ S₂) (h : ∀ Δ ∈ S₁, Δ.weight < Γ.weight) :

S₁.weight < S₂.weight

@[reducible, inline]

abbrev LO.Propositional.Derivations {α : Type u_1} (T : Theory α) (S : Sequents α) :

Type u_1

Equations

LO.Propositional.Derivations T S = ((Γ : LO.Propositional.Sequent α) → Γ ∈ S → T ⟹ Γ)

@[reducible, inline]

abbrev LO.Propositional.Derivations! {α : Type u_1} (T : Theory α) (S : Sequents α) :

Equations

LO.Propositional.Derivations! T S = ∀ Γ ∈ S, T ⟹! Γ

def LO.Propositional.Derivations.ofSubset {α : Type u_1} {T : Theory α} {S₁ S₂ : Sequents α} (ss : S₁ ⊆ S₂) :

Derivations T S₂ → Derivations T S₁

Equations

LO.Propositional.Derivations.ofSubset ss d Γ hΓ = d Γ ⋯

def LO.Propositional.Derivations.nil {α : Type u_1} {T : Theory α} :

Derivations T []

Equations

LO.Propositional.Derivations.nil x✝ h = ⋯.elim

@[simp]

theorem LO.Propositional.Derivations!.nil {α✝ : Type u_2} {T : Theory α✝} :

Derivations! T []

def LO.Propositional.Sequent.IsClosed {α : Type u_1} (Γ : Sequent α) :

Equations

Γ.IsClosed = ∃ φ ∈ Γ, ∼φ ∈ Γ

Instances For

LO.Propositional.instDecidablePredSequentIsClosedOfDecidableEq

theorem LO.Propositional.Sequent.IsClosed.cons_iff {α : Type u_1} {φ : NNFormula α} {Γ : Sequent α} :

IsClosed (φ :: Γ) ↔ ∼φ ∈ Γ ∨ Γ.IsClosed

instance LO.Propositional.instDecidablePredSequentIsClosedOfDecidableEq {α : Type u_1} [DecidableEq α] :

DecidablePred Sequent.IsClosed

Equations

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

def LO.Propositional.Sequent.IsClosed.choose {α : Type u_1} [DecidableEq α] (Γ : Sequent α) :

Γ.IsClosed → { φ : NNFormula α // φ ∈ Γ ∧ ∼φ ∈ Γ }

Equations

LO.Propositional.Sequent.IsClosed.choose [] h = ⋯.elim
LO.Propositional.Sequent.IsClosed.choose (φ :: Γ) h = if hn : ∼φ ∈ Γ then ⟨φ, ⋯⟩ else have this := ⋯; match LO.Propositional.Sequent.IsClosed.choose Γ this with | ⟨ψ, hψ⟩ => ⟨ψ, ⋯⟩

def LO.Propositional.Derivation.ofIsClosed {α : Type u_1} [DecidableEq α] {T : Theory α} {Γ : Sequent α} (h : Γ.IsClosed) :

T ⟹ Γ

Equations

LO.Propositional.Derivation.ofIsClosed h = match LO.Propositional.Sequent.IsClosed.choose Γ h with | ⟨φ, ⋯⟩ => LO.Propositional.Derivation.em h hn

@[reducible, inline]

abbrev LO.Propositional.Sequent.IsOpen {α : Type u_1} (Γ : Sequent α) :

Equations

Γ.IsOpen = (Γ.IsAtomic ∧ ¬Γ.IsClosed)

Instances For

LO.Propositional.instDecidablePredSequentIsOpenOfDecidableEq

instance LO.Propositional.instDecidablePredSequentIsOpenOfDecidableEq {α : Type u_1} [DecidableEq α] :

DecidablePred Sequent.IsOpen

Equations

LO.Propositional.instDecidablePredSequentIsOpenOfDecidableEq = inferInstance

theorem LO.Propositional.Sequent.IsOpen.not_tautology {α : Type u_1} {Γ : Sequent α} (h : Γ.IsOpen) :

¬Γ.IsTautology

def LO.Propositional.Sequents.IsClosed {α : Type u_1} (S : Sequents α) :

Equations

S.IsClosed = ∀ Γ ∈ S, Γ.IsClosed

Instances For

LO.Propositional.instDecidablePredSequentsIsClosedOfDecidableEq

instance LO.Propositional.instDecidablePredSequentsIsClosedOfDecidableEq {α : Type u_1} [DecidableEq α] :

DecidablePred Sequents.IsClosed

Equations

LO.Propositional.instDecidablePredSequentsIsClosedOfDecidableEq = List.decidableBAll LO.Propositional.Sequent.IsClosed

def LO.Propositional.Sequent.reduction {α : Type u_1} [DecidableEq α] {Γ : Sequent α} (h : ¬Γ.IsAtomic) :

Equations

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

theorem LO.Propositional.Sequent.reduction_verum {α : Type u_1} {Γ : Sequent α} [DecidableEq α] {h : ¬Γ.IsAtomic} (H : Γ.chooseNonAtomic h = ⊤) :

reduction h = []

theorem LO.Propositional.Sequent.reduction_falsum {α : Type u_1} {Γ : Sequent α} [DecidableEq α] {h : ¬Γ.IsAtomic} (H : Γ.chooseNonAtomic h = ⊥) :

reduction h = [List.remove ⊥ Γ]

theorem LO.Propositional.Sequent.reduction_and {α : Type u_1} {Γ : Sequent α} [DecidableEq α] {φ ψ : NNFormula α} {h : ¬Γ.IsAtomic} (H : Γ.chooseNonAtomic h = φ ⋏ ψ) :

reduction h = [(List.remove (φ ⋏ ψ) Γ).concat φ, (List.remove (φ ⋏ ψ) Γ).concat ψ]

theorem LO.Propositional.Sequent.reduction_or {α : Type u_1} {Γ : Sequent α} [DecidableEq α] {φ ψ : NNFormula α} {h : ¬Γ.IsAtomic} (H : Γ.chooseNonAtomic h = φ ⋎ ψ) :

reduction h = [((List.remove (φ ⋎ ψ) Γ).concat φ).concat ψ]

theorem LO.Propositional.Sequent.weight_lt_weight_of_mem_reduction {α : Type u_1} {Γ Δ : Sequent α} [DecidableEq α] {h : ¬Γ.IsAtomic} :

Δ ∈ reduction h → Δ.weight < Γ.weight

def LO.Propositional.Derivation.ofReduction {α : Type u_1} [DecidableEq α] {T : Theory α} {Γ : Sequent α} {hΓ : ¬Γ.IsAtomic} (d : Derivations T (Sequent.reduction hΓ)) :

T ⟹ Γ

Equations

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

theorem LO.Propositional.Derivation.toReduction {α : Type u_1} [DecidableEq α] {T : Theory α} {Γ : Sequent α} (hΓ : ¬Γ.IsAtomic) (d : T ⟹! Γ) :

Derivations! T (Sequent.reduction hΓ)

@[reducible, inline]

abbrev LO.Propositional.Sequents.Refuted {α : Type u_1} (S : Sequents α) :

Equations

S.Refuted = ∃ Γ ∈ S, Γ.IsOpen

Instances For

LO.Propositional.instDecidablePredSequentsRefutedOfDecidableEq

theorem LO.Propositional.Sequents.Refuted.not_iff {α : Type u_1} {S : Sequents α} :

¬S.Refuted ↔ ∀ Γ ∈ S, Γ.IsAtomic → Γ.IsClosed

instance LO.Propositional.instDecidablePredSequentsRefutedOfDecidableEq {α : Type u_1} [DecidableEq α] :

DecidablePred Sequents.Refuted

Equations

LO.Propositional.instDecidablePredSequentsRefutedOfDecidableEq = List.decidableBEx LO.Propositional.Sequent.IsOpen

def LO.Propositional.Sequents.reduction {α : Type u_1} [DecidableEq α] (S : Sequents α) :

Equations

S.reduction = List.flatMap (fun (Γ : LO.Propositional.Sequent α) => if h : Γ.IsAtomic then [] else LO.Propositional.Sequent.reduction h) S

theorem LO.Propositional.Sequent.reduction_sublist {α : Type u_1} [DecidableEq α] {Γ : Sequent α} (hΓ : ¬Γ.IsAtomic) {S : Sequents α} (h : Γ ∈ S) :

List.Sublist (reduction hΓ) S.reduction

def LO.Propositional.Derivations.ofReduction {α : Type u_1} {T : Theory α} [DecidableEq α] {S : Sequents α} (hS : ¬S.Refuted) (d : Derivations T S.reduction) :

Derivations T S

Equations

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

theorem LO.Propositional.Derivations.toReduction {α : Type u_1} {T : Theory α} [DecidableEq α] {S : Sequents α} (d : Derivations! T S) :

Derivations! T S.reduction

theorem LO.Propositional.Sequents.reduction_weight_lt_weight {α : Type u_1} [DecidableEq α] (S : Sequents α) (h : S ≠ []) :

S.reduction.weight < S.weight

inductive LO.Propositional.Derivations.Dec {α : Type u_1} :

Sequents α → Type u_1

provable {α : Type u_1} {S : Sequents α} : Derivations ∅ S → Dec S
unprovable {α : Type u_1} {S : Sequents α} (Γ : Sequent α) : Γ ∈ S → ¬Γ.IsTautology → Dec S

def LO.Propositional.Derivations.Dec.ofReduction {α : Type u_1} [DecidableEq α] {S : Sequents α} (hS : ¬S.Refuted) :

Dec S.reduction → Dec S

Equations

One or more equations did not get rendered due to their size.
LO.Propositional.Derivations.Dec.ofReduction hS (LO.Propositional.Derivations.Dec.provable d) = LO.Propositional.Derivations.Dec.provable (LO.Propositional.Derivations.ofReduction hS d)

@[irreducible]

def LO.Propositional.Sequents.dec {α : Type u_1} [DecidableEq α] (S : Sequents α) :

Derivations.Dec S

Equations

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

instance LO.Propositional.instDecidablePredSequentIsTautologyOfDecidableEq {α : Type u_1} [DecidableEq α] :

DecidablePred fun (Γ : Sequent α) => Γ.IsTautology

Equations

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

instance LO.Propositional.instDecidablePredNNFormulaIsTautologyOfDecidableEq {α : Type u_1} [DecidableEq α] :

DecidablePred fun (φ : NNFormula α) => φ.IsTautology

Equations

LO.Propositional.instDecidablePredNNFormulaIsTautologyOfDecidableEq x✝ = inferInstance