-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathPrime.v
168 lines (130 loc) · 5.28 KB
/
Prime.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
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
(* -*- mode: coq; coq-prog-args: ("-allow-sprop") -*- *)
Require Import Relations.
Set Primitive Projections.
From Equations Require Import Equations.
Notation "{ x : A & P }" := (sigmaSP A (fun x => P)) : type_scope.
Notation "x .1" := (prSP1 x) (at level 3).
Notation "x .2" := (prSP2 x) (at level 3).
Notation " ( x ; p ) " := (sigmaSPI _ x p).
(** INTERNAL: Equations binding *)
(** This binds constants to use by Equations, only the sort, true and
false propositions are used by the Derive Invert command. Work is in
progress to use a general registration command as for sigma types below. *)
Require Import Equations.ConstantsSProp.
Register sigmaP as equations.sigmasP.type.
Register sigmaPI as equations.sigmasP.intro.
Register prP1 as equations.sigmasP.pr1.
Register prP2 as equations.sigmasP.pr2.
(** END INTERNAL: Equations binding *)
(** The standard library's le cannot be turned into a natural SProp *)
Fail Derive Invert for le.
(** Definable but squashed *)
Inductive le : nat -> nat -> SProp :=
| ind_le_0 n : le 0 n
| ind_le_S n m (H : le n m) : le (S n) (S m).
Fail Check (fun m n (H : le m n) => match H with ind_le_0 n => true | ind_le_S m n H => false end).
Derive Invert for le.
Check eq_refl : invert_le =
(fix le (var var0 : nat) {struct var} : SProp :=
match var with
| 0 => fun _ : nat => sTrue
| S n =>
fun var1 : nat =>
match var1 with
| 0 => sFalse
| S n0 => le n n0
end
end var0).
Infix "<=" := invert_le.
Infix "<" := (fun n m => S n <= m).
Definition le_0 : forall n, 0 <= n := fun n => sI.
Definition le_S : forall {m n}, m <= n -> S m <= S n := fun n m e => e.
(** The induction principle is not generated automatically yet. *)
Definition le_rect
(P : forall m n , m <= n -> Type)
(X0 : forall n : nat, P 0 n (le_0 n))
(XS : forall (m n : nat) (e:m <= n), P m n e -> P (S m) (S n) (le_S e))
: forall n m (e: n <= m), P n m e :=
fix le_rect (var var0 : nat) (var1 : var <= var0) {struct var} : P var var0 var1 :=
match var return (forall var0 (var1 : var <= var0), P var var0 var1) with
| 0 => fun (var0: nat) var1 => X0 var0
| S n0 =>
fun var0 : nat =>
match var0 with
| 0 => fun var1 => match var1 with end
| S n1 => fun var1 => XS n0 n1 var1 (le_rect n0 n1 var1)
end
end var0 var1.
Check (fun m n (H : invert_le m n) => le_rect (fun _ _ _ => bool) (fun n => true) (fun _ _ _ _ => false) m n H).
Definition minus_correct n m (e : n <= m) : n + (m - n) = m.
Proof.
generalize dependent n.
induction m; intros.
- destruct n. reflexivity. destruct e.
- destruct n. reflexivity. cbn in *. f_equal.
apply IHm; assumption.
Defined.
Inductive Divide : nat -> nat -> SProp :=
| divide_0' : forall n, Divide n 0
| divide_S' : forall n m (e: S n <= S m), Divide (S n) (m - n) -> Divide (S n) (S m).
Derive Invert for Divide.
Check eq_refl : invert_Divide =
fix invert_Divide var var0 {struct var0} : SProp :=
match var0 with
| 0 => sTrue
| S n =>
match var with
| 0 => fun _ : nat => sFalse
| S n0 =>
fun n1 : nat => {_ : S n0 <= S n1 & invert_Divide (S n0) (n1 - n0)}
end n
end.
Infix "|" := invert_Divide (at level 80).
Definition divide_0 n : n | 0 := sI.
Definition divide_S n m (e: S n <= S m) (H: S n | S m - S n) : S n | S m
:= (e;H).
Fixpoint divide_rect (P : forall n m, n | m -> Type)
(H0 : forall n : nat, P n 0 (divide_0 n))
(HS : forall (n m : nat) (e : S n <= S m) (d : S n | m - n),
P (S n) (m - n) d -> P (S n) (S m) (divide_S n m e d))
(n n0 : nat) (H : n | n0) {struct n0} : P n n0 H.
Proof.
destruct n0.
- exact (H0 n).
- destruct n. destruct H.
exact (HS n n0 H.1 H.2 (divide_rect P H0 HS (S n) (n0 - n) H.2)).
Defined.
Goal 5 | 145.
cbn. repeat econstructor.
Defined.
Goal (5 | 146) -> sFalse.
cbn. firstorder.
Defined.
(* Although we have definitional proof irrelevance for n | m, we can still extract the natural number
that witnesses the fact that n is a divisor of m out of the proof that n | m *)
Definition divide_to_nat {n m} : n | m -> nat :=
divide_rect (fun _ _ (_:_ | _) => nat) (fun _ => 0) (fun _ _ _ _ k => S k) n m.
Lemma divide_to_nat_correct n m (e:n | m): divide_to_nat e * n = m.
Proof.
refine (divide_rect (fun n m e => divide_to_nat e * n = m) _ _ n m e).
- intro n0. cbn. reflexivity.
- intros. cbn in *. f_equal. rewrite <- (minus_correct n0 m0 e0).
f_equal. exact H.
Defined.
Inductive is_gcd (a b g:nat) : SProp :=
is_gcd_intro :
(g | a) -> (g | b) -> (forall x, (x | a) -> (x | b) -> (x | g)) ->
is_gcd a b g.
Definition rel_prime (a b:nat) : SProp := is_gcd a b 1.
(* This definition gives us definitional proof irrelevance for prime, without paying the price of the definition of a decision procedure into booleans
(for instance using the sieve of Eratosthenes) and a proof that it corresponds to primality *)
Inductive prime (p:nat) : SProp :=
prime_intro :
1 < p -> (forall n, (1 <= n) -> (n < p) -> rel_prime n p) -> prime p.
Goal prime 13.
cbn. econstructor. exact sI. intro n.
destruct n. inversion 1. intros _ e. cbn in e.
repeat (try solve [firstorder];
destruct n; [ cbn; repeat econstructor; repeat (destruct x; firstorder) |]).
firstorder.
Defined.