blob: 0307a6a644db2a9d5c47337dacf6fcf563219a33 (
plain)
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
|
Require Import ZArith.
Require Import ConstructiveEpsilon.
Definition Z_inj_nat (z : Z) : nat :=
match z with
| Z0 => 0
| Zpos p => Pos.to_nat (p~0)
| Zneg p => Pos.to_nat (Pos.pred_double p)
end.
Definition Z_inj_nat_rev (n : nat) : Z :=
match n with
| O => 0
| S n' => match Pos.of_nat n with
| xH => Zneg xH
| xO p => Zpos p
| xI p => Zneg (Pos.succ p)
end
end.
Lemma Pos_pred_double_inj: forall (p q : positive),
Pos.pred_double p = Pos.pred_double q -> p = q.
Proof.
intros p q H.
apply (f_equal Pos.succ) in H.
do 2 rewrite Pos.succ_pred_double in H.
inversion H; reflexivity.
Qed.
Lemma Z_inj_nat_id: forall (z : Z),
Z_inj_nat_rev (Z_inj_nat z) = z.
Proof.
intros z.
unfold Z_inj_nat, Z_inj_nat_rev.
destruct z eqn:Hdz.
- reflexivity.
- rewrite Pos2Nat.id.
destruct (Pos.to_nat p~0) eqn:Hd.
+ pose proof Pos2Nat.is_pos p~0 as H.
rewrite <- Nat.neq_0_lt_0 in H.
exfalso; apply H, Hd.
+ reflexivity.
- rewrite Pos2Nat.id.
destruct (Pos.to_nat (Pos.pred_double p)) eqn: Hd.
+ pose proof Pos2Nat.is_pos (Pos.pred_double p) as H.
rewrite <- Nat.neq_0_lt_0 in H.
exfalso; apply H, Hd.
+ destruct (Pos.pred_double p) eqn:Hd2.
* rewrite <- Pos.pred_double_succ in Hd2.
apply Pos_pred_double_inj in Hd2.
rewrite Hd2; reflexivity.
* apply (f_equal Pos.succ) in Hd2.
rewrite Pos.succ_pred_double in Hd2.
rewrite <- Pos.xI_succ_xO in Hd2.
inversion Hd2.
* change xH with (Pos.pred_double xH) in Hd2.
apply Pos_pred_double_inj in Hd2.
rewrite Hd2; reflexivity.
Qed.
Lemma Z_inj_nat_inj: forall (x y : Z),
Z_inj_nat x = Z_inj_nat y -> x = y.
Proof.
intros x y H.
apply (f_equal Z_inj_nat_rev) in H.
do 2 rewrite Z_inj_nat_id in H.
assumption.
Qed.
Lemma constructive_indefinite_ground_description_Z:
forall P : Z -> Prop,
(forall z : Z, {P z} + {~ P z}) ->
(exists z : Z, P z) -> {z : Z | P z}.
Proof.
apply (constructive_indefinite_ground_description Z Z_inj_nat Z_inj_nat_rev Z_inj_nat_id).
Qed.
|
