Skip to content

Commit

Permalink
refactor(IntProp): Remove flexible simp in Hetring Semantics
Browse files Browse the repository at this point in the history
  • Loading branch information
SnO2WMaN committed Jan 1, 2025
1 parent 830d76e commit 76ff67f
Show file tree
Hide file tree
Showing 2 changed files with 16 additions and 16 deletions.
22 changes: 11 additions & 11 deletions Foundation/IntProp/Heyting/Semantics.lean
Original file line number Diff line number Diff line change
Expand Up @@ -87,7 +87,10 @@ instance : Semantics.And (HeytingSemantics α) := ⟨fun {ℍ φ ψ} ↦ by simp
@[simp] lemma val_iff {φ ψ : Formula α} : ℍ ⊧ φ ⭤ ψ ↔ (ℍ ⊧ₕ φ) = (ℍ ⊧ₕ ψ) := by
simp [LogicalConnective.iff, antisymm_iff]

lemma val_not (φ : Formula α) : ℍ ⊧ ∼φ ↔ (ℍ ⊧ₕ φ) = ⊥ := by simp [val_def]; rw [←HeytingAlgebra.himp_bot, himp_eq_top_iff, le_bot_iff]; rfl
lemma val_not (φ : Formula α) : ℍ ⊧ ∼φ ↔ (ℍ ⊧ₕ φ) = ⊥ := by
simp only [val_def, Formula.hVal_neg];
rw [←HeytingAlgebra.himp_bot, himp_eq_top_iff, le_bot_iff];
rfl

@[simp] lemma val_or (φ ψ : Formula α) : ℍ ⊧ φ ⋎ ψ ↔ (ℍ ⊧ₕ φ) ⊔ (ℍ ⊧ₕ ψ) = ⊤ := by
simp [val_def]; rfl
Expand All @@ -96,8 +99,6 @@ def mod (H : Hilbert α) : Set (HeytingSemantics α) := Semantics.models (Heytin

variable {H : Hilbert α}

instance [H.IncludeEFQ] : System.Intuitionistic H where

lemma mod_models_iff {φ : Formula α} :
mod.{_,w} H ⊧ φ ↔ ∀ ℍ : HeytingSemantics.{_,w} α, ℍ ⊧* H.axioms → ℍ ⊧ φ := by
simp [mod, Semantics.models, Semantics.set_models_iff]
Expand Down Expand Up @@ -136,17 +137,16 @@ def lindenbaum : HeytingSemantics α where
valAtom a := ⟦.atom a⟧

lemma lindenbaum_val_eq : (lindenbaum H ⊧ₕ φ) = ⟦φ⟧ := by
induction φ using Formula.rec' <;> try simp [top_def, bot_def]
case hatom => rfl
case hverum => rfl
case hfalsum => rfl
case hand ihp ihq => simp [ihp, ihq]; rw [inf_def]
case hor ihp ihq => simp [ihp, ihq]; rw [sup_def]
case himp ihp ihq => simp [ihp, ihq]; rw [himp_def]
case hneg ih => simp [ih]; rw [compl_def]
induction φ using Formula.rec' with
| hand _ _ ihp ihq => simp only [hVal_and, ihp, ihq]; rw [inf_def];
| hor _ _ ihp ihq => simp only [hVal_or, ihp, ihq]; rw [sup_def];
| himp _ _ ihp ihq => simp only [hVal_imply, ihp, ihq]; rw [himp_def];
| hneg _ ih => simp only [hVal_not, ih]; rw [compl_def];
| _ => rfl

variable {H}

omit [System.Consistent H] in
lemma lindenbaum_complete_iff [System.Consistent H] {φ : Formula α} : lindenbaum H ⊧ φ ↔ H ⊢! φ := by
simp [val_def', lindenbaum_val_eq, provable_iff_eq_top]

Expand Down
10 changes: 5 additions & 5 deletions Foundation/Logic/LindenbaumAlgebra.lean
Original file line number Diff line number Diff line change
Expand Up @@ -136,7 +136,7 @@ lemma provable_iff_eq_top {φ : F} : 𝓢 ⊢! φ ↔ (⟦φ⟧ : LindenbaumAlge
simp [top_def, provable_iff_provablyEquivalent_verum]; rfl

lemma inconsistent_iff_trivial : Inconsistent 𝓢 ↔ (∀ φ : LindenbaumAlgebra 𝓢, φ = ⊤) := by
simp [Inconsistent, provable_iff_eq_top]
simp only [Inconsistent, provable_iff_eq_top]
constructor
· intro h φ;
induction φ using Quotient.ind
Expand All @@ -145,7 +145,7 @@ lemma inconsistent_iff_trivial : Inconsistent 𝓢 ↔ (∀ φ : LindenbaumAlgeb

lemma consistent_iff_nontrivial : Consistent 𝓢 ↔ Nontrivial (LindenbaumAlgebra 𝓢) := by
apply not_iff_not.mp
simp [not_consistent_iff_inconsistent, nontrivial_iff, inconsistent_iff_trivial]
simp only [not_consistent_iff_inconsistent, inconsistent_iff_trivial, nontrivial_iff, ne_eq, not_exists, not_not]
constructor
· intro h φ ψ; simp [h]
· intro h φ; exact h φ ⊤
Expand All @@ -167,7 +167,7 @@ instance LindenbaumAlgebra.heyting [DecidableEq F] : HeytingAlgebra (LindenbaumA
exact efq!
himp_bot φ := by
induction' φ using Quotient.ind with φ
simp [bot_def, himp_def, compl_def]
simp only [bot_def, himp_def, compl_def, Quotient.eq]
exact iff_comm! ⨀ neg_equiv!

end intuitionistic
Expand All @@ -184,7 +184,7 @@ instance LindenbaumAlgebra.boolean [DecidableEq F] : BooleanAlgebra (LindenbaumA
simp only [compl_def, inf_def, bot_def, le_def, intro_bot_of_and!]
top_le_sup_compl φ := by
induction' φ using Quotient.ind with φ
simp [compl_def, sup_def, top_def, le_def]
simp only [top_def, compl_def, sup_def, le_def]
apply imply₁'! lem!
le_top φ := by
induction' φ using Quotient.ind with φ
Expand All @@ -198,7 +198,7 @@ instance LindenbaumAlgebra.boolean [DecidableEq F] : BooleanAlgebra (LindenbaumA
induction' φ using Quotient.ind with φ
induction' ψ using Quotient.ind with ψ
rw [sup_comm]
simp [himp_def, compl_def, sup_def]
simp only [himp_def, compl_def, sup_def, Quotient.eq]
exact imply_iff_not_or!

end classical
Expand Down

0 comments on commit 76ff67f

Please sign in to comment.