This repository was archived by the owner on Jul 2, 2026. It is now read-only.
forked from gotrevor/Foundation
-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathBalloon.lean
More file actions
105 lines (91 loc) · 3.74 KB
/
Copy pathBalloon.lean
File metadata and controls
105 lines (91 loc) · 3.74 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
module
public import Foundation.Modal.Kripke.Cluster
public import Foundation.Modal.Kripke.Terminated
public import Foundation.Modal.Kripke.LinearFrame
@[expose] public section
namespace LO.Modal.Kripke
class Frame.IsBalloon (F : Frame) [F.IsTransitive] (e : Cluster F) extends IsStrictTotalOrder _ F, IsTerminated (F.strictSkelteon) e where
envelope_non_degenerated : ¬e.degenerate
not_envelope_degenerated : ∀ C, C ≠ e → C.degenerate
namespace Frame.IsBalloon
open Formula.Kripke
variable {F : Frame} [IsStrictTotalOrder _ F] {e : Cluster F} [F.IsBalloon e] {x : F.World} {φ : Formula ℕ}
/-- Every points in enverope is reflexive. -/
lemma rfl_in_envelope (hx : x ∈ e) : x ≺ x := Cluster.refl_of_mem_non_degenerate (envelope_non_degenerated) hx
/-- Every point in balloon can see all points in envelope. -/
lemma covered_in_envelope (x : F.World) : ∀ t ∈ e, x ≺ t := by
obtain ⟨t₁, rfl⟩ := Quotient.exists_rep e;
intro t₂ ht₂;
replace ht₂ := Cluster.mem_iff₂.mp ht₂;
rcases ht₂ with rfl | ⟨Rt₁₂, Rt₂₁⟩;
. by_cases ext₁ : (⟦x⟧ : Cluster F) = ⟦t₁⟧;
. simp only [Quotient.eq] at ext₁;
rcases ext₁ with rfl | ⟨Rxt₁, Rtx₁⟩;
. exact rfl_in_envelope (by tauto);
. assumption;
. have := IsTerminated.direct_terminated_of_trans (F := F.strictSkelteon) (t := ⟦t₁⟧) ⟦x⟧ ext₁;
exact this.1;
. by_cases ext₁ : (⟦x⟧ : Cluster F) = ⟦t₁⟧;
. rcases Cluster.iff_eq_cluster.mp ext₁ with rfl | ⟨Rxt₁, Rtx₁⟩;
. assumption;
. exact _root_.trans Rxt₁ Rt₁₂;
. have := IsTerminated.direct_terminated_of_trans (F := F.strictSkelteon) (t := ⟦t₁⟧) ⟦x⟧ ext₁;
exact _root_.trans this.1 Rt₁₂;
/-- Every points from enverope is in enverope. -/
lemma in_envelope_of_in_envelope (hx : x ∈ e) : ∀ {y}, x ≺ y → y ∈ e := by
obtain ⟨t, rfl⟩ := Quotient.exists_rep e;
intro y Rxy;
apply Cluster.mem_iff₂.mpr;
by_cases t = y;
. tauto;
. right;
replace hx := Cluster.mem_iff₂.mp hx;
rcases hx with rfl | ⟨Rtx, Rxt⟩;
. constructor;
. exact Rxy;
. apply covered_in_envelope (e := ⟦t⟧);
tauto;
. constructor;
. exact _root_.trans Rtx Rxy;
. apply covered_in_envelope (e := ⟦t⟧);
tauto;
end Frame.IsBalloon
/-- In finite strict total ordered frame, `□φ` is not valid at x, farthest point from `x` exists s.t. not validate `φ` and validate `□φ`. -/
lemma farthermost_point_of_not_box {M : Kripke.Model} [IsStrictOrder _ M.toFrame] {x : M} (h : ¬x ⊧ □φ) : ∃ y, x ≺ y ∧ ¬y ⊧ φ ∧ y ⊧ □φ := by
sorry;
open
Formula.Kripke
Frame.IsBalloon
in
lemma balooon_validates_axiomZ
{F : Frame} [F.IsTransitive] {e : Cluster F} [F.IsBalloon e] : F ⊧ (Axioms.Z (.atom 0)) := by
intro V x;
suffices ¬(Satisfies _ x (□(□(.atom 0) 🡒 (.atom 0)))) ∨ ¬(Satisfies _ x (◇□(.atom 0))) ∨ (Satisfies _ x (□(.atom 0))) by tauto;
by_cases h : Satisfies _ x (□(.atom 0));
. right; right; assumption;
. obtain ⟨y, Rxy, hy, hy_far⟩ := farthermost_point_of_not_box h;
by_cases hxT : x ∈ e;
. right; left;
apply Satisfies.dia_def.not.mpr;
push Not;
intro z Rxz;
apply Satisfies.box_def.not.mpr;
push Not;
use y;
constructor;
. have hzT : z ∈ e := in_envelope_of_in_envelope hxT Rxz;
rcases Cluster.mem_same_cluster hxT hzT with rfl | ⟨Rzx, Rxz⟩;
. assumption;
. exact _root_.trans Rzx Rxy;
. assumption;
. left;
apply Satisfies.box_def.not.mpr;
push Not;
use y;
constructor;
. assumption;
. apply Satisfies.imp_def₂.not.mpr
push Not;
tauto;
end LO.Modal.Kripke
end