Created
December 12, 2025 22:06
-
-
Save gaxiiiiiiiiiiii/bd26dddac60225f3d88d93b1ce6a95bc to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| import Mathlib | |
| lemma le_iff_inf_compl_eq_bot [BooleanAlgebra B] (x y : B) : | |
| x ≤ y ↔ x ⊓ yᶜ = ⊥ | |
| := by | |
| constructor<;> intro H | |
| · rw [<- sup_eq_right] at H | |
| rw [<- H, compl_sup, <- inf_assoc, inf_compl_eq_bot, bot_inf_eq] | |
| · rw [<- bot_sup_eq (a := y), <- H, sup_inf_right, compl_sup_eq_top, inf_top_eq] | |
| apply le_sup_left | |
| lemma le_iff_compl_sup_eq_top [BooleanAlgebra B] (x y : B) : | |
| x ≤ y ↔ xᶜ ⊔ y = ⊤ | |
| := by | |
| constructor<;> intro H | |
| · rw [<- inf_eq_right] at H | |
| rw [<- H, compl_inf, sup_comm, <- sup_assoc, sup_compl_eq_top, top_sup_eq] | |
| · rw [<- top_inf_eq (a := x), <- H, inf_sup_right, compl_inf_eq_bot, bot_sup_eq] | |
| apply inf_le_left | |
| class Heyting (H : Type _) extends Lattice H where | |
| imp : H → H → H | |
| galois (c : H) : GaloisConnection (c ⊓ ·) (fun b => imp c b) | |
| def Heyting.not [Heyting H] [OrderBot H] (a : H) : H := imp a ⊥ | |
| lemma Heyting.le_imp_iff [Heyting H] (a b c : H) : | |
| a ≤ imp b c ↔ a ⊓ b ≤ c | |
| := by | |
| rw [inf_comm] | |
| rw [(Heyting.galois b).le_iff_le] | |
| instance (B : BoolAlg) : Heyting B where | |
| imp := fun a b => aᶜ ⊔ b | |
| galois (c : B) := by | |
| intro a b; dsimp | |
| conv => arg 1;rw [le_iff_compl_sup_eq_top, compl_inf] | |
| conv => arg 2; rw [le_iff_compl_sup_eq_top, <- sup_assoc, sup_comm aᶜ] | |
| instance Heyting.distribLattice [Heyting L] : | |
| DistribLattice L | |
| := by | |
| apply DistribLattice.ofInfSupLe | |
| intro a b c | |
| rw [(Heyting.galois a).le_iff_le] | |
| simp; constructor | |
| · rw [<- (Heyting.galois a).le_iff_le] | |
| apply le_sup_left | |
| · rw [<- (Heyting.galois a).le_iff_le] | |
| apply le_sup_right | |
| namespace Heyting | |
| variable [Heyting H] [OrderBot H] (a b c : H) | |
| lemma le_not_iff_eq : | |
| b ≤ not a ↔ b ⊓ a = ⊥ | |
| := by | |
| simp [not] | |
| rw [le_imp_iff] | |
| simp | |
| lemma le_not_iff_le : | |
| a ≤ not b ↔ b ≤ not a | |
| := by | |
| rw [le_not_iff_eq, inf_comm, <- le_not_iff_eq] | |
| lemma inf_not_eq_bot : | |
| a ⊓ not a = ⊥ | |
| := by | |
| rw [inf_comm] | |
| rw [<- le_not_iff_eq] | |
| lemma le_not_not : | |
| a ≤ not (not a) | |
| := by | |
| rw [le_not_iff_eq] | |
| rw [inf_not_eq_bot] | |
| lemma contrapose : | |
| a ≤ b → not b ≤ not a | |
| := by | |
| intro H | |
| rw [le_not_iff_eq, inf_comm, <- le_not_iff_eq] | |
| apply le_trans H | |
| apply le_not_not | |
| lemma not_elm : | |
| not (not (not a)) = not a | |
| := by | |
| apply le_antisymm; swap | |
| · rw [le_not_iff_eq, inf_comm, <- le_not_iff_eq] | |
| · apply contrapose | |
| apply le_not_not | |
| lemma not_sup : | |
| not (a ⊔ b) = not a ⊓ not b | |
| := by | |
| apply le_antisymm | |
| · apply le_inf<;> apply contrapose<;> simp | |
| · rw [le_not_iff_eq] | |
| rw [inf_assoc, inf_sup_left, inf_comm _ b, inf_not_eq_bot, sup_bot_eq] | |
| rw [inf_comm, inf_assoc, inf_not_eq_bot, inf_bot_eq] | |
| lemma not_not_inf : | |
| not (not (a ⊓ b)) = not (not a) ⊓ not (not b) | |
| := by | |
| apply le_antisymm | |
| · rw [<- not_sup] | |
| apply contrapose; simp; constructor<;> apply contrapose<;> simp | |
| · rw [le_not_iff_eq, inf_assoc, inf_comm, <- le_not_iff_eq, not_elm, <- not_sup] | |
| rw [le_not_iff_eq, not_sup, inf_assoc, inf_comm, <- le_not_iff_eq, not_elm] | |
| rw [le_not_iff_eq, inf_assoc, inf_comm, inf_not_eq_bot] | |
| lemma not_ext : | |
| a ⊓ b = ⊥ → a ⊔ b = not ⊥ → b = not a | |
| := by | |
| intro Hb Ht | |
| rw [inf_comm, <- le_not_iff_eq] at Hb | |
| apply le_antisymm Hb | |
| rw [<- sup_bot_eq a, not_sup, <- Ht] | |
| rw [inf_sup_left, inf_comm, inf_not_eq_bot] | |
| rw [bot_sup_eq] | |
| apply inf_le_right | |
| end Heyting | |
| def Heyting.regular (H : Type _) [Heyting H] [OrderBot H]: Type _ := {a : H // Heyting.not (Heyting.not a) = a} | |
| instance Heyting.toBooleanAlgebra [Heyting H] [OrderBot H] (Hbot : not (not (⊥ : H)) = ⊥): | |
| BooleanAlgebra (regular H) | |
| where | |
| top := by | |
| use not ⊥ | |
| rw [not_elm] | |
| bot := by | |
| use ⊥ | |
| compl a := by | |
| use not a.val | |
| rw [not_elm] | |
| inf := by | |
| intro ⟨a, Ha⟩ ⟨b, Hb⟩ | |
| use a ⊓ b | |
| rw [not_not_inf, Ha, Hb] | |
| sup := by | |
| intro ⟨a, Ha⟩ ⟨b, Hb⟩ | |
| use not (not (a ⊔ b)) | |
| apply le_antisymm | |
| · rw [not_sup] | |
| apply contrapose | |
| rw [le_not_iff_le] | |
| · rw [le_not_iff_le] | |
| le a b := a.val ⊓ b.val = a.val | |
| le_refl a := by simp | |
| le_trans a b c := by grind | |
| le_antisymm a b := by simp; grind | |
| le_top := by | |
| intro ⟨a, Ha⟩; simp | |
| rw [le_not_iff_le]; simp | |
| bot_le := by | |
| intro ⟨a, Ha⟩; simp | |
| le_sup_left := by | |
| intro ⟨a, Ha⟩ ⟨b, Hb⟩; simp | |
| rw [le_not_iff_le, not_sup]; simp | |
| le_sup_right := by | |
| intro ⟨a, Ha⟩ ⟨b, Hb⟩; simp | |
| rw [le_not_iff_le, not_sup]; simp | |
| sup_le := by | |
| intro ⟨a, Ha⟩ ⟨b, Hb⟩ ⟨c, Hc⟩ Hac Hbc; simp at Hac Hbc ⊢ | |
| rw [<- Hc] | |
| apply contrapose; apply contrapose | |
| apply sup_le Hac Hbc | |
| inf_le_left := by | |
| intro ⟨a, Ha⟩ ⟨b, Hb⟩; simp | |
| inf_le_right := by | |
| intro ⟨a, Ha⟩ ⟨b, Hb⟩; simp | |
| le_inf := by | |
| intro ⟨a, Ha⟩ ⟨b, Hb⟩ ⟨c, Hc⟩ Hac Hbc; simp at Hac Hbc ⊢ | |
| constructor<;> assumption | |
| le_sup_inf := by | |
| simp [max, min] | |
| intro ⟨a, Ha⟩ ⟨b, Hb⟩ ⟨c, Hc⟩; simp | |
| change | |
| ((not (not (a ⊔ b))) ⊓ (not (not (a ⊔ c)))) ⊓ (not (not (a ⊔ (b ⊓ c)))) = | |
| not (not (a ⊔ b)) ⊓ not (not (a ⊔ c)) | |
| simp | |
| rw [sup_inf_left, not_not_inf] | |
| inf_compl_le_bot := by | |
| simp [min] | |
| intro ⟨a, Ha⟩; simp | |
| change (a ⊓ not a) ⊓ ⊥ = (a ⊓ not a) | |
| rw [inf_not_eq_bot, inf_idem] | |
| top_le_sup_compl := by | |
| simp [min, max] | |
| intro ⟨a, Ha⟩; simp | |
| change (not ⊥) ⊓ not (not (a ⊔ not a)) = not ⊥ | |
| rw [not_sup, Ha, inf_comm _ a, inf_not_eq_bot] | |
| simp |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment