]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/contribs/ng_assembly/num/quatern_lemmas.ma
wip ....
[helm.git] / matitaB / matita / contribs / ng_assembly / num / quatern_lemmas.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* ********************************************************************** *)
16 (*                          Progetto FreeScale                            *)
17 (*                                                                        *)
18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
19 (*   Sviluppo: 2008-2010                                                  *)
20 (*                                                                        *)
21 (* ********************************************************************** *)
22
23 include "num/quatern.ma".
24 include "num/bool_lemmas.ma".
25
26 (* ********** *)
27 (* QUATERNARI *)
28 (* ********** *)
29
30 (*
31 ndefinition quatern_destruct_aux ≝
32 Πn1,n2:quatern.ΠP:Prop.n1 = n2 →
33  match eq_qu n1 n2 with [ true ⇒ P → P | false ⇒ P ].
34
35 ndefinition quatern_destruct : quatern_destruct_aux.
36  #n1; #n2; #P; #H;
37  nrewrite < H;
38  nelim n1;
39  nnormalize;
40  napply (λx.x).
41 nqed.
42 *)
43
44 nlemma eq_to_eqqu : ∀n1,n2.n1 = n2 → eq_qu n1 n2 = true.
45  #n1; #n2; #H;
46  nrewrite > H;
47  nelim n2;
48  nnormalize;
49  napply refl_eq.
50 nqed.
51
52 nlemma neqqu_to_neq : ∀n1,n2.eq_qu n1 n2 = false → n1 ≠ n2.
53  #n1; #n2; #H;
54  napply (not_to_not (n1 = n2) (eq_qu n1 n2 = true) …);
55  ##[ ##1: napply (eq_to_eqqu n1 n2)
56  ##| ##2: napply (eqfalse_to_neqtrue … H)
57  ##]
58 nqed.
59
60 nlemma eqqu_to_eq : ∀n1,n2.eq_qu n1 n2 = true → n1 = n2.
61  #n1; #n2;
62  ncases n1;
63  ncases n2;
64  nnormalize;
65  ##[ ##1,6,11,16: #H; napply refl_eq
66  ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*)
67  ##]
68 nqed.
69
70 nlemma neq_to_neqqu : ∀n1,n2.n1 ≠ n2 → eq_qu n1 n2 = false.
71  #n1; #n2; #H;
72  napply (neqtrue_to_eqfalse (eq_qu n1 n2));
73  napply (not_to_not (eq_qu n1 n2 = true) (n1 = n2) ? H);
74  napply (eqqu_to_eq n1 n2).
75 nqed.
76
77 nlemma decidable_qu : ∀x,y:quatern.decidable (x = y).
78  #x; #y; nnormalize;
79  napply (or2_elim (eq_qu x y = true) (eq_qu x y = false) ? (decidable_bexpr ?));
80  ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqqu_to_eq … H))
81  ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqqu_to_neq … H))
82  ##]
83 nqed.
84
85 nlemma symmetric_eqqu : symmetricT quatern bool eq_qu.
86  #n1; #n2;
87  napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_qu n1 n2));
88  ##[ ##1: #H; nrewrite > H; napply refl_eq
89  ##| ##2: #H; nrewrite > (neq_to_neqqu n1 n2 H);
90           napply (symmetric_eq ? (eq_qu n2 n1) false);
91           napply (neq_to_neqqu n2 n1 (symmetric_neq ? n1 n2 H))
92  ##]
93 nqed.