No title

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
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
Require Import Arith.
Require Import Omega.

CoInductive conat :=
| cO : conat
| cS : conat -> conat.

(* A few helper definitions.*)
CoFixpoint inf : conat := cS inf.
Definition unfold_conat (c : conat) : conat :=
  match c with
  | cO => cO
  | cS c => cS c
  end.
Lemma unfold_conat_eq (c : conat) : c = unfold_conat c.
Proof.
  now destruct c.
Qed.

(* Co-inductive equality on conats. *)
CoInductive conat_eq : conat -> conat -> Prop :=
| conat_eq_O : conat_eq cO cO
| conat_eq_S : forall n1 n2, conat_eq n1 n2 -> conat_eq (cS n1) (cS n2).

(* You probably cannot prove this, but it should hold for any specific
   (and constructive) p. *)
Axiom conat_eq_fun : forall (p : conat -> bool) (c d : conat), conat_eq c d -> p c = p d.

(* Comparison of two conats. *)
CoInductive conat_lt (c : conat) : conat -> Prop :=
| conat_lt_c : conat_lt c (cS c)
| conat_lt_S : forall (d : conat), conat_lt c d -> conat_lt c (cS d).

Lemma conat_lt_O_S (c : conat) : conat_lt cO (cS c).
Proof.
  revert c. cofix.
  destruct c.
  - constructor.
  - constructor. apply conat_lt_O_S.
Qed.

(* Injection of nats into conats. *)
Fixpoint add_nat_to_conat (n : nat) (c : conat) : conat :=
  match n with
  | O => c
  | S n => cS (add_nat_to_conat n c)
  end.
Definition nat_to_conat (n : nat) : conat := add_nat_to_conat n cO.

(* Few helper lemmas about it. *)
Lemma add_nat_to_conat_cS (n : nat) (c : conat) :
  add_nat_to_conat n (cS c) = cS (add_nat_to_conat n c).
Proof.
  induction n.
  - reflexivity.
  - simpl. now f_equal.
Qed.

Lemma conat_lt_from_nat (n m : nat) : n < m -> conat_lt (nat_to_conat n) (nat_to_conat m).
Proof.
  induction 1.
  - rewrite (unfold_conat_eq (nat_to_conat (S n))). simpl.
    constructor.
  - rewrite (unfold_conat_eq (nat_to_conat (S m))). simpl.
    now constructor.
Qed.

Lemma add_nat_to_conat_sub_1 (n : nat) (c : conat) : n > 0 ->
  add_nat_to_conat (n - 1) (cS c) = add_nat_to_conat n c.
Proof.
  intros.
  replace n with (S (n - 1)) at 2 by omega.
  simpl. now rewrite add_nat_to_conat_cS.
Qed.

Lemma add_nat_to_conat_sub_1' (n : nat) (c : conat) : n > 0 ->
  add_nat_to_conat n c = cS (add_nat_to_conat (n - 1) c).
Proof.
  intros.
  now replace n with (S (n - 1)) at 1 by omega.
Qed.

(* Finit conats. *)
Definition lt_inf (c : conat) : Prop := exists n, c = nat_to_conat n.
Lemma lt_inf_S (c : conat) : lt_inf c -> lt_inf (cS c).
Proof.
  destruct 1. exists (S x).
  rewrite (unfold_conat_eq (nat_to_conat (S x))). simpl.
  now f_equal.
Qed.

(* Finally, your definition. *)
CoFixpoint root_main (p : conat -> bool) (i : conat) : conat :=
if p i
  then cO
  else cS (root_main p (cS i)).

Definition root (p : conat -> bool) : conat := root_main p cO.

(* Not useful in this case I think, but provable. *)
Lemma root_always_false :
  forall p : conat -> bool,
  (forall c, p c = false) -> conat_eq (root p) inf.
Proof.
  intros.
  unfold root. generalize cO.
  cofix. intros.
  rewrite (unfold_conat_eq (root_main p c)).
  rewrite (unfold_conat_eq inf).
  simpl. rewrite H. constructor.
  apply root_always_false.
Qed.

Lemma root_lt_inf_false :
  forall p : conat -> bool,
  (forall c, lt_inf c -> p c = false) -> conat_eq (root p) inf.
Proof.
  intros.
  unfold root.
  enough (forall (c : conat), lt_inf c -> conat_eq (root_main p c) inf).
  { apply H0. now exists 0. }
  cofix. intros.
  rewrite (unfold_conat_eq (root_main p c)).
  rewrite (unfold_conat_eq inf).
  simpl. rewrite H; [|assumption].
  constructor. apply root_lt_inf_false.
  now apply lt_inf_S.
Qed.

Lemma root_lt_precise :
  forall (p : conat -> bool) (c : conat),
  (lt_inf c /\ p c = true /\ (forall d, conat_lt d c -> p d = false)) -> root p = c.
Proof.
  intros. destruct H as [[n Hcn] [Hc H]].
  enough (forall m, m <= n -> add_nat_to_conat (n - m) (root_main p (nat_to_conat (n - m))) = c).
  { specialize (H0 n (le_n n)). rewrite Nat.sub_diag in H0. apply H0. }
  refine (nat_rect (fun m => m <= n ->
    add_nat_to_conat (n - m) (root_main p (nat_to_conat (n - m))) = c) _ _);
  intros; simpl in *; subst.
  - rewrite Nat.sub_0_r.
    rewrite (unfold_conat_eq (root_main p (nat_to_conat n))). simpl.
    now rewrite Hc.
  - intros.
    rewrite (unfold_conat_eq (root_main p (nat_to_conat (n - S n0)))). simpl.
    assert (p (nat_to_conat (n - S n0)) = false).
    { apply H. apply conat_lt_from_nat. omega. }
    rewrite H2.
    replace (cS (nat_to_conat (n - S n0))) with (nat_to_conat (n - n0)); swap 1 2.
    { unfold nat_to_conat. rewrite add_nat_to_conat_sub_1'; [|omega].
      f_equal. f_equal. omega. }
    rewrite <- H0; [|omega].
    rewrite <- add_nat_to_conat_sub_1 with (n := n - n0); [|omega].
    f_equal. omega.
Qed.

Lemma lt_inf_min :
  forall p : conat -> bool,
  (exists c, lt_inf c /\ p c = true) ->
  (exists c, (lt_inf c /\ p c = true /\ (forall d, conat_lt d c -> p d = false))).
Proof.
  (* TODO *)
  (* Should be provable... *)
Admitted.

Lemma root_lt_inf_correct :
  forall p : conat -> bool,
  (exists c, lt_inf c /\ p c = true) -> p (root p) = true.
Proof.
  intros. pose proof (lt_inf_min p H).
  destruct H0 as [c Hc].
  replace (root p) with c; [|symmetry; now apply root_lt_precise].
  apply Hc.
Qed.

Axiom lt_inf_or_not :
  forall p : conat -> bool,
  (exists c, is_true (p c)) ->
    ((exists c, lt_inf c /\ p c = true) \/ 
     ((forall c, lt_inf c -> p c = false) /\ p inf = true)).

Theorem root_correct :
  forall p : conat -> bool,
  (exists c, is_true (p c)) -> is_true (p (root p)).
Proof.
  intros. destruct (lt_inf_or_not p H).
  - now apply root_lt_inf_correct.
  - now rewrite conat_eq_fun with (c := root p) (d := inf); [|apply root_lt_inf_false].
Qed.