1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "nat_ordered_set.ma".
16 include "models/q_support.ma".
17 include "models/list_support.ma".
18 include "logic/cprop_connectives.ma".
20 definition bar ≝ ℚ × (ℚ × ℚ).
22 notation < "\rationals \sup 2" non associative with precedence 90 for @{'q2}.
23 interpretation "Q x Q" 'q2 = (Prod Q Q).
25 definition empty_bar : bar ≝ 〈Qpos one,〈OQ,OQ〉〉.
26 notation "\rect" with precedence 90 for @{'empty_bar}.
27 interpretation "q0" 'empty_bar = empty_bar.
29 notation < "\ldots\rect\square\EmptySmallSquare\ldots" with precedence 90 for @{'lq2}.
30 interpretation "lq2" 'lq2 = (list bar).
32 definition q2_lt := mk_rel bar (λx,y:bar.\fst x < \fst y).
34 interpretation "bar lt" 'lt x y = (rel_op _ q2_lt x y).
36 lemma q2_trans : ∀a,b,c:bar. a < b → b < c → a < c.
37 intros 3; cases a; cases b; cases c; unfold q2_lt; simplify; intros;
38 apply (q_lt_trans ??? H H1);
41 definition q2_trel := mk_trans_rel bar q2_lt q2_trans.
43 interpretation "bar lt" 'lt x y = (FunClass_2_OF_trans_rel q2_trel x y).
45 definition canonical_q_lt : rel bar → trans_rel ≝ λx:rel bar.q2_trel.
47 coercion canonical_q_lt with nocomposites.
49 interpretation "bar lt" 'lt x y = (FunClass_2_OF_trans_rel (canonical_q_lt _) x y).
51 definition nth_base ≝ λf,n. \fst (\nth f ▭ n).
52 definition nth_height ≝ λf,n. \snd (\nth f ▭ n).
56 bars_sorted : sorted q2_lt bars;
57 bars_begin_OQ : nth_base bars O = OQ;
58 bars_end_OQ : nth_height bars (pred (\len bars)) = 〈OQ,OQ〉
61 lemma len_bases_gt_O: ∀f.O < \len (bars f).
62 intros; generalize in match (bars_begin_OQ f); cases (bars f); intros;
63 [2: simplify; apply le_S_S; apply le_O_n;
64 |1: normalize in H; destruct H;]
67 lemma all_bases_positive : ∀f:q_f.∀i. OQ < nth_base (bars f) (S i).
68 intro f; generalize in match (bars_begin_OQ f); generalize in match (bars_sorted f);
69 cases (len_gt_non_empty ?? (len_bases_gt_O f)); intros;
70 cases (cmp_nat (\len l) i);
71 [2: lapply (sorted_tail_bigger q2_lt ?? ▭ H ? H2) as K;
72 simplify in H1; rewrite < H1; apply K;
73 |1: simplify; elim l in i H2;[simplify; rewrite > nth_nil; apply (q_pos_OQ one)]
74 cases n in H3; intros; [simplify in H3; cases (not_le_Sn_O ? H3)]
75 apply (H2 n1); simplify in H3; apply (le_S_S_to_le ?? H3);]
78 alias symbol "lt" (instance 9) = "Q less than".
79 alias symbol "lt" (instance 7) = "natural 'less than'".
80 alias symbol "lt" (instance 6) = "natural 'less than'".
81 alias symbol "lt" (instance 5) = "Q less than".
82 alias symbol "lt" (instance 4) = "natural 'less than'".
83 alias symbol "lt" (instance 2) = "natural 'less than'".
84 alias symbol "leq" = "Q less or equal than".
85 coinductive value_spec (f : list bar) (i : ℚ) : ℚ × ℚ → CProp ≝
87 nth_height f j = q → nth_base f j < i → j < \len f →
88 (∀n.n<j → nth_base f n < i) →
89 (∀n.j < n → n < \len f → i ≤ nth_base f n) → value_spec f i q.
91 alias symbol "lt" (instance 5) = "Q less than".
92 alias symbol "lt" (instance 6) = "natural 'less than'".
93 definition value_lemma :
94 ∀f:list bar.sorted q2_lt f → O < length bar f →
95 ∀i:ratio.nth_base f O < Qpos i → ∃p:ℚ×ℚ.value_spec f (Qpos i) p.
96 intros (f bars_sorted_f len_bases_gt_O_f i bars_begin_OQ_f);
98 (λx:bar.match q_cmp (Qpos i) (\fst x) with[ q_leq _ ⇒ true| q_gt _ ⇒ false]);
99 exists [apply (nth_height f (pred (find ? P f ▭)));]
100 apply (value_of ?? (pred (find ? P f ▭)));
102 |2: cases (cases_find bar P f ▭);
103 [1: cases i1 in H H1 H2 H3; simplify; intros;
104 [1: generalize in match (bars_begin_OQ_f);
105 cases (len_gt_non_empty ?? (len_bases_gt_O_f)); simplify; intros;
107 |2: cases (len_gt_non_empty ?? (len_bases_gt_O_f)) in H3;
108 intros; lapply (H3 n (le_n ?)) as K; unfold P in K;
109 cases (q_cmp (Qpos i) (\fst (\nth (x::l) ▭ n))) in K;
110 simplify; intros; [destruct H5] assumption]
111 |2: destruct H; cases (len_gt_non_empty ?? (len_bases_gt_O_f)) in H2;
112 simplify; intros; lapply (H (\len l) (le_n ?)) as K; clear H;
113 unfold P in K; cases (q_cmp (Qpos i) (\fst (\nth (x::l) ▭ (\len l)))) in K;
114 simplify; intros; [destruct H2] assumption;]
115 |5: intro; cases (cases_find bar P f ▭); intros;
116 [1: generalize in match (bars_sorted_f);
117 cases (list_break ??? H) in H1; rewrite > H6;
118 rewrite < H1; simplify; rewrite > nth_len; unfold P;
119 cases (q_cmp (Qpos i) (\fst x)); simplify;
120 intros (X Hs); [2: destruct X] clear X;
121 cases (sorted_pivot q2_lt ??? ▭ Hs);
122 cut (\len l1 ≤ n) as Hn; [2:
123 rewrite > H1; cases i1 in H4; simplify; intro X; [2: assumption]
124 apply lt_to_le; assumption;]
125 unfold nth_base; rewrite > (nth_append_ge_len ????? Hn);
126 cut (n - \len l1 < \len (x::l2)) as K; [2:
127 simplify; rewrite > H1; rewrite > (?:\len l2 = \len f - \len (l1 @ [x]));[2:
128 rewrite > H6; repeat rewrite > len_append; simplify;
129 repeat rewrite < plus_n_Sm; rewrite < plus_n_O; simplify;
130 rewrite > sym_plus; rewrite < minus_plus_m_m; reflexivity;]
131 rewrite > len_append; rewrite > H1; simplify; rewrite < plus_n_SO;
132 apply le_S_S; clear H1 H6 H7 Hs H8 H9 Hn x l2 l1 H4 H3 H2 H P;
133 elim (\len f) in i1 n H5; [cases (not_le_Sn_O ? H);]
134 simplify; cases n2; [ repeat rewrite < minus_n_O; apply le_S_S_to_le; assumption]
135 cases n1 in H1; [intros; rewrite > eq_minus_n_m_O; apply le_O_n]
136 intros; simplify; apply H; apply le_S_S_to_le; assumption;]
137 cases (n - \len l1) in K; simplify; intros; [ assumption]
138 lapply (H9 ? (le_S_S_to_le ?? H10)) as W; apply (q_le_trans ??? H7);
139 apply q_lt_to_le; apply W;
140 |2: cases (not_le_Sn_n i1); rewrite > H in ⊢ (??%);
141 apply (trans_le ??? ? H4); cases i1 in H3; intros; apply le_S_S;
142 [ apply le_O_n; | assumption]]
143 |3: cases (cases_find bar P f ▭); [
144 cases i1 in H; intros; simplify; [assumption]
145 apply lt_S_to_lt; assumption;]
146 rewrite > H; cases (\len f) in len_bases_gt_O_f; intros; [cases (not_le_Sn_O ? H3)]
147 simplify; apply le_n;
148 |4: intros; cases (cases_find bar P f ▭) in H; simplify; intros;
149 [1: lapply (H3 n); [2: cases i1 in H4; intros [assumption] apply le_S; assumption;]
150 unfold P in Hletin; cases (q_cmp (Qpos i) (\fst (\nth f ▭ n))) in Hletin;
151 simplify; intros; [destruct H6] assumption;
152 |2: destruct H; cases f in len_bases_gt_O_f H2 H3; clear H1; simplify; intros;
153 [cases (not_le_Sn_O ? H)] lapply (H1 n); [2: apply le_S; assumption]
154 unfold P in Hletin; cases (q_cmp (Qpos i) (\fst (\nth (b::l) ▭ n))) in Hletin;
155 simplify; intros; [destruct H4] assumption;]]
158 lemma bars_begin_lt_Qpos : ∀q,r. nth_base (bars q) O<Qpos r.
159 intros; rewrite > bars_begin_OQ; apply q_pos_OQ;
162 lemma value : q_f → ratio → ℚ × ℚ.
163 intros; cases (value_lemma (bars q) ?? r);
165 | apply len_bases_gt_O;
167 | apply bars_begin_lt_Qpos;]
170 alias symbol "lt" (instance 5) = "natural 'less than'".
171 alias symbol "lt" (instance 4) = "Q less than".
173 ∀f:list bar.sorted q2_lt f → O < (length bar f) →
174 ∀i:ratio.nth_base f O < Qpos i → ℚ × ℚ.
175 intros; cases (value_lemma f H H1 i H2); assumption;
178 lemma cases_value : ∀f,i. value_spec (bars f) (Qpos i) (value f i).
179 intros; unfold value;
180 cases (value_lemma (bars f) (bars_sorted f) (len_bases_gt_O f) i (bars_begin_lt_Qpos f i));
184 lemma cases_value_simpl :
185 ∀f,H1,H2,i,Hi.value_spec f (Qpos i) (value_simpl f H1 H2 i Hi).
186 intros; unfold value_simpl; cases (value_lemma f H1 H2 i Hi);
190 definition same_values ≝ λl1,l2:q_f.∀input. value l1 input = value l2 input.
191 definition same_values_simpl ≝
192 λl1,l2:list bar.∀H1,H2,H3,H4,input,Hi1,Hi2.
193 value_simpl l1 H1 H2 input Hi1 = value_simpl l2 H3 H4 input Hi2.
197 Qpos i ≤ \fst x → value_simpl (y::x::l) H1 H2 i H3 = \snd y.
198 intros; cases (cases_value_simpl ? H1 H2 i H3);
199 cases j in H4 H5 H6 H7 H8 (j); simplify; intros;
200 [1: symmetry; assumption;
201 |2: cases (?:False); cases j in H4 H5 H6 H7 H8; intros;
202 [1: lapply (q_le_lt_trans ??? H H5) as K;cases (q_lt_corefl ? K);
203 |2: lapply (H7 1); [2: do 2 apply le_S_S; apply le_O_n;]
205 lapply (q_le_lt_trans ??? H Hletin) as K;cases (q_lt_corefl ? K);]]
208 lemma same_values_simpl_to_same_values:
209 ∀b1,b2,Hs1,Hs2,Hb1,Hb2,He1,He2,input.
210 same_values_simpl b1 b2 →
211 value (mk_q_f b1 Hs1 Hb1 He1) input =
212 value (mk_q_f b2 Hs2 Hb2 He2) input.
214 lapply (len_bases_gt_O (mk_q_f b1 Hs1 Hb1 He1));
215 lapply (len_bases_gt_O (mk_q_f b2 Hs2 Hb2 He2));
216 lapply (H ???? input) as K; try assumption;
217 [2: rewrite > Hb1; apply q_pos_OQ;
218 |3: rewrite > Hb2; apply q_pos_OQ;
222 include "russell_support.ma".
227 value_simpl (y::x::l) H1 H2 i H3 =
228 value_simpl (x::l) ?? i ?.
229 [1: apply hide; apply (sorted_tail q2_lt); [apply y| assumption]
230 |2: apply hide; simplify; apply le_S_S; apply le_O_n;
231 |3: apply hide; assumption;]
232 intros;cases (cases_value_simpl ? H1 H2 i H3);
233 generalize in ⊢ (? ? ? (? ? % ? ? ?)); intro;
234 generalize in ⊢ (? ? ? (? ? ? % ? ?)); intro;
235 generalize in ⊢ (? ? ? (? ? ? ? ? %)); intro;
236 cases (cases_value_simpl (x::l) H9 H10 i H11);
237 cut (j = S j1) as E; [ destruct E; destruct H12; reflexivity;]
238 clear H12 H4; cases j in H8 H5 H6 H7;
239 [1: intros;cases (?:False); lapply (H7 1 (le_n ?)); [2: simplify; do 2 apply le_S_S; apply le_O_n]
240 simplify in Hletin; apply (q_lt_corefl (\fst x));
241 apply (q_lt_le_trans ??? H Hletin);
242 |2: simplify; intros; clear q q1 j H11 H10 H1 H2; simplify in H3 H14; apply eq_f;
243 cases (cmp_nat n j1); [cases (cmp_nat j1 n);[apply le_to_le_to_eq; assumption]]
244 [1: clear H1; cases (?:False);
245 lapply (H7 (S j1)); [2: cases j1 in H2; intros[cases (not_le_Sn_O ? H1)] apply le_S_S; assumption]
246 [2: apply le_S_S; assumption;] simplify in Hletin;
247 apply (q_lt_corefl ? (q_le_lt_trans ??? Hletin H13));
249 lapply (H16 n); [2: assumption|3:simplify; apply le_S_S_to_le; assumption]
250 apply (q_lt_corefl ? (q_le_lt_trans ??? Hletin H4));]]
254 ∀x,i,h1,h2,h3.value_simpl [x] h1 h2 i h3 = \snd x.
255 intros; cases (cases_value_simpl [x] h1 h2 i h3); cases j in H H2; simplify;
256 intros; [2: cases (?:False); apply (not_le_Sn_O n); apply le_S_S_to_le; apply H2]
257 symmetry; assumption;
260 lemma same_value_tail:
261 ∀b,b1,h1,h3,xs,r1,input,H12,H13,Hi1,H14,H15,Hi2.
262 same_values_simpl (〈b1,h1〉::xs) (〈b1,h3〉::r1) →
263 value_simpl (b::〈b1,h1〉::xs) H12 H13 input Hi1
264 =value_simpl (b::〈b1,h3〉::r1) H14 H15 input Hi2.
265 intros; cases (q_cmp (Qpos input) b1);
266 [1: rewrite > (value_head 〈b1,h1〉 b xs); [2:assumption]
267 rewrite > (value_head 〈b1,h3〉 b r1); [2:assumption] reflexivity;
268 |2: rewrite > (value_tail 〈b1,h1〉 b xs);[2: assumption]
269 rewrite > (value_tail 〈b1,h3〉 b r1);[2: assumption] apply H;]
272 definition same_bases ≝ λl1,l2:list bar. ∀i.\fst (\nth l1 ▭ i) = \fst (\nth l2 ▭ i).
274 lemma same_bases_cons: ∀a,b,l1,l2.
275 same_bases l1 l2 → \fst a = \fst b → same_bases (a::l1) (b::l2).
276 intros; intro; cases i; simplify; [assumption;] apply (H n);
279 alias symbol "lt" = "Q less than".
280 lemma unpos: ∀x:ℚ.OQ < x → ∃r:ratio.Qpos r = x.
281 intro; cases x; intros; [2:exists [apply r] reflexivity]
283 [ apply (q_lt_corefl ? H)| cases (q_lt_le_incompat ?? (q_neg_gt ?) (q_lt_to_le ?? H))]
286 notation < "x \blacksquare" non associative with precedence 50 for @{'unpos $x}.
287 interpretation "hide unpos proof" 'unpos x = (unpos x _).