helm/software/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: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
  19 (*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "num/quatern.ma".
  24 include "num/bool_lemmas.ma".
  25
  26 (* ********** *)
  27 (* QUATERNARI *)
  28 (* ********** *)
  29
  30 ndefinition quatern_destruct_aux ≝
  31 Πn1,n2:quatern.ΠP:Prop.n1 = n2 →
  32  match n1 with
  33   [ q0 ⇒ match n2 with [ q0 ⇒ P → P | _ ⇒ P ]
  34   | q1 ⇒ match n2 with [ q1 ⇒ P → P | _ ⇒ P ]
  35   | q2 ⇒ match n2 with [ q2 ⇒ P → P | _ ⇒ P ]
  36   | q3 ⇒ match n2 with [ q3 ⇒ P → P | _ ⇒ P ]
  37   ].
  38
  39 ndefinition quatern_destruct : quatern_destruct_aux.
  40  #n1; #n2; #P;
  41  nelim n1;
  42  ##[ ##1: nelim n2; nnormalize; #H;
  43           ##[ ##1: napply (λx:P.x)
  44           ##| ##*: napply False_ind;
  45                    nchange with (match q0 with [ q0 ⇒ False | _ ⇒ True ]);
  46                    nrewrite > H; nnormalize; napply I
  47           ##]
  48  ##| ##2: nelim n2; nnormalize; #H;
  49           ##[ ##2: napply (λx:P.x)
  50           ##| ##*: napply False_ind;
  51                    nchange with (match q1 with [ q1 ⇒ False | _ ⇒ True ]);
  52                    nrewrite > H; nnormalize; napply I
  53           ##]
  54  ##| ##3: nelim n2; nnormalize; #H;
  55           ##[ ##3: napply (λx:P.x)
  56           ##| ##*: napply False_ind;
  57                    nchange with (match q2 with [ q2 ⇒ False | _ ⇒ True ]);
  58                    nrewrite > H; nnormalize; napply I
  59           ##]
  60  ##| ##4: nelim n2; nnormalize; #H;
  61           ##[ ##4: napply (λx:P.x)
  62           ##| ##*: napply False_ind;
  63                    nchange with (match q3 with [ q3 ⇒ False | _ ⇒ True ]);
  64                    nrewrite > H; nnormalize; napply I
  65           ##]
  66  ##]
  67 nqed.
  68
  69 nlemma symmetric_eqqu : symmetricT quatern bool eq_qu.
  70  #n1; #n2;
  71  nelim n1;
  72  nelim n2;
  73  nnormalize;
  74  napply refl_eq.
  75 nqed.
  76
  77 nlemma eqqu_to_eq : ∀n1,n2.eq_qu n1 n2 = true → n1 = n2.
  78  #n1; #n2;
  79  ncases n1;
  80  ncases n2;
  81  nnormalize;
  82  ##[ ##1,6,11,16: #H; napply refl_eq
  83  ##| ##*: #H; napply (bool_destruct … H)
  84  ##]
  85 nqed.
  86
  87 nlemma eq_to_eqqu : ∀n1,n2.n1 = n2 → eq_qu n1 n2 = true.
  88  #n1; #n2;
  89  ncases n1;
  90  ncases n2;
  91  nnormalize;
  92  ##[ ##1,6,11,16: #H; napply refl_eq
  93  ##| ##*: #H; napply (quatern_destruct … H)
  94  ##]
  95 nqed.
  96
  97 nlemma neqqu_to_neq : ∀n1,n2.eq_qu n1 n2 = false → n1 ≠ n2.
  98  #n1; #n2;
  99  ncases n1;
 100  ncases n2;
 101  nnormalize;
 102  ##[ ##1,6,11,16: #H; napply (bool_destruct … H)
 103  ##| ##*: #H; #H1; napply (quatern_destruct … H1)
 104  ##]
 105 nqed.
 106
 107 nlemma neq_to_neqqu : ∀n1,n2.n1 ≠ n2 → eq_qu n1 n2 = false.
 108  #n1; #n2;
 109  ncases n1;
 110  ncases n2;
 111  nnormalize;
 112  ##[ ##1,6,11,16: #H; napply False_ind; napply (H (refl_eq …))
 113  ##| ##*: #H; napply refl_eq
 114  ##]
 115 nqed.