helm/software/matita/contribs/ng_assembly/num/oct_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 (*   Ultima modifica: 05/08/2009                                          *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "num/oct.ma".
  24 include "num/bool_lemmas.ma".
  25
  26 (* ****** *)
  27 (* OTTALI *)
  28 (* ****** *)
  29
  30 ndefinition oct_destruct_aux ≝
  31 Πn1,n2:oct.ΠP:Prop.n1 = n2 →
  32  match n1 with
  33   [ o0 ⇒ match n2 with [ o0 ⇒ P → P | _ ⇒ P ]
  34   | o1 ⇒ match n2 with [ o1 ⇒ P → P | _ ⇒ P ]
  35   | o2 ⇒ match n2 with [ o2 ⇒ P → P | _ ⇒ P ]
  36   | o3 ⇒ match n2 with [ o3 ⇒ P → P | _ ⇒ P ]
  37   | o4 ⇒ match n2 with [ o4 ⇒ P → P | _ ⇒ P ]
  38   | o5 ⇒ match n2 with [ o5 ⇒ P → P | _ ⇒ P ]
  39   | o6 ⇒ match n2 with [ o6 ⇒ P → P | _ ⇒ P ]
  40   | o7 ⇒ match n2 with [ o7 ⇒ P → P | _ ⇒ P ]
  41   ].
  42
  43 ndefinition oct_destruct : oct_destruct_aux.
  44  #n1; #n2; #P;
  45  nelim n1;
  46  ##[ ##1: nelim n2; nnormalize; #H;
  47           ##[ ##1: napply (λx:P.x)
  48           ##| ##*: napply False_ind;
  49                    nchange with (match o0 with [ o0 ⇒ False | _ ⇒ True ]);
  50                    nrewrite > H; nnormalize; napply I
  51           ##]
  52  ##| ##2: nelim n2; nnormalize; #H;
  53           ##[ ##2: napply (λx:P.x)
  54           ##| ##*: napply False_ind;
  55                    nchange with (match o1 with [ o1 ⇒ False | _ ⇒ True ]);
  56                    nrewrite > H; nnormalize; napply I
  57           ##]
  58  ##| ##3: nelim n2; nnormalize; #H;
  59           ##[ ##3: napply (λx:P.x)
  60           ##| ##*: napply False_ind;
  61                    nchange with (match o2 with [ o2 ⇒ False | _ ⇒ True ]);
  62                    nrewrite > H; nnormalize; napply I
  63           ##]
  64  ##| ##4: nelim n2; nnormalize; #H;
  65           ##[ ##4: napply (λx:P.x)
  66           ##| ##*: napply False_ind;
  67                    nchange with (match o3 with [ o3 ⇒ False | _ ⇒ True ]);
  68                    nrewrite > H; nnormalize; napply I
  69           ##]
  70  ##| ##5: nelim n2; nnormalize; #H;
  71           ##[ ##5: napply (λx:P.x)
  72           ##| ##*: napply False_ind;
  73                    nchange with (match o4 with [ o4 ⇒ False | _ ⇒ True ]);
  74                    nrewrite > H; nnormalize; napply I
  75           ##]
  76  ##| ##6: nelim n2; nnormalize; #H;
  77           ##[ ##6: napply (λx:P.x)
  78           ##| ##*: napply False_ind;
  79                    nchange with (match o5 with [ o5 ⇒ False | _ ⇒ True ]);
  80                    nrewrite > H; nnormalize; napply I
  81           ##]
  82  ##| ##7: nelim n2; nnormalize; #H;
  83           ##[ ##7: napply (λx:P.x)
  84           ##| ##*: napply False_ind;
  85                    nchange with (match o6 with [ o6 ⇒ False | _ ⇒ True ]);
  86                    nrewrite > H; nnormalize; napply I
  87           ##]
  88  ##| ##8: nelim n2; nnormalize; #H;
  89           ##[ ##8: napply (λx:P.x)
  90           ##| ##*: napply False_ind;
  91                    nchange with (match o7 with [ o7 ⇒ False | _ ⇒ True ]);
  92                    nrewrite > H; nnormalize; napply I
  93           ##]
  94  ##]
  95 nqed.
  96
  97 nlemma symmetric_eqoct : symmetricT oct bool eq_oct.
  98  #n1; #n2;
  99  nelim n1;
 100  nelim n2;
 101  nnormalize;
 102  napply refl_eq.
 103 nqed.
 104
 105 nlemma eqoct_to_eq : ∀n1,n2.eq_oct n1 n2 = true → n1 = n2.
 106  #n1; #n2;
 107  ncases n1;
 108  ncases n2;
 109  nnormalize;
 110  ##[ ##1,10,19,28,37,46,55,64: #H; napply refl_eq
 111  ##| ##*: #H; napply (bool_destruct … H)
 112  ##]
 113 nqed.
 114
 115 nlemma eq_to_eqoct : ∀n1,n2.n1 = n2 → eq_oct n1 n2 = true.
 116  #n1; #n2;
 117  ncases n1;
 118  ncases n2;
 119  nnormalize;
 120  ##[ ##1,10,19,28,37,46,55,64: #H; napply refl_eq
 121  ##| ##*: #H; napply (oct_destruct … H)
 122  ##]
 123 nqed.