-
Notifications
You must be signed in to change notification settings - Fork 0
/
lem.lagda
188 lines (159 loc) · 7.84 KB
/
lem.lagda
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
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
\begin{code}
{-# OPTIONS --rewriting #-}
{-# OPTIONS --guardedness #-}
open import Level using (Level ; 0ℓ ; Lift ; lift ; lower) renaming (suc to lsuc)
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite
open import Agda.Builtin.Sigma
open import Relation.Nullary
open import Relation.Unary using (Pred; Decidable)
open import Relation.Binary.PropositionalEquality using (sym ; trans ; subst)
open import Data.Product
open import Data.Product.Properties
open import Data.Sum
open import Data.Empty
open import Data.Maybe
open import Data.Unit using (⊤ ; tt)
open import Data.Nat using (ℕ ; _<_ ; _≤_ ; _≥_ ; _≤?_ ; suc ; _+_ ; pred)
open import Data.Nat.Properties
open import Agda.Builtin.String
open import Agda.Builtin.String.Properties
open import Data.List
open import Data.List.Properties
open import Data.List.Relation.Unary.Any
open import Data.List.Membership.Propositional
open import Data.List.Membership.Propositional.Properties
open import Function.Bundles
open import Induction.WellFounded
open import Axiom.ExcludedMiddle
open import util
open import name
open import calculus
open import terms
open import world
open import choice
open import compatible
open import choiceExt
open import choiceVal
open import getChoice
open import newChoice
open import progress
open import exBar
open import mod
open import encode
module lem {L : Level} (W : PossibleWorlds {L}) (M : Mod W)
(C : Choice)
(K : Compatible {L} W C)
-- (P : Progress {L} W C K)
(G : GetChoice {L} W C K)
(X : ChoiceExt W C)
(N : NewChoice W C K G)
-- (V : ChoiceVal W C K G X N)
-- (E : Extensionality 0ℓ (lsuc(lsuc(L))))
(EM : ExcludedMiddle (lsuc(L)))
(EB : ExBar W M)
(EC : Encode)
where
open import worldDef(W)
open import choiceDef{L}(C)
open import exBarDef(W)(M)(EB)
open import computation(W)(C)(K)(G)(X)(N)(EC)
open import bar(W)
open import barI(W)(M)--(C)(K)(P)
open import forcing(W)(M)(C)(K)(G)(X)(N)(EC)
--open import props0(W)(M)(C)(K)(G)(X)(N)(EC)
--open import ind2(W)(M)(C)(K)(G)(X)(N)(EC)
open import props1(W)(M)(C)(K)(G)(X)(N)(EC)
open import props2(W)(M)(C)(K)(G)(X)(N)(EC)
open import props3(W)(M)(C)(K)(G)(X)(N)(EC)
open import lem_props(W)(M)(C)(K)(G)(X)(N)(EC)
□·⊎inhType : (i : ℕ) (w : 𝕎·) (T : CTerm)
→ □· w (λ w' _ → inhType i w' T ⊎ ∀𝕎 w' (λ w'' _ → ¬ inhType i w'' T))
□·⊎inhType i w T =
∀∃𝔹· (λ w' e1 e2 h → h) aw
where
aw : ∀𝕎 w (λ w1 e1 → ∃𝕎 w1 (λ w2 e2 → □· w2 (λ w' e → inhType i w' T ⊎ ∀𝕎 w' (λ w'' _ → ¬ inhType i w'' T))))
aw w1 e1 = cc (EM {∃𝕎 w1 (λ w2 e2 → inhType i w2 T)})
where
cc : Dec (∃𝕎 w1 (λ w2 e2 → inhType i w2 T))
→ ∃𝕎 w1 (λ w2 e2 → □· w2 (λ w' e → inhType i w' T ⊎ ∀𝕎 w' (λ w'' _ → ¬ inhType i w'' T)))
cc (no ¬p) = w1 , ⊑-refl· _ , Mod.∀𝕎-□ M (λ w3 e3 → inj₂ (λ w4 e4 z → ¬p (w4 , ⊑-trans· e3 e4 , z)))
cc (yes (w2 , e2 , p)) = w2 , e2 , Mod.∀𝕎-□ M (λ w3 e3 → inj₁ (inhType-mon e3 p))
classical : (w : 𝕎·) {n i : ℕ} (p : i < n) → member w (#LEM p) #lamAX
classical w {n} {i} p rewrite #LEM≡#PI p =
n , equalInType-PI {_} {_} {#UNIV i} {#[0]SQUASH (#[0]UNION #[0]VAR (#[0]NEG #[0]VAR))} p1 p2 p3
where
-- p1 and p2 prove that LEM is a type
p1 : ∀𝕎 w (λ w' _ → isType n w' (#UNIV i))
p1 w1 _ = eqTypesUniv w1 n i p
p2 : ∀𝕎 w (λ w' _ → (a₁ a₂ : CTerm) (ea : equalInType n w' (#UNIV i) a₁ a₂)
→ equalTypes n w' (sub0 a₁ (#[0]SQUASH (#[0]UNION #[0]VAR (#[0]NEG #[0]VAR))))
(sub0 a₂ (#[0]SQUASH (#[0]UNION #[0]VAR (#[0]NEG #[0]VAR)))))
p2 w1 e1 a₁ a₂ ea =
≡CTerm→eqTypes (sym (sub0-#[0]SQUASH-LEM p a₁))
(sym (sub0-#[0]SQUASH-LEM p a₂))
(eqTypesSQUASH← (eqTypesUNION← (equalInType→equalTypes p w1 a₁ a₂ ea)
(eqTypesNEG← (equalInType→equalTypes p w1 a₁ a₂ ea))))
-- now we prove that it is inhabited
p3 : ∀𝕎 w (λ w' _ → (a₁ a₂ : CTerm) → equalInType n w' (#UNIV i) a₁ a₂
→ equalInType n w' (sub0 a₁ (#[0]SQUASH (#[0]UNION #[0]VAR (#[0]NEG #[0]VAR))))
(#APPLY #lamAX a₁) (#APPLY #lamAX a₂))
p3 w1 e1 a₁ a₂ ea =
≡CTerm→equalInType
(sym (sub0-#[0]SQUASH-LEM p a₁))
(→equalInType-SQUASH p4)
where
p6 : □· w1 (λ w' _ → inhType n w' a₁ ⊎ ∀𝕎 w' (λ w'' _ → ¬ inhType n w'' a₁))
p6 = □·⊎inhType n w1 a₁
p5 : □· w1 (λ w' _ → inhType n w' a₁ ⊎ inhType n w' (#NEG a₁))
p5 = Mod.∀𝕎-□Func M aw p6
where
aw : ∀𝕎 w1 (λ w' e' → (inhType n w' a₁ ⊎ ∀𝕎 w' (λ w'' _ → ¬ inhType n w'' a₁))
→ (inhType n w' a₁ ⊎ inhType n w' (#NEG a₁)))
aw w2 e2 (inj₁ i) = inj₁ i
aw w2 e2 (inj₂ i) = inj₂ (equalInType-NEG-inh (equalInType→equalTypes p w2 a₁ a₁ (equalInType-refl (equalInType-mon ea w2 e2))) i)
p4 : □· w1 (λ w' _ → Σ CTerm (λ t → ∈Type n w' (#UNION a₁ (#NEG a₁)) t))
p4 = Mod.∀𝕎-□Func M aw p5
where
aw : ∀𝕎 w1 (λ w' e' → inhType n w' a₁ ⊎ inhType n w' (#NEG a₁)
→ Σ CTerm (λ t → ∈Type n w' (#UNION a₁ (#NEG a₁)) t))
aw w2 e2 (inj₁ (t , h)) =
#INL t ,
→equalInType-UNION
(equalInType→equalTypes p w2 a₁ a₁ (equalInType-refl (equalInType-mon ea w2 e2)))
(eqTypesNEG← (equalInType→equalTypes p w2 a₁ a₁ (equalInType-refl (equalInType-mon ea w2 e2))))
(Mod.∀𝕎-□ M (λ w3 e3 → t , t , inj₁ (⇓-refl ⌜ #INL t ⌝ w3 {--#compAllRefl (#INL t) _--} ,
⇓-refl ⌜ #INL t ⌝ w3 {--#compAllRefl (#INL t) _--} ,
equalInType-mon h w3 e3)))
aw w2 e2 (inj₂ (t , h)) =
#INR t ,
→equalInType-UNION
(equalInType→equalTypes p w2 a₁ a₁ (equalInType-refl (equalInType-mon ea w2 e2)))
(eqTypesNEG← (equalInType→equalTypes p w2 a₁ a₁ (equalInType-refl (equalInType-mon ea w2 e2))))
(Mod.∀𝕎-□ M (λ w3 e3 → t , t , inj₂ (⇓-refl ⌜ #INR t ⌝ w3 {--#compAllRefl (#INR t) _--} ,
⇓-refl ⌜ #INR t ⌝ w3 {--#compAllRefl (#INR t) _--} ,
equalInType-mon h w3 e3)))
-- We now prove that open bars satisfy the ExBar property
open import barOpen(W)
∀∃𝔹-open : {w : 𝕎·} {f : wPred w} → wPredExtIrr f → ∀𝕎 w (λ w1 e1 → ∃𝕎 w1 (λ w2 e2 → inOpenBar w2 (↑wPred f (⊑-trans· e1 e2)))) → inOpenBar w f
∀∃𝔹-open {w} {f} ext h w1 e1 =
w3 ,
⊑-trans· e2 e3 ,
λ w4 e4 z → ext w4 (⊑-trans· (⊑-trans· e1 e2) (⊑-trans· e3 e4)) z (h3 w4 e4 (⊑-trans· e3 e4))
where
w2 : 𝕎·
w2 = fst (h w1 e1)
e2 : w1 ⊑· w2
e2 = fst (snd (h w1 e1))
h2 : inOpenBar w2 (↑wPred f (⊑-trans· e1 e2))
h2 = snd (snd (h w1 e1))
w3 : 𝕎·
w3 = fst (h2 w2 (⊑-refl· _))
e3 : w2 ⊑· w3
e3 = fst (snd (h2 w2 (⊑-refl· _)))
h3 : ∀𝕎 w3 (λ w4 e4 → (z : w2 ⊑· w4) → f w4 (⊑-trans· (⊑-trans· e1 e2) z))
h3 = snd (snd (h2 w2 (⊑-refl· _)))
exBar-open : ExBar W inOpenBar-Mod
exBar-open = mkExBar ∀∃𝔹-open
\end{code}[hide]