1 (* (C) 2014 Luca Bressan *)
3 include "notations.ma".
5 universe constraint Type[0] < Type[1].
6 universe constraint Type[1] < Type[2].
8 notation "'cl'" with precedence 90 for @{ Type[1] }.
9 notation "'st'" with precedence 90 for @{ Type[0] }.
10 notation "'prop'" with precedence 90 for @{ CProp[1] }.
11 notation "'props'" with precedence 90 for @{ CProp[0] }.
13 record Sigma (B: cl) (C: B → cl) : cl ≝
17 interpretation "Strong Indexed Sum" 'sigma x = (Sigma ? x).
18 interpretation "Strong Indexed Sum constructor" 'mk_sigma x y = (mk_Sigma ?? x y).
19 interpretation "First projection of Strong Indexed Sum" 'sig1 x = (Sig1 ?? x).
20 interpretation "Second projection of Strong Indexed Sum" 'sig2 x = (Sig2 ?? x).
22 definition Times: cl → cl → cl ≝
23 λB,C. Sigma B (λ_. C).
24 interpretation "Binary collection product" 'times B C = (Times B C).
30 interpretation "Element of the singleton" 'star = star.
32 record sigma (B: st) (C : B → st) : st ≝
36 interpretation "Strong Indexed Sum set" 'sigma x = (sigma ? x).
37 interpretation "Strong Indexed Sum set constructor" 'mk_sigma x y = (mk_sigma ?? x y).
38 interpretation "First projection of Strong Indexed Sum set" 'sig1 x = (sig1 ?? x).
39 interpretation "Second projection of Strong Indexed Sum set" 'sig2 x = (sig2 ?? x).
41 definition times: st → st → st ≝
42 λB,C. sigma B (λ_. C).
43 interpretation "Binary set product" 'times B C = (times B C).
45 inductive list (C: st) : st (*CSC: Type[0]*) ≝
47 | cons: list C → C → list C.
48 interpretation "Empty list" 'epsilon = (epsilon ?).
49 interpretation "List constructor" 'cons l c = (cons ? l c).
51 inductive plus (B: st) (C: st) : st ≝
54 interpretation "Disjoint Sum set" 'plus B C = (plus B C).
56 inductive Falsum: prop ≝ .
57 interpretation "Falsum" 'falsum = Falsum.
59 inductive Disj (B: prop) (C: prop) : prop ≝
62 interpretation "Disjunction" 'disj B C = (Disj B C).
64 record Conj (B: prop) (C: prop) : prop ≝
68 interpretation "Conjunction" 'conj B C = (Conj B C).
70 definition Implies: prop → prop → prop ≝
72 interpretation "Implication" 'implies B C = (Implies B C).
74 record Exists (B: cl) (C: B → prop) : prop ≝
78 interpretation "Existential quantification" 'exists x = (Exists ? x).
79 interpretation "Existential quantification constructor" 'mk_exists x y = (mk_Exists ?? x y).
81 definition Forall: ∀B: cl. (B → prop) → prop ≝ λB,C. ∀b: B. C b.
83 inductive Id (A: cl) (a: A) : A → prop ≝
84 Reflexivity: Id A a a.
85 interpretation "Propositional Equality" 'id a b = (Id ? a b).
86 interpretation "Reflexivity in Extensional Collections" 'rfl x = (Reflexivity ? x).
88 definition Verum: prop ≝ Implies Falsum Falsum.
89 interpretation "Verum" 'verum = Verum.
91 inductive falsum: props ≝ .
92 interpretation "Small Falsum" 'falsum = falsum.
94 inductive disj (B: props) (C: props) : props ≝
97 interpretation "Small Disjunction" 'disj B C = (disj B C).
99 record conj (B: props) (C: props) : props ≝
103 interpretation "Small Conjunction" 'conj B C = (conj B C).
105 definition implies: props → props → props ≝
107 interpretation "Small Implication" 'implies B C = (implies B C).
109 record exists (B: st) (C: B → props) : props ≝
113 interpretation "Small Existential quantification" 'exists x = (exists ? x).
114 interpretation "Small Existential quantification constructor" 'mk_exists x y = (mk_exists ?? x y).
116 definition forall: ∀B: st. (B → props) → props ≝ λB,C. ∀b: B. C b.
118 inductive id (A: st) (a: A) : A → props ≝
119 reflexivity: id A a a.
120 interpretation "Small Propositional Equality" 'id a b = (id ? a b).
121 interpretation "Reflexivity in Extensional Sets" 'rfl x = (reflexivity ? x).
123 definition verum: props ≝ implies falsum falsum.
124 interpretation "Verum" 'verum = verum.
126 definition fun_to_props: st → cl ≝ λB. B → props.
128 lemma Symmetry: ∀A: cl. ∀x,x': A. x = x' → x' = x.
131 interpretation "Symmetry in Intensional Collections" 'sym d = (Symmetry ??? d).
133 lemma Transitivity: ∀A: cl. ∀x,x',x'': A. x = x' → x' = x'' → x = x''.
136 interpretation "Transitivity in Intensional Collections" 'tra d = (Transitivity ???? d).
138 lemma rewrite_l: ∀A: st. ∀x: A. ∀P: A → props. P x → ∀y: A. x = y → P y.
142 notation "hvbox(> h)"
143 non associative with precedence 45
144 for @{ 'rewrite_l $h }.
145 interpretation "Rewrite left" 'rewrite_l h = (rewrite_l ????? h).
147 lemma symmetry: ∀A: st. ∀x,x': A. x = x' → x' = x.
150 interpretation "Symmetry in Intensional Sets" 'sym d = (symmetry ??? d).
152 notation "hvbox(< h)"
153 non associative with precedence 45
154 for @{ 'rewrite_r $h }.
155 interpretation "Rewrite right" 'rewrite_r h = (rewrite_l ????? (symmetry ??? h)).
157 lemma transitivity: ∀A: st. ∀x,x',x'': A. x = x' → x' = x'' → x = x''.
160 interpretation "Transitivity in Intensional Sets" 'tra d = (transitivity ???? d).
162 definition lift_to_list: ∀A,A': st. (A → A') → list A → list A' ≝
163 λA,A',f. list_rect_Type0 … (λ_. list A') ϵ (λl,x,l'. ⌈l', f x⌉).
165 definition proj_l: ∀B,C: st. B → plus B C → B ≝
166 λB,C,b'. plus_rect_Type0 B C (λ_. B) (λb. b) (λ_. b').
168 definition proj_r: ∀B,C: st. C → plus B C → C ≝
169 λB,C,c'. plus_rect_Type0 B C (λ_. C) (λ_. c') (λc. c).
171 lemma injectivity_inl: ∀B,C: st. ∀x,x'. inl B C x = inl B C x' → x = x'.
173 @(rewrite_l … (inl … x) (λz. proj_l … x (inl … x) = proj_l … x z)
174 (ı(proj_l … x (inl … x))) (inl … x'))
177 lemma injectivity_inr: ∀B,C: st. ∀y,y'. inr B C y = inr B C y' → y = y'.
179 @(rewrite_l … (inr … y) (λz. proj_r … y (inr … y) = proj_r … y z)
180 (ı(proj_r … y (inr … y))) (inr … y'))
183 lemma injectivity_cons1: ∀C: st. ∀l,l': list C. ∀c,c': C. ⌈l, c⌉ = ⌈l', c'⌉ → l = l'.
185 @(rewrite_l … ⌈l1, c1⌉
186 (list_rect_Type1 … (λ_. props) ⊥ (λl,c,h. l1 = l))
190 lemma injectivity_cons2: ∀C: st. ∀l,l': list C. ∀c,c': C. ⌈l, c⌉ = ⌈l', c'⌉ → c = c'.
192 @(rewrite_l … ⌈l1, c1⌉
193 (list_rect_Type1 … (λ_. props) ⊥ (λl,c,h. c1 = c))
197 lemma plus_clash: ∀B,C: st. ∀b: B. ∀c: C. inl … b = inr … c → ⊥.
199 @(rewrite_l … (inl … b) (plus_rect_Type1 … (λ_. props) (λ_. ⊤) (λ_. ⊥))
203 lemma list_clash: ∀C: st. ∀l: list C. ∀c: C. ϵ = ⌈l, c⌉ → ⊥.
205 @(rewrite_l … ϵ (list_rect_Type1 … (λ_. props) ⊤ (λ_,_,_. ⊥))
209 definition nat: st ≝ list n1.
210 definition zero: nat ≝ ϵ.
211 definition succ: nat → nat ≝ λn. cons … n ⋆.
212 definition nat_rect_Type0: ∀Q: nat → st. Q zero → (∀n. Q n → Q (succ n)) → ∀n. Q n.
213 #Q #h0 #hi @list_rect_Type0 [ @h0 | #n @n1_rect_Type0 @(hi n) ]
215 definition nat_rect_Type1: ∀Q: nat → cl. Q zero → (∀n. Q n → Q (succ n)) → ∀n. Q n.
216 #Q #h0 #hi @list_rect_Type1 [ @h0 | #n @n1_rect_Type1 @(hi n) ]
218 definition nat_rect_CProp0: ∀Q: nat → props. Q zero → (∀n. Q n → Q (succ n)) → ∀n. Q n.
219 #Q #h0 #hi @list_rect_CProp0 [ @h0 | #n @n1_rect_CProp0 @(hi n) ]
221 definition nat_rect_CProp1: ∀Q: nat → prop. Q zero → (∀n. Q n → Q (succ n)) → ∀n. Q n.
222 #Q #h0 #hi @list_rect_CProp1 [ @h0 | #n @n1_rect_CProp1 @(hi n) ]
225 inductive De (I: st) : st ≝
228 | c_times: De I → De I → De I
229 | c_plus: De I → De I → De I.
231 definition int: ∀I: st. De I → (I → st) → st.
235 | #L #R #intL #intR #X @((intL X)×(intR X))
236 | #L #R #intL #intR #X @((intL X)+(intR X))
240 definition napply: nat → (st → st) → st → st.
243 | #_ #F' #F #X @(F' F X)
247 definition mu: ∀I: st. (I → De I) → I → st.
248 #I #F #i @(Σn: nat. napply n (λX: st. int I (F i) (λ_. X)) n0)
251 definition is_c_unit: ∀I: st. ∀F: De I. props.
252 #I * [ @verum | #_ @falsum | 3,4: #_ #_ @falsum ]
255 lemma De_clash_unit_ev: ∀I: st. ∀i: I. c_ev I i = c_unit I → falsum.
257 @(rewrite_l (De I) (c_unit I) (is_c_unit I) (λx. x) (c_ev I i) h⁻¹)
259 lemma De_clash_unit_times: ∀I: st. ∀F,G: De I. c_times I F G = c_unit I → falsum.
261 @(rewrite_l (De I) (c_unit I) (is_c_unit I) (λx. x) (c_times I F G) h⁻¹)
263 lemma De_clash_unit_plus: ∀I: st. ∀F,G: De I. c_plus I F G = c_unit I → falsum.
265 @(rewrite_l (De I) (c_unit I) (is_c_unit I) (λx. x) (c_plus I F G) h⁻¹)
268 inductive mu_ (I: st) (F: I → De I) : I → De I → st ≝
269 fold_unit: ∀i: I. mu_ I F i (c_unit I)
270 | fold_ev: ∀i,i': I. mu_ I F i' (F i') → mu_ I F i (c_ev I i')
271 | fold_times: ∀i: I. ∀G1,G2: De I. mu_ I F i G1 → mu_ I F i G2 → mu_ I F i (c_times I G1 G2)
272 | fold_plusL: ∀i: I. ∀G1,G2: De I. mu_ I F i G1 → mu_ I F i (c_plus I G1 G2)
273 | fold_plusR: ∀i: I. ∀G1,G2: De I. mu_ I F i G2 → mu_ I F i (c_plus I G1 G2).