-
Notifications
You must be signed in to change notification settings - Fork 0
/
minimizer_bool.v
145 lines (113 loc) · 3.76 KB
/
minimizer_bool.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
(**************************************************************)
(* Copyright Dominique Larchey-Wendling [*] *)
(* *)
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(**************************************************************)
Require Import Arith Omega.
Set Implicit Arguments.
Section nat_rev_ind.
(** A reverse recursion principle *)
Variables (P : nat -> Prop)
(HP : forall n, P (S n) -> P n).
Theorem nat_rev_ind x y : x <= y -> P y -> P x.
Proof. induction 1; auto. Qed.
End nat_rev_ind.
Section nat_rev_ind'.
(** A reverse recursion principle *)
Variables (P : nat -> Prop) (k : nat)
(HP : forall n, n < k -> P (S n) -> P n).
Theorem nat_rev_ind' x y : x <= y <= k -> P y -> P x.
Proof.
intros H1 H2.
set (Q n := n <= k /\ P n).
assert (forall x y, x <= y -> Q y -> Q x) as H.
apply nat_rev_ind.
intros n (H3 & H4); split.
omega.
revert H4; apply HP, H3.
apply (H x y).
omega.
split; auto; omega.
Qed.
End nat_rev_ind'.
Section minimizer_bool.
Variable (T F : nat -> Prop)
(HFun : forall n, T n -> F n -> False)
(HComp : forall n, T n \/ F n -> { T n } + { F n }).
Definition minimizer n := T n /\ forall i, i < n -> F i.
Fact minimizer_fun n m : minimizer n -> minimizer m -> n = m.
Proof.
intros (H1 & H2) (H3 & H4).
destruct (lt_eq_lt_dec n m) as [ [ H | ] | H ]; auto.
* apply H4 in H; destruct (@HFun n); auto.
* apply H2 in H; destruct (@HFun m); auto.
Qed.
Inductive bar n : Prop :=
| in_bar_0 : T n -> bar n
| in_bar_1 : F n -> bar (S n) -> bar n.
Let bar_ex n : bar n -> T n \/ F n.
Proof. induction 1; auto. Qed.
Let loop : forall n, bar n -> { k | T k /\ forall i, n <= i < k -> F i }.
Proof.
refine (fix loop n Hn { struct Hn } := match HComp (bar_ex Hn) with
| left H => exist _ n _
| right H => match loop (S n) _ with
| exist _ k Hk => exist _ k _
end
end).
* split; trivial.
intros; omega.
* destruct Hn; trivial.
destruct (@HFun n); trivial.
* destruct Hk as (H1 & H2); split; trivial.
intros i Hi; destruct (eq_nat_dec i n).
- subst; trivial.
- apply H2; omega.
Qed.
Hypothesis Hmin : ex minimizer.
Let bar_0 : bar 0.
Proof.
destruct Hmin as (k & H1 & H2).
apply in_bar_0 in H1.
revert H1.
apply nat_rev_ind' with (k := k).
intros i H3.
apply in_bar_1, H2; trivial.
omega.
Qed.
Definition minimizer_bool_coq : sig minimizer.
Proof.
destruct (loop bar_0) as (k & H1 & H2).
exists k; split; auto.
intros; apply H2; omega.
Defined.
End minimizer_bool.
Section minimizer.
Variable (R : nat -> nat -> Prop)
(Rfun : forall n u v, R n u -> R n v -> u = v)
(HR : forall n, ex (R n) -> sig (R n)).
Let T n := R n 0.
Let F n := exists u, R n (S u).
Definition minimizer_coq : ex (@minimizer T F) -> sig (@minimizer T F).
Proof.
apply minimizer_bool_coq.
intros n H1 (u & H2).
generalize (Rfun H1 H2); discriminate.
intros n Hn.
refine (match @HR n _ with
| exist _ u Hu => match u as m return R _ m -> _ with
| 0 => fun H => left H
| S v => fun H => right (ex_intro _ v H)
end Hu
end).
destruct Hn as [ Hn | (u & Hu) ].
- exists 0; auto.
- exists (S u); auto.
Defined.
End minimizer.
Check minimizer_coq.
Print Assumptions minimizer_coq.
Extraction "minimizer.ml" minimizer_bool_coq minimizer_coq.