Skip to content

Commit 0b7f8d7

Browse files
klinashkaklinashka
committed
Proved lemmas regarding enumerability for types and predicates.
1 parent bb1a51e commit 0b7f8d7

File tree

3 files changed

+497
-81
lines changed

3 files changed

+497
-81
lines changed

‎code/Enumerability/Definitions.v‎

Lines changed: 0 additions & 81 deletions
This file was deleted.

‎code/Enumerability/EnumerablePredicates.v‎

Lines changed: 230 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,230 @@
1+
Require Import init.imports.
2+
Require Import Inductive.Option.
3+
Require Import Decidability.DecidablePredicates.
4+
Require Import Inductive.Predicates.
5+
Require Import util.NaturalEmbedding.
6+
7+
Definition rangeequiv {X : UU} {Y : UU} (f g : X → Y) := ∏ (y : Y), ∥hfiber f y∥ <-> ∥hfiber g y∥.
8+
9+
Notation "f ≡ᵣ g" := (rangeequiv f g) (at level 50).
10+
11+
Section EnumerablePredicates.
12+
13+
Definition ispredenum {X : UU} (p : X → hProp) (f : nat → option) := ∏ (x : X), (p x) <-> ∥(hfiber f (some x))∥.
14+
15+
Definition predenum {X : UU} (p : X → hProp) := ∑ (f : nat → option), (ispredenum p f).
16+
17+
Definition isenumerablepred {X : UU} (p : X → hProp) := ∥predenum p∥.
18+
19+
Lemma isapropispredenum {X : UU} (p : X → hProp) (f : nat → option) : (isaprop (ispredenum p f)).
20+
Proof.
21+
apply impred_isaprop.
22+
intros t.
23+
apply isapropdirprod; apply isapropimpl, propproperty.
24+
Qed.
25+
26+
Lemma rangeequivtohomot {X : UU} (p q : X → hProp) (e1 : (predenum p)) (e2 : (predenum q)) : ((pr1 e1) ≡ᵣ (pr1 e2)) → p ~ q.
27+
Proof.
28+
intros req x.
29+
destruct e1 as [f ispf].
30+
destruct e2 as [g ispg].
31+
destruct (req (some x)) as [impl1 impl2].
32+
destruct (ispf x) as [if1 if2].
33+
destruct (ispg x) as [ig1 ig2].
34+
use hPropUnivalence.
35+
- intros px.
36+
apply ig2, impl1, if1.
37+
exact px.
38+
- intros qx.
39+
apply if2, impl2, ig1.
40+
exact qx.
41+
Qed.
42+
43+
(* Closure properties *)
44+
Lemma enumconj {X : UU} (p q : X → hProp) (deceq : isdeceq X) : (predenum p) → (predenum q) → (predenum (λ x : X, p x ∧ q x)).
45+
Proof.
46+
intros [f enumf] [g enumg].
47+
use tpair.
48+
- intros n.
49+
destruct (unembed n) as [m1 m2].
50+
induction (f m1), (g m2).
51+
+ induction (deceq a x).
52+
* exact (some x).
53+
* exact none.
54+
+ exact none.
55+
+ exact none.
56+
+ exact none.
57+
- simpl. intros x.
58+
split. intros [px qx].
59+
destruct (enumf x) as [enumfx1 enumfx2].
60+
destruct (enumg x) as [enumgx1 enumgx2].
61+
use squash_to_prop.
62+
+ exact (hfiber f (some x)).
63+
+ exact (enumfx1 px).
64+
+ apply propproperty.
65+
+ intros [m1 m1eq].
66+
use squash_to_prop.
67+
* exact (hfiber g (some x)).
68+
* exact (enumgx1 qx).
69+
* apply propproperty.
70+
* intros [m2 m2eq].
71+
apply hinhpr.
72+
use make_hfiber.
73+
-- exact (embed (m1,, m2)).
74+
-- simpl.
75+
induction (pathsinv0 (unembedinv (m1,, m2))).
76+
induction (pathsinv0 (m1eq)), (pathsinv0 (m2eq)).
77+
simpl.
78+
induction (deceq x x).
79+
++ induction a.
80+
apply idpath.
81+
++ apply fromempty, b. exact (idpath x).
82+
+ intros; split; use squash_to_prop.
83+
* exact (hfiber
84+
(λ n : nat,
85+
coprod_rect (λ _ : X ⨿ unit, option)
86+
(λ a : X,
87+
match g (pr2 (unembed n)) with
88+
| inl x =>
89+
coprod_rect (λ _ : (a = x) ⨿ (a != x), option) (λ _ : a = x, some x)
90+
(λ _ : a != x, none) (deceq a x)
91+
| inr _ => none
92+
end) (λ _ : unit, match g (pr2 (unembed n)) with
93+
| inl _ | _ => none
94+
end) (f (pr1 (unembed n)))) (some x)).
95+
* exact X0.
96+
* apply propproperty.
97+
* intros [mm enumff].
98+
destruct (enumg x), (enumf x).
99+
apply pr3, hinhpr.
100+
destruct (unembed mm) as [m1 m2].
101+
use make_hfiber.
102+
-- exact m1.
103+
-- assert (eq : m1 = Preamble.pr1 (m1,, m2)).
104+
++ apply idpath.
105+
++ induction eq.
106+
assert (eq : m2 = Preamble.pr2 (m1,, m2)).
107+
apply idpath. induction eq.
108+
revert enumff.
109+
induction (g m2).
110+
induction (f m1). simpl.
111+
induction (deceq a0 a). simpl.
112+
induction a1.
113+
apply idfun.
114+
simpl; intros. apply fromempty.
115+
exact (nopathsnonesome x enumff).
116+
simpl; intros. apply fromempty.
117+
exact (nopathsnonesome x enumff).
118+
induction (f m1). simpl. intros. apply fromempty. exact (nopathsnonesome x enumff).
119+
simpl. intros. apply fromempty. exact (nopathsnonesome x enumff).
120+
* exact (hfiber
121+
(λ n : nat,
122+
coprod_rect (λ _ : X ⨿ unit, option)
123+
(λ a : X,
124+
match g (pr2 (unembed n)) with
125+
| inl x =>
126+
coprod_rect (λ _ : (a = x) ⨿ (a != x), option) (λ _ : a = x, some x)
127+
(λ _ : a != x, none) (deceq a x)
128+
| inr _ => none
129+
end) (λ _ : unit, match g (pr2 (unembed n)) with
130+
| inl _ | _ => none
131+
end) (f (pr1 (unembed n)))) (some x)).
132+
* exact X0.
133+
* apply propproperty.
134+
* intros [mm enumgg].
135+
destruct (enumg x), (enumf x).
136+
apply pr2, hinhpr.
137+
destruct (unembed mm) as [m1 m2].
138+
use make_hfiber.
139+
-- exact m2.
140+
-- assert (eq : m1 = Preamble.pr1 (m1,, m2)).
141+
++ apply idpath.
142+
++ induction eq.
143+
assert (eq : m2 = Preamble.pr2 (m1,, m2)).
144+
apply idpath. induction eq.
145+
revert enumgg.
146+
induction (g m2).
147+
induction (f m1). simpl.
148+
induction (deceq a0 a). simpl.
149+
induction a1.
150+
apply idfun.
151+
simpl; intros. apply fromempty.
152+
exact (nopathsnonesome x enumgg).
153+
simpl; intros. apply fromempty.
154+
exact (nopathsnonesome x enumgg).
155+
induction (f m1). simpl. intros. apply fromempty. exact (nopathsnonesome x enumgg).
156+
simpl. intros. apply fromempty. exact (nopathsnonesome x enumgg).
157+
Defined.
158+
159+
Lemma enumdisj {X : UU} (p q : X → hProp) : (predenum p) → (predenum q) → (predenum (λ x : X, p x ∨ q x)).
160+
Proof.
161+
intros [f enumff] [g enumgg].
162+
use tpair.
163+
- intros n.
164+
destruct (unembed n) as [m1 m2].
165+
induction m1.
166+
exact (f m2).
167+
exact (g m2).
168+
- simpl.
169+
intros x; split; intros.
170+
destruct (enumff x), (enumgg x); clear enumff enumgg.
171+
use squash_to_prop. exact (p x ⨿ q x). exact X0. apply propproperty. intros [px | qx]; clear X0.
172+
+ use squash_to_prop. exact (hfiber f (some x)). exact (pr1 px). apply propproperty. intros [m2 feq].
173+
apply hinhpr. use make_hfiber.
174+
exact (embed (0,, m2)). simpl.
175+
rewrite -> (unembedinv (0,, m2)). simpl. exact feq.
176+
+ use squash_to_prop. exact (hfiber g (some x)). exact (pr0 qx). apply propproperty. intros [m2 geq].
177+
apply hinhpr. use make_hfiber.
178+
exact (embed (1,, m2)). simpl.
179+
rewrite -> (unembedinv (1,, m2)). simpl. exact geq.
180+
+ use squash_to_prop.
181+
* exact (hfiber
182+
(λ n : nat,
183+
nat_rect (λ _ : nat, option) (f (pr2 (unembed n)))
184+
(λ (_ : nat) (_ : option), g (pr2 (unembed n))) (pr1 (unembed n)))
185+
(some x)).
186+
* exact X0.
187+
* apply propproperty.
188+
* clear X0. intros [n feq]. revert feq.
189+
destruct (unembed n) as [m1 m2].
190+
assert (eq1 : m1 = pr1 (m1,, m2)) by apply idpath.
191+
assert (eq2 : m2 = pr2 (m1,, m2)) by apply idpath.
192+
induction eq1, eq2.
193+
induction m1; intros; apply hinhpr.
194+
-- left.
195+
destruct (enumff x).
196+
apply pr2, hinhpr. exact (m2,, feq).
197+
-- right.
198+
destruct (enumgg x).
199+
apply pr2, hinhpr. exact (m2,, feq).
200+
Defined.
201+
202+
Lemma isenumerableconj {X : UU} (p q : X → hProp) : (isdeceq X) → (isenumerablepred p) → (isenumerablepred q) → (isenumerablepred (predconj p q)).
203+
Proof.
204+
intros.
205+
use squash_to_prop.
206+
exact (predenum p). exact X1. apply propproperty. intros.
207+
use squash_to_prop.
208+
exact (predenum q). exact X2. apply propproperty. intros.
209+
apply hinhpr. exact (enumconj p q X0 X3 X4).
210+
Qed.
211+
212+
Lemma isenumerabledisj {X : UU} (p q : X → hProp) : (isenumerablepred p) → (isenumerablepred q) → (isenumerablepred (preddisj p q)).
213+
Proof.
214+
intros.
215+
use squash_to_prop.
216+
- exact (predenum p).
217+
- exact X0.
218+
- apply propproperty.
219+
- intros.
220+
use squash_to_prop.
221+
+ exact (predenum q).
222+
+ exact X1.
223+
+ apply propproperty.
224+
+ intros. apply hinhpr.
225+
exact (enumdisj p q X2 X3).
226+
Qed.
227+
228+
End EnumerablePredicates.
229+
230+

0 commit comments

Comments
 (0)