-
Notifications
You must be signed in to change notification settings - Fork 5
/
MoreDecidabilityFacts.v
124 lines (113 loc) · 3.39 KB
/
MoreDecidabilityFacts.v
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
Require Import Arith Lia Nat.
Require Import ConstructiveEpsilon.
From Undecidability.Synthetic Require Import DecidabilityFacts.
From FOL.Tennenbaum Require Import SyntheticInType CantorPairing.
(** Decidability of bounded quantifiers. *)
Lemma Dec_sigT_transport {X} p q :
Dec_sigT p -> (forall x : X, p x <-> q x) -> Dec_sigT q.
Proof.
intros Dec_p Equiv. intros x.
destruct (Dec_p x) as [H|H];
[left | right]; firstorder.
Qed.
Lemma dec_lt_bounded_sig N (p : nat -> Type) :
(forall x, p x + (p x -> False)) ->
{ x & ((x < N) * p x)%type } + (forall x, x < N -> p x -> False).
Proof.
intros Dec_p. induction N.
right. intros []; lia.
destruct (IHN) as [IH | IH].
- left. destruct IH as [x Hx].
exists x. split. destruct Hx. lia. apply Hx.
- destruct (Dec_p N) as [HN | HN].
+ left. exists N. split. lia. apply HN.
+ right. intros x Hx.
assert (x = N \/ x < N) as [->|] by lia; auto.
now apply IH.
Defined.
Lemma dec_lt_bounded_exist' N p :
Dec_sigT p ->
(exists x, x < N /\ p x) + (forall x, x < N -> ~ p x).
Proof.
intros Dec_p. induction N.
right. intros []; lia.
destruct (IHN) as [IH | IH].
- left. destruct IH as [x Hx].
exists x. split. lia. apply Hx.
- destruct (Dec_p N) as [HN | HN].
+ left. exists N. split. lia. apply HN.
+ right. intros x Hx.
assert (x = N \/ x < N) as [->|] by lia; auto.
Defined.
Lemma dec_lt_bounded_exist N p :
Dec_sigT p ->
dec (exists x, x < N /\ p x).
Proof.
intros Dec_p.
destruct (dec_lt_bounded_exist' N p Dec_p).
now left. right. firstorder.
Defined.
Lemma dec_lt_bounded_forall N p :
Dec_sigT p ->
dec (forall x, x < N -> p x).
Proof.
intros Dec_p. induction N.
left. lia.
destruct (Dec_p N) as [HN | HN].
- destruct (IHN) as [IH | IH].
+ left. intros x Hx.
assert (x = N \/ x < N) as [->|] by lia; auto.
+ right. intros H. apply IH.
intros x Hx. apply H. lia.
- right. intros H. apply HN.
apply H. lia.
Defined.
Lemma neg_lt_bounded_forall N p :
Dec_sigT p ->
(~ forall x, x < N -> p x) -> exists x, x < N /\ ~ p x.
Proof.
intros Hp H.
induction N. exfalso. apply H; lia.
destruct (Hp N).
- destruct IHN as [n ].
+ intros H1. apply H. intros.
assert (x = N \/ x < N) as [->|] by lia.
auto. now apply H1.
+ exists n. intuition lia.
- exists N. auto.
Qed.
(** Nat and (Nat * Nat) are witnessing. *)
Definition Witnessing_nat :
Witnessing nat.
Proof.
intros p Dec_p H.
specialize (constructive_indefinite_ground_description_nat p Dec_p H).
intros [x Hx]. now exists x.
Defined.
Theorem ProductWO (p : nat -> nat -> Prop) :
( forall x y, dec (p x y) ) ->
(exists x y, p x y) -> { x & { y & p x y }}.
Proof.
intros Dec_p H.
pose (P n := let (x, y) := decode n in p x y).
assert ({n & P n}) as [n Hn].
apply Witnessing_nat.
- intros n.
destruct (decode n) as [x y] eqn:E.
destruct (Dec_p x y); (left + right); unfold P; now rewrite E.
- destruct H as (x & y & H).
exists (code (x, y)). unfold P.
now rewrite inv_dc.
- destruct (decode n) as [x y] eqn:E.
exists x, y. unfold P in Hn; now rewrite E in Hn.
Qed.
Corollary Witnessing_natnat :
Witnessing (nat * nat).
Proof.
intros p Dec_p Hp.
pose (q x y := p (x, y)).
enough (forall x y, dec (q x y)) as (x & y & H)%ProductWO.
{ exists (x, y); apply H. }
{ destruct Hp as [[x y] H]. exists x, y; auto. }
intros x y. unfold q. apply Dec_p.
Qed.