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 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Sviluppo: 2008-2010 *)
21 (* ********************************************************************** *)
23 include "common/comp.ma".
24 include "common/prod_base.ma".
25 include "num/bool_lemmas.ma".
31 nlemma pair_destruct_1 :
32 ∀T1,T2.∀x1,x2:T1.∀y1,y2:T2.
33 pair T1 T2 x1 y1 = pair T1 T2 x2 y2 → x1 = x2.
34 #T1; #T2; #x1; #x2; #y1; #y2; #H;
35 nchange with (match pair T1 T2 x2 y2 with [ pair a _ ⇒ x1 = a ]);
41 nlemma pair_destruct_2 :
42 ∀T1,T2.∀x1,x2:T1.∀y1,y2:T2.
43 pair T1 T2 x1 y1 = pair T1 T2 x2 y2 → y1 = y2.
44 #T1; #T2; #x1; #x2; #y1; #y2; #H;
45 nchange with (match pair T1 T2 x2 y2 with [ pair _ b ⇒ y1 = b ]);
51 nlemma symmetric_eqpair :
53 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
54 (symmetricT T1 bool f1) →
55 (symmetricT T2 bool f2) →
57 (eq_pair T1 T2 f1 f2 p1 p2 = eq_pair T1 T2 f1 f2 p2 p1)).
58 #T1; #T2; #f1; #f2; #H; #H1;
59 #p1; nelim p1; #x1; #y1;
60 #p2; nelim p2; #x2; #y2;
65 ##[ ##1: nrewrite > (H1 y1 y2); napply refl_eq
66 ##| ##2: napply refl_eq
72 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
73 (∀x,y:T1.x = y → f1 x y = true) →
74 (∀x,y:T2.x = y → f2 x y = true) →
76 (p1 = p2 → eq_pair T1 T2 f1 f2 p1 p2 = true)).
77 #T1; #T2; #f1; #f2; #H1; #H2;
78 #p1; nelim p1; #x1; #y1;
79 #p2; nelim p2; #x2; #y2; #H;
81 nrewrite > (H1 … (pair_destruct_1 … H));
83 nrewrite > (H2 … (pair_destruct_2 … H));
89 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
90 (∀x,y:T1.f1 x y = true → x = y) →
91 (∀x,y:T2.f2 x y = true → x = y) →
93 (eq_pair T1 T2 f1 f2 p1 p2 = true → p1 = p2)).
94 #T1; #T2; #f1; #f2; #H1; #H2;
95 #p1; nelim p1; #x1; #y1;
96 #p2; nelim p2; #x2; #y2; #H;
98 nletin K ≝ (H1 x1 x2);
99 ncases (f1 x1 x2) in H:(%) K:(%);
102 ##[ ##2: ndestruct (*napply (bool_destruct … H3)*) ##]
104 nrewrite > (H4 (refl_eq …));
105 nrewrite > (H2 y1 y2 H3);
109 nlemma decidable_pair :
111 (∀x,y:T1.decidable (x = y)) →
112 (∀x,y:T2.decidable (x = y)) →
113 (∀x,y:ProdT T1 T2.decidable (x = y)).
115 #x; nelim x; #xx1; #xx2;
116 #y; nelim y; #yy1; #yy2;
118 napply (or2_elim (xx1 = yy1) (xx1 ≠ yy1) ? (H xx1 yy1) ?);
119 ##[ ##2: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
120 nnormalize; #H3; napply (H2 (pair_destruct_1 T1 T2 … H3))
121 ##| ##1: #H2; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
122 ##[ ##2: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
123 nnormalize; #H4; napply (H3 (pair_destruct_2 T1 T2 … H4))
124 ##| ##1: #H3; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
125 nrewrite > H2; nrewrite > H3; napply refl_eq
130 nlemma neqpair_to_neq :
132 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
133 (∀x,y:T1.f1 x y = false → x ≠ y) →
134 (∀x,y:T2.f2 x y = false → x ≠ y) →
136 (eq_pair T1 T2 f1 f2 p1 p2 = false → p1 ≠ p2)).
137 #T1; #T2; #f1; #f2; #H1; #H2;
138 #p1; nelim p1; #x1; #y1;
139 #p2; nelim p2; #x2; #y2;
140 nchange with ((((f1 x1 x2) ⊗ (f2 y1 y2)) = false) → ?); #H;
142 napply (or2_elim ((f1 x1 x2) = false) ((f2 y1 y2) = false) ? (andb_false2 … H) ?);
143 ##[ ##1: #H4; napply (H1 x1 x2 H4); napply (pair_destruct_1 T1 T2 … H3)
144 ##| ##2: #H4; napply (H2 y1 y2 H4); napply (pair_destruct_2 T1 T2 … H3)
148 nlemma pair_destruct :
150 (∀x,y:T1.decidable (x = y)) →
151 (∀x,y:T2.decidable (x = y)) →
152 (∀x1,x2:T1.∀y1,y2:T2.
153 (pair T1 T2 x1 y1) ≠ (pair T1 T2 x2 y2) → x1 ≠ x2 ∨ y1 ≠ y2).
154 #T1; #T2; #H1; #H2; #x1; #x2; #y1; #y2;
156 napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?);
157 ##[ ##2: #H3; napply (or2_intro1 … H3)
158 ##| ##1: #H3; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
159 ##[ ##2: #H4; napply (or2_intro2 … H4)
160 ##| ##1: #H4; nrewrite > H3 in H:(%);
161 nrewrite > H4; #H; nelim (H (refl_eq …))
166 nlemma neq_to_neqpair :
168 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
169 (∀x,y:T1.decidable (x = y)) →
170 (∀x,y:T2.decidable (x = y)) →
171 (∀x,y:T1.x ≠ y → f1 x y = false) →
172 (∀x,y:T2.x ≠ y → f2 x y = false) →
174 (p1 ≠ p2 → eq_pair T1 T2 f1 f2 p1 p2 = false)).
175 #T1; #T2; #f1; #f2; #H1; #H2; #H3; #H4;
176 #p1; nelim p1; #x1; #y1;
177 #p2; nelim p2; #x2; #y2; #H;
178 nchange with (((f1 x1 x2) ⊗ (f2 y1 y2)) = false);
179 napply (or2_elim (x1 ≠ x2) (y1 ≠ y2) ? (pair_destruct T1 T2 H1 H2 … H) ?);
180 ##[ ##2: #H5; nrewrite > (H4 … H5); nrewrite > (andb_false2_2 (f1 x1 x2)); napply refl_eq
181 ##| ##1: #H5; nrewrite > (H3 … H5); nnormalize; napply refl_eq
185 nlemma pair_is_comparable :
186 comparable → comparable → comparable.
187 #T1; #T2; napply (mk_comparable (ProdT T1 T2));
188 ##[ napply (pair … (zeroc T1) (zeroc T2))
189 ##| napply (λP.(forallc T1)
191 (λe2.P (pair … e1 e2))))
192 ##| napply (eq_pair … (eqc T1) (eqc T2))
193 ##| napply (eqpair_to_eq … (eqc T1) (eqc T2));
194 ##[ napply (eqc_to_eq T1)
195 ##| napply (eqc_to_eq T2)
197 ##| napply (eq_to_eqpair … (eqc T1) (eqc T2));
198 ##[ napply (eq_to_eqc T1)
199 ##| napply (eq_to_eqc T2)
201 ##| napply (neqpair_to_neq … (eqc T1) (eqc T2));
202 ##[ napply (neqc_to_neq T1)
203 ##| napply (neqc_to_neq T2)
205 ##| napply (neq_to_neqpair … (eqc T1) (eqc T2));
206 ##[ napply (decidable_c T1)
207 ##| napply (decidable_c T2)
208 ##| napply (neq_to_neqc T1)
209 ##| napply (neq_to_neqc T2)
211 ##| napply decidable_pair;
212 ##[ napply (decidable_c T1)
213 ##| napply (decidable_c T2)
215 ##| napply symmetric_eqpair;
216 ##[ napply (symmetric_eqc T1)
217 ##| napply (symmetric_eqc T2)
222 unification hint 0 ≔ S1: comparable, S2: comparable;
223 T1 ≟ (carr S1), T2 ≟ (carr S2),
224 X ≟ (pair_is_comparable S1 S2)
225 (*********************************************) ⊢
226 carr X ≡ ProdT T1 T2.
232 nlemma triple_destruct_1 :
233 ∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
234 triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → x1 = x2.
235 #T1; #T2; #T3; #x1; #x2; #y1; #y2; #z1; #z2; #H;
236 nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple a _ _ ⇒ x1 = a ]);
242 nlemma triple_destruct_2 :
243 ∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
244 triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → y1 = y2.
245 #T1; #T2; #T3; #x1; #x2; #y1; #y2; #z1; #z2; #H;
246 nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple _ b _ ⇒ y1 = b ]);
252 nlemma triple_destruct_3 :
253 ∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
254 triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → z1 = z2.
255 #T1; #T2; #T3; #x1; #x2; #y1; #y2; #z1; #z2; #H;
256 nchange with (match triple T1 T2 T3 x2 y2 z2 with [ triple _ _ c ⇒ z1 = c ]);
262 nlemma symmetric_eqtriple :
264 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
265 (symmetricT T1 bool f1) →
266 (symmetricT T2 bool f2) →
267 (symmetricT T3 bool f3) →
268 (∀p1,p2:Prod3T T1 T2 T3.
269 (eq_triple T1 T2 T3 f1 f2 f3 p1 p2 = eq_triple T1 T2 T3 f1 f2 f3 p2 p1)).
270 #T1; #T2; #T3; #f1; #f2; #f3; #H; #H1; #H2;
271 #p1; nelim p1; #x1; #y1; #z1;
272 #p2; nelim p2; #x2; #y2; #z2;
274 nrewrite > (H x1 x2);
277 ##[ ##1: nrewrite > (H1 y1 y2);
280 ##[ ##1: nrewrite > (H2 z1 z2); napply refl_eq
281 ##| ##2: napply refl_eq
283 ##| ##2: napply refl_eq
287 nlemma eq_to_eqtriple :
289 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
290 (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) →
291 (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
292 (∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) →
293 (∀p1,p2:Prod3T T1 T2 T3.
294 (p1 = p2 → eq_triple T1 T2 T3 f1 f2 f3 p1 p2 = true)).
295 #T1; #T2; #T3; #f1; #f2; #f3; #H1; #H2; #H3;
296 #p1; nelim p1; #x1; #y1; #z1;
297 #p2; nelim p2; #x2; #y2; #z2; #H;
299 nrewrite > (H1 … (triple_destruct_1 … H));
301 nrewrite > (H2 … (triple_destruct_2 … H));
303 nrewrite > (H3 … (triple_destruct_3 … H));
307 nlemma eqtriple_to_eq :
309 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
310 (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) →
311 (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
312 (∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) →
313 (∀p1,p2:Prod3T T1 T2 T3.
314 (eq_triple T1 T2 T3 f1 f2 f3 p1 p2 = true → p1 = p2)).
315 #T1; #T2; #T3; #f1; #f2; #f3; #H1; #H2; #H3;
316 #p1; nelim p1; #x1; #y1; #z1;
317 #p2; nelim p2; #x2; #y2; #z2; #H;
319 nletin K ≝ (H1 x1 x2);
320 ncases (f1 x1 x2) in H:(%) K:(%);
322 ##[ ##2: #H4; ndestruct (*napply (bool_destruct … H4)*) ##]
323 nletin K1 ≝ (H2 y1 y2);
324 ncases (f2 y1 y2) in K1:(%) ⊢ %;
326 ##[ ##2: #H4; #H5; ndestruct (*napply (bool_destruct … H5)*) ##]
328 nrewrite > (H4 (refl_eq …));
329 nrewrite > (H6 (refl_eq …));
330 nrewrite > (H3 z1 z2 H5);
334 nlemma decidable_triple :
336 (∀x,y:T1.decidable (x = y)) →
337 (∀x,y:T2.decidable (x = y)) →
338 (∀x,y:T3.decidable (x = y)) →
339 (∀x,y:Prod3T T1 T2 T3.decidable (x = y)).
340 #T1; #T2; #T3; #H; #H1; #H2;
341 #x; nelim x; #xx1; #xx2; #xx3;
342 #y; nelim y; #yy1; #yy2; #yy3;
344 napply (or2_elim (xx1 = yy1) (xx1 ≠ yy1) ? (H xx1 yy1) ?);
345 ##[ ##2: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
346 nnormalize; #H4; napply (H3 (triple_destruct_1 T1 T2 T3 … H4))
347 ##| ##1: #H3; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
348 ##[ ##2: #H4; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
349 nnormalize; #H5; napply (H4 (triple_destruct_2 T1 T2 T3 … H5))
350 ##| ##1: #H4; napply (or2_elim (xx3 = yy3) (xx3 ≠ yy3) ? (H2 xx3 yy3) ?);
351 ##[ ##2: #H5; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
352 nnormalize; #H6; napply (H5 (triple_destruct_3 T1 T2 T3 … H6))
353 ##| ##1: #H5; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
363 nlemma neqtriple_to_neq :
365 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
366 (∀x,y:T1.f1 x y = false → x ≠ y) →
367 (∀x,y:T2.f2 x y = false → x ≠ y) →
368 (∀x,y:T3.f3 x y = false → x ≠ y) →
369 (∀p1,p2:Prod3T T1 T2 T3.
370 (eq_triple T1 T2 T3 f1 f2 f3 p1 p2 = false → p1 ≠ p2)).
371 #T1; #T2; #T3; #f1; #f2; #f3; #H1; #H2; #H3;
372 #p1; nelim p1; #x1; #y1; #z1;
373 #p2; nelim p2; #x2; #y2; #z2;
374 nchange with ((((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2)) = false) → ?); #H;
376 napply (or3_elim ((f1 x1 x2) = false) ((f2 y1 y2) = false) ((f3 z1 z2) = false) ? (andb_false3 … H) ?);
377 ##[ ##1: #H5; napply (H1 x1 x2 H5); napply (triple_destruct_1 T1 T2 T3 … H4)
378 ##| ##2: #H5; napply (H2 y1 y2 H5); napply (triple_destruct_2 T1 T2 T3 … H4)
379 ##| ##3: #H5; napply (H3 z1 z2 H5); napply (triple_destruct_3 T1 T2 T3 … H4)
383 nlemma triple_destruct :
385 (∀x,y:T1.decidable (x = y)) →
386 (∀x,y:T2.decidable (x = y)) →
387 (∀x,y:T3.decidable (x = y)) →
388 (∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
389 (triple T1 T2 T3 x1 y1 z1) ≠ (triple T1 T2 T3 x2 y2 z2) →
390 Or3 (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2)).
391 #T1; #T2; #T3; #H1; #H2; #H3; #x1; #x2; #y1; #y2; #z1; #z2;
393 napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?);
394 ##[ ##2: #H4; napply (or3_intro1 … H4)
395 ##| ##1: #H4; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
396 ##[ ##2: #H5; napply (or3_intro2 … H5)
397 ##| ##1: #H5; napply (or2_elim (z1 = z2) (z1 ≠ z2) ? (H3 z1 z2) ?);
398 ##[ ##2: #H6; napply (or3_intro3 … H6)
399 ##| ##1: #H6; nrewrite > H4 in H:(%);
401 nrewrite > H6; #H; nelim (H (refl_eq …))
407 nlemma neq_to_neqtriple :
409 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
410 (∀x,y:T1.decidable (x = y)) →
411 (∀x,y:T2.decidable (x = y)) →
412 (∀x,y:T3.decidable (x = y)) →
413 (∀x,y:T1.x ≠ y → f1 x y = false) →
414 (∀x,y:T2.x ≠ y → f2 x y = false) →
415 (∀x,y:T3.x ≠ y → f3 x y = false) →
416 (∀p1,p2:Prod3T T1 T2 T3.
417 (p1 ≠ p2 → eq_triple T1 T2 T3 f1 f2 f3 p1 p2 = false)).
418 #T1; #T2; #T3; #f1; #f2; #f3; #H1; #H2; #H3; #H4; #H5; #H6;
419 #p1; nelim p1; #x1; #y1; #z1;
420 #p2; nelim p2; #x2; #y2; #z2; #H;
421 nchange with (((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2)) = false);
422 napply (or3_elim (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) ? (triple_destruct T1 T2 T3 H1 H2 H3 … H) ?);
423 ##[ ##1: #H7; nrewrite > (H4 … H7); nrewrite > (andb_false3_1 (f2 y1 y2) (f3 z1 z2)); napply refl_eq
424 ##| ##2: #H7; nrewrite > (H5 … H7); nrewrite > (andb_false3_2 (f1 x1 x2) (f3 z1 z2)); napply refl_eq
425 ##| ##3: #H7; nrewrite > (H6 … H7); nrewrite > (andb_false3_3 (f1 x1 x2) (f2 y1 y2)); napply refl_eq
429 nlemma triple_is_comparable :
430 comparable → comparable → comparable → comparable.
431 #T1; #T2; #T3; napply (mk_comparable (Prod3T T1 T2 T3));
432 ##[ napply (triple … (zeroc T1) (zeroc T2) (zeroc T3))
433 ##| napply (λP.(forallc T1)
436 (λe3.P (triple … e1 e2 e3)))))
437 ##| napply (eq_triple … (eqc T1) (eqc T2) (eqc T3))
438 ##| napply (eqtriple_to_eq … (eqc T1) (eqc T2) (eqc T3));
439 ##[ napply (eqc_to_eq T1)
440 ##| napply (eqc_to_eq T2)
441 ##| napply (eqc_to_eq T3)
443 ##| napply (eq_to_eqtriple … (eqc T1) (eqc T2) (eqc T3));
444 ##[ napply (eq_to_eqc T1)
445 ##| napply (eq_to_eqc T2)
446 ##| napply (eq_to_eqc T3)
448 ##| napply (neqtriple_to_neq … (eqc T1) (eqc T2) (eqc T3));
449 ##[ napply (neqc_to_neq T1)
450 ##| napply (neqc_to_neq T2)
451 ##| napply (neqc_to_neq T3)
453 ##| napply (neq_to_neqtriple … (eqc T1) (eqc T2) (eqc T3));
454 ##[ napply (decidable_c T1)
455 ##| napply (decidable_c T2)
456 ##| napply (decidable_c T3)
457 ##| napply (neq_to_neqc T1)
458 ##| napply (neq_to_neqc T2)
459 ##| napply (neq_to_neqc T3)
461 ##| napply decidable_triple;
462 ##[ napply (decidable_c T1)
463 ##| napply (decidable_c T2)
464 ##| napply (decidable_c T3)
466 ##| napply symmetric_eqtriple;
467 ##[ napply (symmetric_eqc T1)
468 ##| napply (symmetric_eqc T2)
469 ##| napply (symmetric_eqc T3)
474 unification hint 0 ≔ S1: comparable, S2: comparable, S3: comparable;
475 T1 ≟ (carr S1), T2 ≟ (carr S2), T3 ≟ (carr S3),
476 X ≟ (triple_is_comparable S1 S2 S3)
477 (*********************************************) ⊢
478 carr X ≡ Prod3T T1 T2 T3.
484 nlemma quadruple_destruct_1 :
485 ∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
486 quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → x1 = x2.
487 #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
488 nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple a _ _ _ ⇒ x1 = a ]);
494 nlemma quadruple_destruct_2 :
495 ∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
496 quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → y1 = y2.
497 #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
498 nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ b _ _ ⇒ y1 = b ]);
504 nlemma quadruple_destruct_3 :
505 ∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
506 quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → z1 = z2.
507 #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
508 nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ _ c _ ⇒ z1 = c ]);
514 nlemma quadruple_destruct_4 :
515 ∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
516 quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → v1 = v2.
517 #T1; #T2; #T3; #T4; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #H;
518 nchange with (match quadruple T1 T2 T3 T4 x2 y2 z2 v2 with [ quadruple _ _ _ d ⇒ v1 = d ]);
524 nlemma symmetric_eqquadruple :
526 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
527 (symmetricT T1 bool f1) →
528 (symmetricT T2 bool f2) →
529 (symmetricT T3 bool f3) →
530 (symmetricT T4 bool f4) →
531 (∀p1,p2:Prod4T T1 T2 T3 T4.
532 (eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p1 p2 = eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p2 p1)).
533 #T1; #T2; #T3; #T4; #f1; #f2; #f3; #f4; #H; #H1; #H2; #H3;
534 #p1; nelim p1; #x1; #y1; #z1; #v1;
535 #p2; nelim p2; #x2; #y2; #z2; #v2;
537 nrewrite > (H x1 x2);
540 ##[ ##1: nrewrite > (H1 y1 y2);
543 ##[ ##1: nrewrite > (H2 z1 z2);
546 ##[ ##1: nrewrite > (H3 v1 v2); napply refl_eq
547 ##| ##2: napply refl_eq
549 ##| ##2: napply refl_eq
551 ##| ##2: napply refl_eq
555 nlemma eq_to_eqquadruple :
557 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
558 (∀x,y:T1.x = y → f1 x y = true) →
559 (∀x,y:T2.x = y → f2 x y = true) →
560 (∀x,y:T3.x = y → f3 x y = true) →
561 (∀x,y:T4.x = y → f4 x y = true) →
562 (∀p1,p2:Prod4T T1 T2 T3 T4.
563 (p1 = p2 → eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p1 p2 = true)).
564 #T1; #T2; #T3; #T4; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
565 #p1; nelim p1; #x1; #y1; #z1; #v1;
566 #p2; nelim p2; #x2; #y2; #z2; #v2; #H;
568 nrewrite > (H1 … (quadruple_destruct_1 … H));
570 nrewrite > (H2 … (quadruple_destruct_2 … H));
572 nrewrite > (H3 … (quadruple_destruct_3 … H));
574 nrewrite > (H4 … (quadruple_destruct_4 … H));
578 nlemma eqquadruple_to_eq :
580 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
581 (∀x,y:T1.f1 x y = true → x = y) →
582 (∀x,y:T2.f2 x y = true → x = y) →
583 (∀x,y:T3.f3 x y = true → x = y) →
584 (∀x,y:T4.f4 x y = true → x = y) →
585 (∀p1,p2:Prod4T T1 T2 T3 T4.
586 (eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p1 p2 = true → p1 = p2)).
587 #T1; #T2; #T3; #T4; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
588 #p1; nelim p1; #x1; #y1; #z1; #v1;
589 #p2; nelim p2; #x2; #y2; #z2; #v2; #H;
591 nletin K ≝ (H1 x1 x2);
592 ncases (f1 x1 x2) in H:(%) K:(%);
594 ##[ ##2: #H5; ndestruct (*napply (bool_destruct … H5)*) ##]
595 nletin K1 ≝ (H2 y1 y2);
596 ncases (f2 y1 y2) in K1:(%) ⊢ %;
598 ##[ ##2: #H5; #H6; ndestruct (*napply (bool_destruct … H6)*) ##]
599 nletin K2 ≝ (H3 z1 z2);
600 ncases (f3 z1 z2) in K2:(%) ⊢ %;
602 ##[ ##2: #H5; #H6; #H7; ndestruct (*napply (bool_destruct … H7)*) ##]
604 nrewrite > (H5 (refl_eq …));
605 nrewrite > (H6 (refl_eq …));
606 nrewrite > (H8 (refl_eq …));
607 nrewrite > (H4 v1 v2 H7);
611 nlemma decidable_quadruple :
613 (∀x,y:T1.decidable (x = y)) →
614 (∀x,y:T2.decidable (x = y)) →
615 (∀x,y:T3.decidable (x = y)) →
616 (∀x,y:T4.decidable (x = y)) →
617 (∀x,y:Prod4T T1 T2 T3 T4.decidable (x = y)).
618 #T1; #T2; #T3; #T4; #H; #H1; #H2; #H3;
619 #x; nelim x; #xx1; #xx2; #xx3; #xx4;
620 #y; nelim y; #yy1; #yy2; #yy3; #yy4;
622 napply (or2_elim (xx1 = yy1) (xx1 ≠ yy1) ? (H xx1 yy1) ?);
623 ##[ ##2: #H4; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
624 nnormalize; #H5; napply (H4 (quadruple_destruct_1 T1 T2 T3 T4 … H5))
625 ##| ##1: #H4; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
626 ##[ ##2: #H5; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
627 nnormalize; #H6; napply (H5 (quadruple_destruct_2 T1 T2 T3 T4 … H6))
628 ##| ##1: #H5; napply (or2_elim (xx3 = yy3) (xx3 ≠ yy3) ? (H2 xx3 yy3) ?);
629 ##[ ##2: #H6; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
630 nnormalize; #H7; napply (H6 (quadruple_destruct_3 T1 T2 T3 T4 … H7))
631 ##| ##1: #H6; napply (or2_elim (xx4 = yy4) (xx4 ≠ yy4) ? (H3 xx4 yy4) ?);
632 ##[ ##2: #H7; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
633 nnormalize; #H8; napply (H7 (quadruple_destruct_4 T1 T2 T3 T4 … H8))
634 ##| ##1: #H7; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
646 nlemma neqquadruple_to_neq :
648 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
649 (∀x,y:T1.f1 x y = false → x ≠ y) →
650 (∀x,y:T2.f2 x y = false → x ≠ y) →
651 (∀x,y:T3.f3 x y = false → x ≠ y) →
652 (∀x,y:T4.f4 x y = false → x ≠ y) →
653 (∀p1,p2:Prod4T T1 T2 T3 T4.
654 (eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p1 p2 = false → p1 ≠ p2)).
655 #T1; #T2; #T3; #T4; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
656 #p1; nelim p1; #x1; #y1; #z1; #v1;
657 #p2; nelim p2; #x2; #y2; #z2; #v2;
658 nchange with ((((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 v1 v2)) = false) → ?); #H;
660 napply (or4_elim ((f1 x1 x2) = false) ((f2 y1 y2) = false) ((f3 z1 z2) = false) ((f4 v1 v2) = false) ? (andb_false4 … H) ?);
661 ##[ ##1: #H6; napply (H1 x1 x2 H6); napply (quadruple_destruct_1 T1 T2 T3 T4 … H5)
662 ##| ##2: #H6; napply (H2 y1 y2 H6); napply (quadruple_destruct_2 T1 T2 T3 T4 … H5)
663 ##| ##3: #H6; napply (H3 z1 z2 H6); napply (quadruple_destruct_3 T1 T2 T3 T4 … H5)
664 ##| ##4: #H6; napply (H4 v1 v2 H6); napply (quadruple_destruct_4 T1 T2 T3 T4 … H5)
668 nlemma quadruple_destruct :
670 (∀x,y:T1.decidable (x = y)) →
671 (∀x,y:T2.decidable (x = y)) →
672 (∀x,y:T3.decidable (x = y)) →
673 (∀x,y:T4.decidable (x = y)) →
674 (∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
675 (quadruple T1 T2 T3 T4 x1 y1 z1 v1) ≠ (quadruple T1 T2 T3 T4 x2 y2 z2 v2) →
676 Or4 (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) (v1 ≠ v2)).
677 #T1; #T2; #T3; #T4; #H1; #H2; #H3; #H4;
678 #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2;
680 napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?);
681 ##[ ##2: #H5; napply (or4_intro1 … H5)
682 ##| ##1: #H5; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
683 ##[ ##2: #H6; napply (or4_intro2 … H6)
684 ##| ##1: #H6; napply (or2_elim (z1 = z2) (z1 ≠ z2) ? (H3 z1 z2) ?);
685 ##[ ##2: #H7; napply (or4_intro3 … H7)
686 ##| ##1: #H7; napply (or2_elim (v1 = v2) (v1 ≠ v2) ? (H4 v1 v2) ?);
687 ##[ ##2: #H8; napply (or4_intro4 … H8)
688 ##| ##1: #H8; nrewrite > H5 in H:(%);
691 nrewrite > H8; #H; nelim (H (refl_eq …))
698 nlemma neq_to_neqquadruple :
700 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
701 (∀x,y:T1.decidable (x = y)) →
702 (∀x,y:T2.decidable (x = y)) →
703 (∀x,y:T3.decidable (x = y)) →
704 (∀x,y:T4.decidable (x = y)) →
705 (∀x,y:T1.x ≠ y → f1 x y = false) →
706 (∀x,y:T2.x ≠ y → f2 x y = false) →
707 (∀x,y:T3.x ≠ y → f3 x y = false) →
708 (∀x,y:T4.x ≠ y → f4 x y = false) →
709 (∀p1,p2:Prod4T T1 T2 T3 T4.
710 (p1 ≠ p2 → eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p1 p2 = false)).
711 #T1; #T2; #T3; #T4; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4; #H5; #H6; #H7; #H8;
712 #p1; nelim p1; #x1; #y1; #z1; #v1;
713 #p2; nelim p2; #x2; #y2; #z2; #v2; #H;
714 nchange with (((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 v1 v2)) = false);
715 napply (or4_elim (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) (v1 ≠ v2) ? (quadruple_destruct T1 T2 T3 T4 H1 H2 H3 H4 … H) ?);
716 ##[ ##1: #H9; nrewrite > (H5 … H9); nrewrite > (andb_false4_1 (f2 y1 y2) (f3 z1 z2) (f4 v1 v2)); napply refl_eq
717 ##| ##2: #H9; nrewrite > (H6 … H9); nrewrite > (andb_false4_2 (f1 x1 x2) (f3 z1 z2) (f4 v1 v2)); napply refl_eq
718 ##| ##3: #H9; nrewrite > (H7 … H9); nrewrite > (andb_false4_3 (f1 x1 x2) (f2 y1 y2) (f4 v1 v2)); napply refl_eq
719 ##| ##4: #H9; nrewrite > (H8 … H9); nrewrite > (andb_false4_4 (f1 x1 x2) (f2 y1 y2) (f3 z1 z2)); napply refl_eq
723 nlemma quadruple_is_comparable :
724 comparable → comparable → comparable → comparable → comparable.
725 #T1; #T2; #T3; #T4; napply (mk_comparable (Prod4T T1 T2 T3 T4));
726 ##[ napply (quadruple … (zeroc T1) (zeroc T2) (zeroc T3) (zeroc T4))
727 ##| napply (λP.(forallc T1)
731 (λe4.P (quadruple … e1 e2 e3 e4))))))
732 ##| napply (eq_quadruple … (eqc T1) (eqc T2) (eqc T3) (eqc T4))
733 ##| napply (eqquadruple_to_eq … (eqc T1) (eqc T2) (eqc T3) (eqc T4));
734 ##[ napply (eqc_to_eq T1)
735 ##| napply (eqc_to_eq T2)
736 ##| napply (eqc_to_eq T3)
737 ##| napply (eqc_to_eq T4)
739 ##| napply (eq_to_eqquadruple … (eqc T1) (eqc T2) (eqc T3) (eqc T4));
740 ##[ napply (eq_to_eqc T1)
741 ##| napply (eq_to_eqc T2)
742 ##| napply (eq_to_eqc T3)
743 ##| napply (eq_to_eqc T4)
745 ##| napply (neqquadruple_to_neq … (eqc T1) (eqc T2) (eqc T3) (eqc T4));
746 ##[ napply (neqc_to_neq T1)
747 ##| napply (neqc_to_neq T2)
748 ##| napply (neqc_to_neq T3)
749 ##| napply (neqc_to_neq T4)
751 ##| napply (neq_to_neqquadruple … (eqc T1) (eqc T2) (eqc T3) (eqc T4));
752 ##[ napply (decidable_c T1)
753 ##| napply (decidable_c T2)
754 ##| napply (decidable_c T3)
755 ##| napply (decidable_c T4)
756 ##| napply (neq_to_neqc T1)
757 ##| napply (neq_to_neqc T2)
758 ##| napply (neq_to_neqc T3)
759 ##| napply (neq_to_neqc T4)
761 ##| napply decidable_quadruple;
762 ##[ napply (decidable_c T1)
763 ##| napply (decidable_c T2)
764 ##| napply (decidable_c T3)
765 ##| napply (decidable_c T4)
767 ##| napply symmetric_eqquadruple;
768 ##[ napply (symmetric_eqc T1)
769 ##| napply (symmetric_eqc T2)
770 ##| napply (symmetric_eqc T3)
771 ##| napply (symmetric_eqc T4)
776 unification hint 0 ≔ S1: comparable, S2: comparable, S3: comparable, S4: comparable;
777 T1 ≟ (carr S1), T2 ≟ (carr S2), T3 ≟ (carr S3), T4 ≟ (carr S4),
778 X ≟ (quadruple_is_comparable S1 S2 S3 S4)
779 (*********************************************) ⊢
780 carr X ≡ Prod4T T1 T2 T3 T4.
786 nlemma quintuple_destruct_1 :
787 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
788 quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → x1 = x2.
789 #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
790 nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple a _ _ _ _ ⇒ x1 = a ]);
796 nlemma quintuple_destruct_2 :
797 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
798 quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → y1 = y2.
799 #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
800 nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ b _ _ _ ⇒ y1 = b ]);
806 nlemma quintuple_destruct_3 :
807 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
808 quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → z1 = z2.
809 #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
810 nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ c _ _ ⇒ z1 = c ]);
816 nlemma quintuple_destruct_4 :
817 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
818 quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → v1 = v2.
819 #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
820 nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ _ d _ ⇒ v1 = d ]);
826 nlemma quintuple_destruct_5 :
827 ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
828 quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → w1 = w2.
829 #T1; #T2; #T3; #T4; #T5; #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; #H;
830 nchange with (match quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 with [ quintuple _ _ _ _ e ⇒ w1 = e ]);
836 nlemma symmetric_eqquintuple :
837 ∀T1,T2,T3,T4,T5:Type.
838 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
839 (symmetricT T1 bool f1) →
840 (symmetricT T2 bool f2) →
841 (symmetricT T3 bool f3) →
842 (symmetricT T4 bool f4) →
843 (symmetricT T5 bool f5) →
844 (∀p1,p2:Prod5T T1 T2 T3 T4 T5.
845 (eq_quintuple T1 T2 T3 T4 T5 f1 f2 f3 f4 f5 p1 p2 = eq_quintuple T1 T2 T3 T4 T5 f1 f2 f3 f4 f5 p2 p1)).
846 #T1; #T2; #T3; #T4; #T5; #f1; #f2; #f3; #f4; #f5; #H; #H1; #H2; #H3; #H4;
847 #p1; nelim p1; #x1; #y1; #z1; #v1; #w1;
848 #p2; nelim p2; #x2; #y2; #z2; #v2; #w2;
850 nrewrite > (H x1 x2);
853 ##[ ##1: nrewrite > (H1 y1 y2);
856 ##[ ##1: nrewrite > (H2 z1 z2);
859 ##[ ##1: nrewrite > (H3 v1 v2);
862 ##[ ##1: nrewrite > (H4 w1 w2); napply refl_eq
863 ##| ##2: napply refl_eq
865 ##| ##2: napply refl_eq
867 ##| ##2: napply refl_eq
869 ##| ##2: napply refl_eq
873 nlemma eq_to_eqquintuple :
875 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
876 (∀x,y:T1.x = y → f1 x y = true) →
877 (∀x,y:T2.x = y → f2 x y = true) →
878 (∀x,y:T3.x = y → f3 x y = true) →
879 (∀x,y:T4.x = y → f4 x y = true) →
880 (∀x,y:T5.x = y → f5 x y = true) →
881 (∀p1,p2:Prod5T T1 T2 T3 T4 T5.
882 (p1 = p2 → eq_quintuple T1 T2 T3 T4 T5 f1 f2 f3 f4 f5 p1 p2 = true)).
883 #T1; #T2; #T3; #T4; #T5; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
884 #p1; nelim p1; #x1; #y1; #z1; #v1; #w1;
885 #p2; nelim p2; #x2; #y2; #z2; #v2; #w2; #H;
887 nrewrite > (H1 … (quintuple_destruct_1 … H));
889 nrewrite > (H2 … (quintuple_destruct_2 … H));
891 nrewrite > (H3 … (quintuple_destruct_3 … H));
893 nrewrite > (H4 … (quintuple_destruct_4 … H));
895 nrewrite > (H5 … (quintuple_destruct_5 … H));
899 nlemma eqquintuple_to_eq :
901 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
902 (∀x,y:T1.f1 x y = true → x = y) →
903 (∀x,y:T2.f2 x y = true → x = y) →
904 (∀x,y:T3.f3 x y = true → x = y) →
905 (∀x,y:T4.f4 x y = true → x = y) →
906 (∀x,y:T5.f5 x y = true → x = y) →
907 (∀p1,p2:Prod5T T1 T2 T3 T4 T5.
908 (eq_quintuple T1 T2 T3 T4 T5 f1 f2 f3 f4 f5 p1 p2 = true → p1 = p2)).
909 #T1; #T2; #T3; #T4; #T5; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
910 #p1; nelim p1; #x1; #y1; #z1; #v1; #w1;
911 #p2; nelim p2; #x2; #y2; #z2; #v2; #w2; #H;
913 nletin K ≝ (H1 x1 x2);
914 ncases (f1 x1 x2) in H:(%) K:(%);
916 ##[ ##2: #H6; ndestruct (*napply (bool_destruct … H6)*) ##]
917 nletin K1 ≝ (H2 y1 y2);
918 ncases (f2 y1 y2) in K1:(%) ⊢ %;
920 ##[ ##2: #H6; #H7; ndestruct (*napply (bool_destruct … H7)*) ##]
921 nletin K2 ≝ (H3 z1 z2);
922 ncases (f3 z1 z2) in K2:(%) ⊢ %;
924 ##[ ##2: #H6; #H7; #H8; ndestruct (*napply (bool_destruct … H8)*) ##]
925 nletin K3 ≝ (H4 v1 v2);
926 ncases (f4 v1 v2) in K3:(%) ⊢ %;
928 ##[ ##2: #H6; #H7; #H8; #H9; ndestruct (*napply (bool_destruct … H9)*) ##]
929 #H6; #H7; #H8; #H9; #H10;
930 nrewrite > (H6 (refl_eq …));
931 nrewrite > (H7 (refl_eq …));
932 nrewrite > (H8 (refl_eq …));
933 nrewrite > (H10 (refl_eq …));
934 nrewrite > (H5 w1 w2 H9);
938 nlemma decidable_quintuple :
940 (∀x,y:T1.decidable (x = y)) →
941 (∀x,y:T2.decidable (x = y)) →
942 (∀x,y:T3.decidable (x = y)) →
943 (∀x,y:T4.decidable (x = y)) →
944 (∀x,y:T5.decidable (x = y)) →
945 (∀x,y:Prod5T T1 T2 T3 T4 T5.decidable (x = y)).
946 #T1; #T2; #T3; #T4; #T5; #H; #H1; #H2; #H3; #H4;
947 #x; nelim x; #xx1; #xx2; #xx3; #xx4; #xx5;
948 #y; nelim y; #yy1; #yy2; #yy3; #yy4; #yy5;
950 napply (or2_elim (xx1 = yy1) (xx1 ≠ yy1) ? (H xx1 yy1) ?);
951 ##[ ##2: #H5; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
952 nnormalize; #H6; napply (H5 (quintuple_destruct_1 T1 T2 T3 T4 T5 … H6))
953 ##| ##1: #H5; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
954 ##[ ##2: #H6; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
955 nnormalize; #H7; napply (H6 (quintuple_destruct_2 T1 T2 T3 T4 T5 … H7))
956 ##| ##1: #H6; napply (or2_elim (xx3 = yy3) (xx3 ≠ yy3) ? (H2 xx3 yy3) ?);
957 ##[ ##2: #H7; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
958 nnormalize; #H8; napply (H7 (quintuple_destruct_3 T1 T2 T3 T4 T5 … H8))
959 ##| ##1: #H7; napply (or2_elim (xx4 = yy4) (xx4 ≠ yy4) ? (H3 xx4 yy4) ?);
960 ##[ ##2: #H8; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
961 nnormalize; #H9; napply (H8 (quintuple_destruct_4 T1 T2 T3 T4 T5 … H9))
962 ##| ##1: #H8; napply (or2_elim (xx5 = yy5) (xx5 ≠ yy5) ? (H4 xx5 yy5) ?);
963 ##[ ##2: #H9; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
964 nnormalize; #H10; napply (H9 (quintuple_destruct_5 T1 T2 T3 T4 T5 … H10))
965 ##| ##1: #H9; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
979 nlemma neqquintuple_to_neq :
981 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
982 (∀x,y:T1.f1 x y = false → x ≠ y) →
983 (∀x,y:T2.f2 x y = false → x ≠ y) →
984 (∀x,y:T3.f3 x y = false → x ≠ y) →
985 (∀x,y:T4.f4 x y = false → x ≠ y) →
986 (∀x,y:T5.f5 x y = false → x ≠ y) →
987 (∀p1,p2:Prod5T T1 T2 T3 T4 T5.
988 (eq_quintuple T1 T2 T3 T4 T5 f1 f2 f3 f4 f5 p1 p2 = false → p1 ≠ p2)).
989 #T1; #T2; #T3; #T4; #T5; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
990 #p1; nelim p1; #x1; #y1; #z1; #v1; #w1;
991 #p2; nelim p2; #x2; #y2; #z2; #v2; #w2;
992 nchange with ((((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 v1 v2) ⊗ (f5 w1 w2)) = false) → ?); #H;
994 napply (or5_elim ((f1 x1 x2) = false) ((f2 y1 y2) = false) ((f3 z1 z2) = false) ((f4 v1 v2) = false) ((f5 w1 w2) = false) ? (andb_false5 … H) ?);
995 ##[ ##1: #H7; napply (H1 x1 x2 H7); napply (quintuple_destruct_1 T1 T2 T3 T4 T5 … H6)
996 ##| ##2: #H7; napply (H2 y1 y2 H7); napply (quintuple_destruct_2 T1 T2 T3 T4 T5 … H6)
997 ##| ##3: #H7; napply (H3 z1 z2 H7); napply (quintuple_destruct_3 T1 T2 T3 T4 T5 … H6)
998 ##| ##4: #H7; napply (H4 v1 v2 H7); napply (quintuple_destruct_4 T1 T2 T3 T4 T5 … H6)
999 ##| ##5: #H7; napply (H5 w1 w2 H7); napply (quintuple_destruct_5 T1 T2 T3 T4 T5 … H6)
1003 nlemma quintuple_destruct :
1005 (∀x,y:T1.decidable (x = y)) →
1006 (∀x,y:T2.decidable (x = y)) →
1007 (∀x,y:T3.decidable (x = y)) →
1008 (∀x,y:T4.decidable (x = y)) →
1009 (∀x,y:T5.decidable (x = y)) →
1010 (∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
1011 (quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1) ≠ (quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2) →
1012 Or5 (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) (v1 ≠ v2) (w1 ≠ w2)).
1013 #T1; #T2; #T3; #T4; #T5; #H1; #H2; #H3; #H4; #H5;
1014 #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2;
1016 napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?);
1017 ##[ ##2: #H6; napply (or5_intro1 … H6)
1018 ##| ##1: #H6; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
1019 ##[ ##2: #H7; napply (or5_intro2 … H7)
1020 ##| ##1: #H7; napply (or2_elim (z1 = z2) (z1 ≠ z2) ? (H3 z1 z2) ?);
1021 ##[ ##2: #H8; napply (or5_intro3 … H8)
1022 ##| ##1: #H8; napply (or2_elim (v1 = v2) (v1 ≠ v2) ? (H4 v1 v2) ?);
1023 ##[ ##2: #H9; napply (or5_intro4 … H9)
1024 ##| ##1: #H9; napply (or2_elim (w1 = w2) (w1 ≠ w2) ? (H5 w1 w2) ?);
1025 ##[ ##2: #H10; napply (or5_intro5 … H10)
1026 ##| ##1: #H10; nrewrite > H6 in H:(%);
1030 nrewrite > H10; #H; nelim (H (refl_eq …))
1038 nlemma neq_to_neqquintuple :
1040 ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
1041 (∀x,y:T1.decidable (x = y)) →
1042 (∀x,y:T2.decidable (x = y)) →
1043 (∀x,y:T3.decidable (x = y)) →
1044 (∀x,y:T4.decidable (x = y)) →
1045 (∀x,y:T5.decidable (x = y)) →
1046 (∀x,y:T1.x ≠ y → f1 x y = false) →
1047 (∀x,y:T2.x ≠ y → f2 x y = false) →
1048 (∀x,y:T3.x ≠ y → f3 x y = false) →
1049 (∀x,y:T4.x ≠ y → f4 x y = false) →
1050 (∀x,y:T5.x ≠ y → f5 x y = false) →
1051 (∀p1,p2:Prod5T T1 T2 T3 T4 T5.
1052 (p1 ≠ p2 → eq_quintuple T1 T2 T3 T4 T5 f1 f2 f3 f4 f5 p1 p2 = false)).
1053 #T1; #T2; #T3; #T4; #T5; #f1; #f2; #f3; #f4; #f5;
1054 #H1; #H2; #H3; #H4; #H5; #H6; #H7; #H8; #H9; #H10;
1055 #p1; nelim p1; #x1; #y1; #z1; #v1; #w1;
1056 #p2; nelim p2; #x2; #y2; #z2; #v2; #w2; #H;
1057 nchange with (((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 v1 v2) ⊗ (f5 w1 w2)) = false);
1058 napply (or5_elim (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) (v1 ≠ v2) (w1 ≠ w2) ? (quintuple_destruct T1 T2 T3 T4 T5 H1 H2 H3 H4 H5 … H) ?);
1059 ##[ ##1: #H11; nrewrite > (H6 … H11); nrewrite > (andb_false5_1 (f2 y1 y2) (f3 z1 z2) (f4 v1 v2) (f5 w1 w2)); napply refl_eq
1060 ##| ##2: #H11; nrewrite > (H7 … H11); nrewrite > (andb_false5_2 (f1 x1 x2) (f3 z1 z2) (f4 v1 v2) (f5 w1 w2)); napply refl_eq
1061 ##| ##3: #H11; nrewrite > (H8 … H11); nrewrite > (andb_false5_3 (f1 x1 x2) (f2 y1 y2) (f4 v1 v2) (f5 w1 w2)); napply refl_eq
1062 ##| ##4: #H11; nrewrite > (H9 … H11); nrewrite > (andb_false5_4 (f1 x1 x2) (f2 y1 y2) (f3 z1 z2) (f5 w1 w2)); napply refl_eq
1063 ##| ##5: #H11; nrewrite > (H10 … H11); nrewrite > (andb_false5_5 (f1 x1 x2) (f2 y1 y2) (f3 z1 z2) (f4 v1 v2)); napply refl_eq
1067 nlemma quintuple_is_comparable :
1068 comparable → comparable → comparable → comparable → comparable → comparable.
1069 #T1; #T2; #T3; #T4; #T5; napply (mk_comparable (Prod5T T1 T2 T3 T4 T5));
1070 ##[ napply (quintuple … (zeroc T1) (zeroc T2) (zeroc T3) (zeroc T4) (zeroc T5))
1071 ##| napply (λP.(forallc T1)
1076 (λe5.P (quintuple … e1 e2 e3 e4 e5)))))))
1077 ##| napply (eq_quintuple … (eqc T1) (eqc T2) (eqc T3) (eqc T4) (eqc T5))
1078 ##| napply (eqquintuple_to_eq … (eqc T1) (eqc T2) (eqc T3) (eqc T4) (eqc T5));
1079 ##[ napply (eqc_to_eq T1)
1080 ##| napply (eqc_to_eq T2)
1081 ##| napply (eqc_to_eq T3)
1082 ##| napply (eqc_to_eq T4)
1083 ##| napply (eqc_to_eq T5)
1085 ##| napply (eq_to_eqquintuple … (eqc T1) (eqc T2) (eqc T3) (eqc T4) (eqc T5));
1086 ##[ napply (eq_to_eqc T1)
1087 ##| napply (eq_to_eqc T2)
1088 ##| napply (eq_to_eqc T3)
1089 ##| napply (eq_to_eqc T4)
1090 ##| napply (eq_to_eqc T5)
1092 ##| napply (neqquintuple_to_neq … (eqc T1) (eqc T2) (eqc T3) (eqc T4) (eqc T5));
1093 ##[ napply (neqc_to_neq T1)
1094 ##| napply (neqc_to_neq T2)
1095 ##| napply (neqc_to_neq T3)
1096 ##| napply (neqc_to_neq T4)
1097 ##| napply (neqc_to_neq T5)
1099 ##| napply (neq_to_neqquintuple … (eqc T1) (eqc T2) (eqc T3) (eqc T4) (eqc T5));
1100 ##[ napply (decidable_c T1)
1101 ##| napply (decidable_c T2)
1102 ##| napply (decidable_c T3)
1103 ##| napply (decidable_c T4)
1104 ##| napply (decidable_c T5)
1105 ##| napply (neq_to_neqc T1)
1106 ##| napply (neq_to_neqc T2)
1107 ##| napply (neq_to_neqc T3)
1108 ##| napply (neq_to_neqc T4)
1109 ##| napply (neq_to_neqc T5)
1111 ##| napply decidable_quintuple;
1112 ##[ napply (decidable_c T1)
1113 ##| napply (decidable_c T2)
1114 ##| napply (decidable_c T3)
1115 ##| napply (decidable_c T4)
1116 ##| napply (decidable_c T5)
1118 ##| napply symmetric_eqquintuple;
1119 ##[ napply (symmetric_eqc T1)
1120 ##| napply (symmetric_eqc T2)
1121 ##| napply (symmetric_eqc T3)
1122 ##| napply (symmetric_eqc T4)
1123 ##| napply (symmetric_eqc T5)
1128 unification hint 0 ≔ S1: comparable, S2: comparable, S3: comparable, S4: comparable, S5: comparable;
1129 T1 ≟ (carr S1), T2 ≟ (carr S2), T3 ≟ (carr S3), T4 ≟ (carr S4), T5 ≟ (carr S5),
1130 X ≟ (quintuple_is_comparable S1 S2 S3 S4 S5)
1131 (*********************************************) ⊢
1132 carr X ≡ Prod5T T1 T2 T3 T4 T5.