Skip to content

Commit ccdce1e

Browse files
klinashkaklinashka
committed
Finalized setup and added some files.
1 parent 3a0e18f commit ccdce1e

File tree

7 files changed

+368
-5
lines changed

7 files changed

+368
-5
lines changed

‎.gitignore‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,7 @@ nlia.cache
3030
nra.cache
3131
Makefile
3232
Makefile.conf
33+
*/CoqMakefile.conf
3334
*.d
3435
*.pdf
3536
*.log
@@ -38,4 +39,5 @@ Makefile.conf
3839
*.bbl
3940
*.blg
4041
*.vok
41-
*.vos
42+
*.vos
43+
_build/

‎code/Decidability/DecidablePredicates.v‎

Lines changed: 248 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,248 @@
1+
Require Import init.imports.
2+
3+
Section Definitions.
4+
5+
Definition isdecider {X : UU} (p : X → hProp) (f : X → bool) : UU := ∏ (x : X), (p x) <-> (f x = true).
6+
7+
Definition decider {X : UU} (p : X → hProp) : UU := ∑ (f : X → bool), (isdecider p f).
8+
9+
Definition deptypeddecider {X : UU} (p : X → hProp) : UU := ∏ (x : X), decidable (p x).
10+
11+
Definition decidable_pred {X : UU} : UU := ∑ (p : X → hProp), (deptypeddecider p).
12+
End Definitions.
13+
14+
Section Properties.
15+
Lemma isapropisdecider {X : UU} (p : X → hProp) (f : X → bool) : isaprop (isdecider p f).
16+
Proof.
17+
apply impred_isaprop.
18+
intro t.
19+
apply isapropdirprod; apply isapropimpl.
20+
- induction (f t).
21+
+ apply isapropifcontr.
22+
use iscontrloopsifisaset.
23+
exact isasetbool.
24+
+ apply isapropifnegtrue.
25+
exact nopathsfalsetotrue.
26+
- apply propproperty.
27+
Qed.
28+
29+
Lemma isapropdeptypeddecider {X : UU} (p : X → hProp) : isaprop (deptypeddecider p).
30+
Proof.
31+
apply impred_isaprop.
32+
intro t.
33+
apply isapropdec.
34+
apply propproperty.
35+
Qed.
36+
37+
Lemma decidertodeptypeddecider {X : UU} (p : X → hProp) : (decider p) → (deptypeddecider p).
38+
Proof.
39+
intros [f isdec] x.
40+
destruct (isdec x) as [isdec1 isdec2].
41+
induction (f x).
42+
- left.
43+
apply isdec2, idpath.
44+
- right; intro px.
45+
apply nopathsfalsetotrue, isdec1.
46+
exact px.
47+
Qed.
48+
49+
Lemma deptypeddecidertodecider {X : UU} (p : X → hProp) : (deptypeddecider p) → (decider p).
50+
Proof.
51+
intros dpd.
52+
use tpair.
53+
- intro x.
54+
induction (dpd x).
55+
+ exact true.
56+
+ exact false.
57+
- simpl.
58+
intro x.
59+
induction (dpd x); split.
60+
+ intro px.
61+
apply idpath.
62+
+ intro; exact a.
63+
+ intro; contradiction.
64+
+ intro.
65+
apply fromempty, nopathsfalsetotrue.
66+
exact X0.
67+
Qed.
68+
69+
70+
Lemma pathsbetweendeciders {X : UU} (p : X → hProp) (f g : X → bool) (isdecf : isdecider p f) (isdecg : isdecider p g) : f = g.
71+
Proof.
72+
apply funextsec.
73+
intro x.
74+
destruct (isdecf x) as [fa fb].
75+
destruct (isdecg x) as [ga gb].
76+
induction (g x).
77+
- set (px := gb (idpath true)).
78+
exact (fa px).
79+
- induction (f x).
80+
+ apply fromempty, nopathsfalsetotrue, ga, fb.
81+
exact (idpath true).
82+
+ exact (idpath false).
83+
Qed.
84+
85+
Lemma isapropdecider {X : UU} (p : X → hProp) : isaprop (decider p).
86+
Proof.
87+
apply invproofirrelevance.
88+
intros [f isdecf] [g isdecg].
89+
induction (pathsbetweendeciders p f g isdecf isdecg).
90+
assert (eq : isdecf = isdecg).
91+
- apply proofirrelevance.
92+
exact (isapropisdecider p f).
93+
- induction eq.
94+
exact (idpath (f,, isdecf)).
95+
Qed.
96+
97+
Lemma isweqdecidertodeptypeddecider {X : UU} (p : X → hProp) : (decider p) ≃ (deptypeddecider p).
98+
Proof.
99+
use make_weq.
100+
- exact (decidertodeptypeddecider p).
101+
- apply (isweqimplimpl).
102+
+ exact (deptypeddecidertodecider p).
103+
+ exact (isapropdecider p).
104+
+ exact (isapropdeptypeddecider p).
105+
Qed.
106+
107+
End Properties.
108+
109+
Section ClosureProperties.
110+
111+
Lemma decidabledisj {X : UU} (p q : X → hProp) : (deptypeddecider p) → (deptypeddecider q) → (deptypeddecider (λ (x : X), (p x) ∨ (q x))).
112+
Proof.
113+
intros decp decq x.
114+
induction (decp x).
115+
- left. apply hinhpr.
116+
left. exact a.
117+
- induction (decq x).
118+
+ left. apply hinhpr.
119+
right. exact a.
120+
+ right. intro.
121+
use squash_to_prop.
122+
* exact ((p x) ⨿ (q x)).
123+
* exact X0.
124+
* exact isapropempty.
125+
* exact (sumofmaps b b0).
126+
Qed.
127+
128+
Lemma decidableconj {X : UU} (p q : X → hProp) : (deptypeddecider p) → (deptypeddecider q) → (deptypeddecider (λ (x : X), (p x) ∧ (q x))).
129+
Proof.
130+
intros decp decq x.
131+
induction (decp x), (decq x).
132+
- left. exact (a,,h).
133+
- right. intros [pp qq]. exact (n qq).
134+
- right. intros [pp qq]. exact (b pp).
135+
- right. intros [pp qq]. exact (b pp).
136+
Qed.
137+
138+
Lemma decidableneg {X : UU} (p q : X → hProp) : (deptypeddecider p) → (deptypeddecider (λ (x : X), hneg (p x))).
139+
Proof.
140+
intros decp x.
141+
induction (decp x).
142+
- right. intros f. exact (f a).
143+
- left. exact b.
144+
Qed.
145+
146+
End ClosureProperties.
147+
148+
Section EqualityDeciders.
149+
150+
Definition iseqdecider (X : UU) (f : X → X → bool) : UU := ∏ (x1 x2 : X), x1 = x2 <-> f x1 x2 = true.
151+
152+
Definition eqdecider (X : UU) := ∑ (f : X → X → bool), (iseqdecider X f).
153+
154+
Definition make_eqdecider {X : UU} {f : X → X → bool} : (iseqdecider X f) → eqdecider (X) := (λ is : (iseqdecider X f), (f,, is)).
155+
156+
Lemma eqdecidertodeptypedeqdecider (X : UU) : (eqdecider X) → (isdeceq X).
157+
Proof.
158+
intros [f is] x y.
159+
destruct (is x y) as [impl1 impl2].
160+
induction (f x y).
161+
- left; apply impl2; apply idpath.
162+
- right. intros eq. apply nopathsfalsetotrue. exact (impl1 eq).
163+
Qed.
164+
165+
Lemma deptypedeqdecidertoeqdecider (X : UU) : (isdeceq X) → (eqdecider X).
166+
Proof.
167+
intros is.
168+
use tpair.
169+
- intros x y.
170+
induction (is x y).
171+
+ exact true.
172+
+ exact false.
173+
- intros x y.
174+
induction (is x y); simpl; split.
175+
+ exact (λ a : (x = y), (idpath true)).
176+
+ exact (λ b : (true = true), a).
177+
+ intros; apply fromempty; exact (b X0).
178+
+ intros; apply fromempty; exact (nopathsfalsetotrue X0).
179+
Qed.
180+
181+
Lemma eqdecidertoisapropeq (X : UU) (f : eqdecider X) : ∏ (x y : X) ,(isaprop (x = y)).
182+
Proof.
183+
intros x.
184+
apply isaproppathsfromisolated.
185+
intros y.
186+
set (dec := eqdecidertodeptypedeqdecider X f).
187+
apply (dec x).
188+
Qed.
189+
190+
Lemma isapropiseqdecider (X : UU) (f : X → X → bool) : (isaprop (iseqdecider X f)).
191+
Proof.
192+
apply isofhlevelsn.
193+
intros is.
194+
repeat (apply impred_isaprop + intros).
195+
apply isapropdirprod; apply isapropimpl.
196+
- induction (f t).
197+
+ apply isapropifcontr.
198+
use iscontrloopsifisaset.
199+
exact isasetbool.
200+
+ apply isapropifnegtrue.
201+
exact nopathsfalsetotrue.
202+
- apply eqdecidertoisapropeq.
203+
use make_eqdecider.
204+
+ exact f.
205+
+ exact is.
206+
Qed.
207+
208+
Lemma pathseqdeciders (X : UU) (f g : X → X → bool) (isf : iseqdecider X f) (isg : iseqdecider X g) : f = g.
209+
Proof.
210+
apply funextsec; intros x.
211+
apply funextsec; intros y.
212+
destruct (isf x y) as [implf1 implf2].
213+
destruct (isg x y) as [implg1 implg2].
214+
induction (g x y).
215+
- apply implf1; apply implg2.
216+
apply idpath.
217+
- induction (f x y).
218+
+ apply fromempty, nopathsfalsetotrue, implg1, implf2.
219+
exact (idpath true).
220+
+ exact (idpath false).
221+
Qed.
222+
223+
Lemma isapropeqdecider (X : UU) : (isaprop (eqdecider X)).
224+
Proof.
225+
apply invproofirrelevance.
226+
intros [f isf] [g isg].
227+
induction (pathseqdeciders X f g isf isg).
228+
assert (eq : isf = isg).
229+
- apply proofirrelevance.
230+
apply isapropiseqdecider.
231+
- induction eq.
232+
apply idpath.
233+
Qed.
234+
235+
Lemma weqisdeceqiseqdecider (X : UU) : (isdeceq X) ≃ (eqdecider X).
236+
Proof.
237+
use make_weq.
238+
- exact (deptypedeqdecidertoeqdecider X).
239+
- apply isweqimplimpl.
240+
+ exact (eqdecidertodeptypedeqdecider X).
241+
+ exact (isapropisdeceq X).
242+
+ exact (isapropeqdecider X).
243+
Qed.
244+
End EqualityDeciders.
245+
246+
Section ChoiceFunction.
247+
248+
End ChoiceFunction.

‎code/Decidability/DiscreteTypes.v‎

Lines changed: 103 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,103 @@
1+
Require Export UniMath.Foundations.All.
2+
3+
Section EqualityDeciders.
4+
5+
Definition iseqdecider (X : UU) (f : X → X → bool) : UU := ∏ (x1 x2 : X), x1 = x2 <-> f x1 x2 = true.
6+
7+
Definition eqdecider (X : UU) := ∑ (f : X → X → bool), (iseqdecider X f).
8+
9+
Definition make_eqdecider {X : UU} {f : X → X → bool} : (iseqdecider X f) → eqdecider (X) := (λ is : (iseqdecider X f), (f,, is)).
10+
11+
Lemma eqdecidertodeptypedeqdecider (X : UU) : (eqdecider X) → (isdeceq X).
12+
Proof.
13+
intros [f is] x y.
14+
destruct (is x y) as [impl1 impl2].
15+
induction (f x y).
16+
- left; apply impl2; apply idpath.
17+
- right. intros eq. apply nopathsfalsetotrue. exact (impl1 eq).
18+
Qed.
19+
20+
Lemma deptypedeqdecidertoeqdecider (X : UU) : (isdeceq X) → (eqdecider X).
21+
Proof.
22+
intros is.
23+
use tpair.
24+
- intros x y.
25+
induction (is x y).
26+
+ exact true.
27+
+ exact false.
28+
- intros x y.
29+
induction (is x y); simpl; split.
30+
+ exact (λ a : (x = y), (idpath true)).
31+
+ exact (λ b : (true = true), a).
32+
+ intros; apply fromempty; exact (b X0).
33+
+ intros; apply fromempty; exact (nopathsfalsetotrue X0).
34+
Qed.
35+
36+
Lemma eqdecidertoisapropeq (X : UU) (f : eqdecider X) : ∏ (x y : X) ,(isaprop (x = y)).
37+
Proof.
38+
intros x.
39+
apply isaproppathsfromisolated.
40+
intros y.
41+
set (dec := eqdecidertodeptypedeqdecider X f).
42+
apply (dec x).
43+
Qed.
44+
45+
Lemma isapropiseqdecider (X : UU) (f : X → X → bool) : (isaprop (iseqdecider X f)).
46+
Proof.
47+
apply isofhlevelsn.
48+
intros is.
49+
repeat (apply impred_isaprop + intros).
50+
apply isapropdirprod; apply isapropimpl.
51+
- induction (f t).
52+
+ apply isapropifcontr.
53+
use iscontrloopsifisaset.
54+
exact isasetbool.
55+
+ apply isapropifnegtrue.
56+
exact nopathsfalsetotrue.
57+
- apply eqdecidertoisapropeq.
58+
use make_eqdecider.
59+
+ exact f.
60+
+ exact is.
61+
Qed.
62+
63+
Lemma pathseqdeciders (X : UU) (f g : X → X → bool) (isf : iseqdecider X f) (isg : iseqdecider X g) : f = g.
64+
Proof.
65+
apply funextsec; intros x.
66+
apply funextsec; intros y.
67+
destruct (isf x y) as [implf1 implf2].
68+
destruct (isg x y) as [implg1 implg2].
69+
induction (g x y).
70+
- apply implf1; apply implg2.
71+
apply idpath.
72+
- induction (f x y).
73+
+ apply fromempty, nopathsfalsetotrue, implg1, implf2.
74+
exact (idpath true).
75+
+ exact (idpath false).
76+
Qed.
77+
78+
Lemma isapropeqdecider (X : UU) : (isaprop (eqdecider X)).
79+
Proof.
80+
apply invproofirrelevance.
81+
intros [f isf] [g isg].
82+
induction (pathseqdeciders X f g isf isg).
83+
assert (eq : isf = isg).
84+
- apply proofirrelevance.
85+
apply isapropiseqdecider.
86+
- induction eq.
87+
apply idpath.
88+
Qed.
89+
90+
Lemma weqisdeceqiseqdecider (X : UU) : (isdeceq X) ≃ (eqdecider X).
91+
Proof.
92+
use make_weq.
93+
- exact (deptypedeqdecidertoeqdecider X).
94+
- apply isweqimplimpl.
95+
+ exact (eqdecidertodeptypedeqdecider X).
96+
+ exact (isapropisdeceq X).
97+
+ exact (isapropeqdecider X).
98+
Qed.
99+
End EqualityDeciders.
100+
101+
Section ChoiceFunction.
102+
103+
End ChoiceFunction.

‎code/TestImports.v‎

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

‎code/_CoqProject‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
COQC = coqc
2+
COQDEP = coqdep
3+
-R . "sem"
4+
5+
-arg "-w -notation-overridden -type-in-type"
6+
7+
init/imports.v
8+
9+
Decidability/DecidablePredicates.v
10+
Decidability/DiscreteTypes.v
11+
12+

‎code/init/imports.v‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
Require Export UniMath.Foundations.All.

‎dune-project‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
(lang dune 3.16)
2-
(using coq 0.6)
2+
(using coq 0.8)
33
(name Computability)

0 commit comments

Comments
 (0)