feat: Propositional

Logic/Propositional/Basic/Calculus.lean

@@ -0,0 +1,140 @@
+import Logic.Propositional.Basic.Formula
+import Logic.Logic.System
+
+namespace LO
+
+namespace Propositional
+
+variable {α : Type*} [DecidableEq α]
+
+abbrev Sequent (α : Type*) := Finset (Formula α)
+
+inductive DerivationCR (P : Formula α → Prop) : Sequent α → Type _
+| axL   : ∀ (Δ : Sequent α) (a : α),
+    Formula.atom a ∈ Δ → Formula.natom a ∈ Δ → DerivationCR P Δ
+| verum : ∀ (Δ : Sequent α), ⊤ ∈ Δ → DerivationCR P Δ
+| or    : ∀ (Δ : Sequent α) (p q : Formula α),
+    DerivationCR P (insert p $ insert q Δ) → DerivationCR P (insert (p ⋎ q) Δ)
+| and   : ∀ (Δ : Sequent α) (p q : Formula α),
+    DerivationCR P (insert p Δ) → DerivationCR P (insert q Δ) → DerivationCR P (insert (p ⋏ q) Δ)
+| cut   : ∀ (Δ Γ : Sequent α) (p : Formula α), P p →
+    DerivationCR P (insert p Δ) → DerivationCR P (insert (~p) Γ) → DerivationCR P (Δ ∪ Γ)
+
+scoped notation :45 "⊢ᴾᶜ[" P "] " Γ:45 => DerivationCR P Γ
+
+abbrev Derivation : Sequent α → Type _ := DerivationCR (fun _ => False)
+
+scoped prefix:45 "⊢ᴾᵀ " => Derivation
+
+abbrev DerivationC : Sequent α → Type _ := DerivationCR (fun _ => True)
+
+scoped prefix:45 "⊢ᴾᶜ " => DerivationC
+
+abbrev DerivationClx (c : ℕ) : Sequent α → Type _ := DerivationCR (·.complexity < c)
+
+scoped notation :45 "⊢ᴾᶜ[< " c "] " Γ:45 => DerivationClx c Γ
+
+namespace DerivationCR
+
+variable {P : Formula α → Prop} {Δ Δ₁ Δ₂ Γ : Sequent α}
+
+def length : {Δ : Sequent α} → DerivationCR P Δ → ℕ
+  | _, axL _ _ _ _       => 0
+  | _, verum Δ _         => 0
+  | _, or _ _ _ d        => d.length.succ
+  | _, and _ _ _ dp dq   => (max dp.length dq.length).succ
+  | _, cut _ _ _ _ dp dn => (max dp.length dn.length).succ
+
+section
+
+@[simp] lemma length_axL {a : α} (hpos : Formula.atom a ∈ Δ) (hneg : Formula.natom a ∈ Δ) :
+  (axL (P := P) Δ a hpos hneg).length = 0 := rfl
+
+@[simp] lemma length_verum (h : ⊤ ∈ Δ) : (verum (P := P) Δ h).length = 0 := rfl
+
+@[simp] lemma length_and {p q} (dp : ⊢ᴾᶜ[P] insert p Δ) (dq : ⊢ᴾᶜ[P] insert q Δ) : (and Δ p q dp dq).length = (max dp.length dq.length).succ := rfl
+
+@[simp] lemma length_or {p q} (d : ⊢ᴾᶜ[P] (insert p $ insert q Δ)) : (or Δ p q d).length = d.length.succ := rfl
+
+@[simp] lemma length_cut {p} (hp : P p) (dp : ⊢ᴾᶜ[P] insert p Δ) (dn : ⊢ᴾᶜ[P] insert (~p) Γ) :
+  (cut _ _ p hp dp dn).length = (max dp.length dn.length).succ := rfl
+
+end
+
+protected def cast (d : ⊢ᴾᶜ[P] Δ) (e : Δ = Γ) : ⊢ᴾᶜ[P] Γ := cast (by simp[HasVdash.vdash, e]) d
+
+@[simp] lemma length_cast (d : ⊢ᴾᶜ[P] Δ) (e : Δ = Γ) : (d.cast e).length = d.length := by
+  rcases e with rfl; simp[DerivationCR.cast]
+
+def weakening : ∀ {Δ}, ⊢ᴾᶜ[P] Δ → ∀ {Γ : Sequent α}, Δ ⊆ Γ → ⊢ᴾᶜ[P] Γ
+  | _, axL Δ a hrel hnrel, Γ,   h => axL Γ a (h hrel) (h hnrel)
+  | _, verum Δ htop,         Γ, h => verum Γ (h htop)
+  | _, or Δ p q d,           Γ, h =>
+      have : ⊢ᴾᶜ[P] (insert p $ insert q Γ) :=
+        weakening d (Finset.insert_subset_insert p $ Finset.insert_subset_insert q (Finset.insert_subset_iff.mp h).2)
+      have : ⊢ᴾᶜ[P] insert (p ⋎ q) Γ := or Γ p q this
+      this.cast (by simp; exact (Finset.insert_subset_iff.mp h).1)
+  | _, and Δ p q dp dq,      Γ, h =>
+      have dp : ⊢ᴾᶜ[P] insert p Γ := dp.weakening (Finset.insert_subset_insert p (Finset.insert_subset_iff.mp h).2)
+      have dq : ⊢ᴾᶜ[P] insert q Γ := dq.weakening (Finset.insert_subset_insert q (Finset.insert_subset_iff.mp h).2)
+      have : ⊢ᴾᶜ[P] insert (p ⋏ q) Γ := and Γ p q dp dq
+      this.cast (by simp; exact (Finset.insert_subset_iff.mp h).1)
+  | _, cut Δ₁ Δ₂ p hp d₁ d₂, Γ, h =>
+      have d₁ : ⊢ᴾᶜ[P] insert p Γ := d₁.weakening (Finset.insert_subset_insert _ (Finset.union_subset_left h))
+      have d₂ : ⊢ᴾᶜ[P] insert (~p) Γ := d₂.weakening (Finset.insert_subset_insert _ (Finset.union_subset_right h))
+      (cut Γ Γ p hp d₁ d₂).cast (by simp)
+
+@[simp] lemma length_weakening {Δ} (d : ⊢ᴾᶜ[P] Δ) {Γ : Sequent α} (h : Δ ⊆ Γ) : (d.weakening h).length = d.length :=
+  by induction d generalizing Γ <;> simp[*, weakening]
+
+def or' {p q : Formula α} (h : p ⋎ q ∈ Δ) (d : ⊢ᴾᶜ[P] (insert p $ insert q $ Δ.erase (p ⋎ q))) : ⊢ᴾᶜ[P] Δ :=
+  (or _ p q d).cast (by simp[Finset.insert_erase h])
+
+def and' {p q : Formula α} (h : p ⋏ q ∈ Δ)
+    (dp : ⊢ᴾᶜ[P] insert p (Δ.erase (p ⋏ q))) (dq : ⊢ᴾᶜ[P] insert q (Δ.erase (p ⋏ q))) : ⊢ᴾᶜ[P] Δ :=
+  (and _ p q dp dq).cast (by simp[Finset.insert_erase h])
+
+def em {p : Formula α} {Δ : Sequent α} (hpos : p ∈ Δ) (hneg : ~p ∈ Δ) : ⊢ᴾᶜ[P] Δ := by
+  induction p using Formula.rec' generalizing Δ
+  case hverum           => exact verum Δ hpos
+  case hfalsum          => exact verum Δ hneg
+  case hrel a           => exact axL Δ a hpos hneg
+  case hnrel a          => exact axL Δ a hneg hpos
+  case hand p q ihp ihq =>
+    simp at hneg
+    exact or' hneg (and' (p := p) (q := q) (by simp[hpos])
+      (ihp (by simp) (by simp; exact Or.inr $ Formula.ne_of_ne_complexity (by simp)))
+      (ihq (by simp) (by simp; exact Or.inr $ Formula.ne_of_ne_complexity (by simp))))
+  case hor p q ihp ihq  =>
+    simp at hneg
+    exact or' hpos (and' (p := ~p) (q := ~q) (by simp[hneg])
+      (ihp (by simp; exact Or.inr $ Formula.ne_of_ne_complexity (by simp)) (by simp))
+      (ihq (by simp; exact Or.inr $ Formula.ne_of_ne_complexity (by simp)) (by simp)))
+
+end DerivationCR
+
+structure DerivationCRWA (P : Formula α → Prop) (T : Theory α) (Δ : Sequent α) where
+  leftHand : Finset (Formula α)
+  hleftHand : (leftHand : Set (Formula α)) ⊆ (~·) '' T
+  derivation : ⊢ᴾᶜ[P] Δ ∪ leftHand
+
+scoped notation :45 T " ⊢ᴾᶜ[" P "] " Γ:45 => DerivationCRWA P T Γ
+
+abbrev DerivationCWA (T : Theory α) (Δ : Sequent α) := DerivationCRWA (fun _ => True) T Δ
+
+scoped infix:45 " ⊢' " => DerivationCWA
+
+instance Proof : System (Formula α) where
+  Bew := fun T σ => T ⊢' {σ}
+  axm := fun {f σ} hσ =>
+    { leftHand := {~σ}
+      hleftHand := by simp[hσ]
+      derivation := DerivationCR.em (p := σ) (by simp) (by simp) }
+  weakening' := fun {T U} f h b =>
+    { leftHand := b.leftHand,
+      hleftHand := Set.Subset.trans b.hleftHand (Set.image_subset _ h),
+      derivation := b.derivation }
+
+end Propositional
+
+end LO

Logic/Propositional/Basic/Formula.lean

@@ -18,12 +18,12 @@ variable
   {α : Type u} {α₁ : Type u₁} {α₂ : Type u₂} {α₃ : Type u₃}
 
 def neg : Formula α → Formula α
-  | verum    => falsum
-  | falsum   => verum
+  | verum   => falsum
+  | falsum  => verum
   | atom a  => natom a
   | natom a => atom a
-  | and p q  => or (neg p) (neg q)
-  | or p q   => and (neg p) (neg q)
+  | and p q => or (neg p) (neg q)
+  | or p q  => and (neg p) (neg q)
 
 lemma neg_neg (p : Formula α) : neg (neg p) = p :=
   by induction p <;> simp[*, neg]
@@ -36,8 +36,155 @@ instance : LogicSymbol (Formula α) where
   top := verum
   bot := falsum
 
+section ToString
+
+variable [ToString α]
+
+def toStr : Formula α → String
+  | ⊤       => "\\top"
+  | ⊥       => "\\bot"
+  | atom a  => "{" ++ toString a ++ "}"
+  | natom a => "\\lnot {" ++ toString a ++ "}"
+  | p ⋏ q   => "\\left(" ++ toStr p ++ " \\land " ++ toStr q ++ "\\right)"
+  | p ⋎ q   => "\\left(" ++ toStr p ++ " \\lor "  ++ toStr q ++ "\\right)"
+
+instance : Repr (Formula α) := ⟨fun t _ => toStr t⟩
+
+instance : ToString (Formula α) := ⟨toStr⟩
+
+end ToString
+
+@[simp] lemma neg_top : ~(⊤ : Formula α) = ⊥ := rfl
+
+@[simp] lemma neg_bot : ~(⊥ : Formula α) = ⊤ := rfl
+
+@[simp] lemma neg_atom (a : α) : ~(atom a) = natom a := rfl
+
+@[simp] lemma neg_natom (a : α) : ~(natom a) = atom a := rfl
+
+@[simp] lemma neg_and (p q : Formula α) : ~(p ⋏ q) = ~p ⋎ ~q := rfl
+
+@[simp] lemma neg_or (p q : Formula α) : ~(p ⋎ q) = ~p ⋏ ~q := rfl
+
+@[simp] lemma neg_neg' (p : Formula α) : ~~p = p := neg_neg p
+
+@[simp] lemma neg_inj (p q : Formula α) : ~p = ~q ↔ p = q := by
+  constructor
+  · intro h; simpa using congr_arg (~·) h
+  · exact congr_arg _
+
+lemma neg_eq (p : Formula α) : ~p = neg p := rfl
+
+lemma imp_eq (p q : Formula α) : p ⟶ q = ~p ⋎ q := rfl
+
+lemma iff_eq (p q : Formula α) : p ⟷ q = (~p ⋎ q) ⋏ (~q ⋎ p) := rfl
+
+@[simp] lemma and_inj (p₁ q₁ p₂ q₂ : Formula α) : p₁ ⋏ p₂ = q₁ ⋏ q₂ ↔ p₁ = q₁ ∧ p₂ = q₂ :=
+by simp[Wedge.wedge]
+
+@[simp] lemma or_inj (p₁ q₁ p₂ q₂ : Formula α) : p₁ ⋎ p₂ = q₁ ⋎ q₂ ↔ p₁ = q₁ ∧ p₂ = q₂ :=
+by simp[Vee.vee]
+
+def complexity : Formula α → ℕ
+| ⊤       => 0
+| ⊥       => 0
+| atom _  => 0
+| natom _ => 0
+| p ⋏ q   => max p.complexity q.complexity + 1
+| p ⋎ q   => max p.complexity q.complexity + 1
+
+@[simp] lemma complexity_top : complexity (⊤ : Formula α) = 0 := rfl
+
+@[simp] lemma complexity_bot : complexity (⊥ : Formula α) = 0 := rfl
+
+@[simp] lemma complexity_rel (a : α) : complexity (atom a) = 0 := rfl
+
+@[simp] lemma complexity_nrel (a : α) : complexity (natom a) = 0 := rfl
+
+@[simp] lemma complexity_and (p q : Formula α) : complexity (p ⋏ q) = max p.complexity q.complexity + 1 := rfl
+@[simp] lemma complexity_and' (p q : Formula α) : complexity (and p q) = max p.complexity q.complexity + 1 := rfl
+
+@[simp] lemma complexity_or (p q : Formula α) : complexity (p ⋎ q) = max p.complexity q.complexity + 1 := rfl
+@[simp] lemma complexity_or' (p q : Formula α) : complexity (or p q) = max p.complexity q.complexity + 1 := rfl
+
+@[elab_as_elim]
+def cases' {C : Formula α → Sort w}
+    (hverum  : C ⊤)
+    (hfalsum : C ⊥)
+    (hrel    : ∀ a : α, C (atom a))
+    (hnrel   : ∀ a : α, C (natom a))
+    (hand    : ∀ (p q : Formula α), C (p ⋏ q))
+    (hor     : ∀ (p q : Formula α), C (p ⋎ q)) : (p : Formula α) → C p
+  | ⊤       => hverum
+  | ⊥       => hfalsum
+  | atom a  => hrel a
+  | natom a => hnrel a
+  | p ⋏ q   => hand p q
+  | p ⋎ q   => hor p q
+
+@[elab_as_elim]
+def rec' {C : Formula α → Sort w}
+  (hverum  : C ⊤)
+  (hfalsum : C ⊥)
+  (hrel    : ∀ a : α, C (atom a))
+  (hnrel   : ∀ a : α, C (natom a))
+  (hand    : ∀ (p q : Formula α), C p → C q → C (p ⋏ q))
+  (hor     : ∀ (p q : Formula α), C p → C q → C (p ⋎ q)) : (p : Formula α) → C p
+  | ⊤       => hverum
+  | ⊥       => hfalsum
+  | atom a  => hrel a
+  | natom a => hnrel a
+  | p ⋏ q   => hand p q (rec' hverum hfalsum hrel hnrel hand hor p) (rec' hverum hfalsum hrel hnrel hand hor q)
+  | p ⋎ q   => hor p q (rec' hverum hfalsum hrel hnrel hand hor p) (rec' hverum hfalsum hrel hnrel hand hor q)
+
+@[simp] lemma complexity_neg (p : Formula α) : complexity (~p) = complexity p :=
+  by induction p using rec' <;> simp[*]
+
+section Decidable
+
+variable [DecidableEq α]
+
+def hasDecEq : (p q : Formula α) → Decidable (p = q)
+  | ⊤,       q => by cases q using cases' <;>
+      { simp; try { exact isFalse not_false }; try { exact isTrue trivial } }
+  | ⊥,       q => by cases q using cases' <;>
+      { simp; try { exact isFalse not_false }; try { exact isTrue trivial } }
+  | atom a,  q => by
+      cases q using cases' <;> try { simp; exact isFalse not_false }
+      simp; exact decEq _ _
+  | natom a, q => by
+      cases q using cases' <;> try { simp; exact isFalse not_false }
+      simp; exact decEq _ _
+  | p ⋏ q,   r => by
+      cases r using cases' <;> try { simp; exact isFalse not_false }
+      case hand p' q' =>
+        exact match hasDecEq p p' with
+        | isTrue hp =>
+          match hasDecEq q q' with
+          | isTrue hq  => isTrue (hp ▸ hq ▸ rfl)
+          | isFalse hq => isFalse (by simp[hp, hq])
+        | isFalse hp => isFalse (by simp[hp])
+  | p ⋎ q,   r => by
+      cases r using cases' <;> try { simp; exact isFalse not_false }
+      case hor p' q' =>
+        exact match hasDecEq p p' with
+        | isTrue hp =>
+          match hasDecEq q q' with
+          | isTrue hq  => isTrue (hp ▸ hq ▸ rfl)
+          | isFalse hq => isFalse (by simp[hp, hq])
+        | isFalse hp => isFalse (by simp[hp])
+
+instance : DecidableEq (Formula α) := hasDecEq
+
+end Decidable
+
+lemma ne_of_ne_complexity {p q : Formula α} (h : p.complexity ≠ q.complexity) : p ≠ q :=
+  by rintro rfl; contradiction
+
 end Formula
 
+abbrev Theory (α : Type*) := Set (Formula α)
+
 end Propositional
 
 end LO

Logic/Propositional/Basic/Semantics.lean

@@ -0,0 +1,27 @@
+import Logic.Propositional.Basic.Formula
+import Logic.Logic.System
+
+namespace LO
+
+namespace Propositional
+
+variable (α : Type*)
+
+structure Structure (α : Type*) where
+  val : α → Prop
+
+namespace Formula
+
+def val (s : Structure α) : Formula α → Prop
+  | atom a  => s.val a
+  | natom a => ¬s.val a
+  | ⊤       => True
+  | ⊥       => False
+  | p ⋏ q   => p.val s ∧ q.val s
+  | p ⋎ q   => p.val s ∨ q.val s
+
+end Formula
+
+end Propositional
+
+end LO