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 "num/bool_lemmas.ma".
30 ninductive oct : Type ≝
40 (* iteratore sugli ottali *)
41 ndefinition forall_oct ≝ λP.
42 P o0 ⊗ P o1 ⊗ P o2 ⊗ P o3 ⊗ P o4 ⊗ P o5 ⊗ P o6 ⊗ P o7.
48 [ o0 ⇒ match n2 with [ o0 ⇒ true | _ ⇒ false ]
49 | o1 ⇒ match n2 with [ o1 ⇒ true | _ ⇒ false ]
50 | o2 ⇒ match n2 with [ o2 ⇒ true | _ ⇒ false ]
51 | o3 ⇒ match n2 with [ o3 ⇒ true | _ ⇒ false ]
52 | o4 ⇒ match n2 with [ o4 ⇒ true | _ ⇒ false ]
53 | o5 ⇒ match n2 with [ o5 ⇒ true | _ ⇒ false ]
54 | o6 ⇒ match n2 with [ o6 ⇒ true | _ ⇒ false ]
55 | o7 ⇒ match n2 with [ o7 ⇒ true | _ ⇒ false ]
60 λe1,e2:oct.match e1 with
62 [ o0 ⇒ o0 | o1 ⇒ o0 | o2 ⇒ o0 | o3 ⇒ o0
63 | o4 ⇒ o0 | o5 ⇒ o0 | o6 ⇒ o0 | o7 ⇒ o0 ]
65 [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o0 | o3 ⇒ o1
66 | o4 ⇒ o0 | o5 ⇒ o1 | o6 ⇒ o0 | o7 ⇒ o1 ]
68 [ o0 ⇒ o0 | o1 ⇒ o0 | o2 ⇒ o2 | o3 ⇒ o2
69 | o4 ⇒ o0 | o5 ⇒ o0 | o6 ⇒ o2 | o7 ⇒ o2 ]
71 [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o2 | o3 ⇒ o3
72 | o4 ⇒ o0 | o5 ⇒ o1 | o6 ⇒ o2 | o7 ⇒ o3 ]
74 [ o0 ⇒ o0 | o1 ⇒ o0 | o2 ⇒ o0 | o3 ⇒ o0
75 | o4 ⇒ o4 | o5 ⇒ o4 | o6 ⇒ o4 | o7 ⇒ o4 ]
77 [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o0 | o3 ⇒ o1
78 | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o4 | o7 ⇒ o5 ]
80 [ o0 ⇒ o0 | o1 ⇒ o0 | o2 ⇒ o2 | o3 ⇒ o2
81 | o4 ⇒ o4 | o5 ⇒ o4 | o6 ⇒ o6 | o7 ⇒ o6 ]
83 [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o2 | o3 ⇒ o3
84 | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o6 | o7 ⇒ o7 ]
89 λe1,e2:oct.match e1 with
91 [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o2 | o3 ⇒ o3
92 | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o6 | o7 ⇒ o7 ]
94 [ o0 ⇒ o1 | o1 ⇒ o1 | o2 ⇒ o3 | o3 ⇒ o3
95 | o4 ⇒ o5 | o5 ⇒ o5 | o6 ⇒ o7 | o7 ⇒ o7 ]
97 [ o0 ⇒ o2 | o1 ⇒ o3 | o2 ⇒ o2 | o3 ⇒ o3
98 | o4 ⇒ o6 | o5 ⇒ o7 | o6 ⇒ o6 | o7 ⇒ o7 ]
100 [ o0 ⇒ o3 | o1 ⇒ o3 | o2 ⇒ o3 | o3 ⇒ o3
101 | o4 ⇒ o7 | o5 ⇒ o7 | o6 ⇒ o7 | o7 ⇒ o7 ]
103 [ o0 ⇒ o4 | o1 ⇒ o5 | o2 ⇒ o6 | o3 ⇒ o7
104 | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o6 | o7 ⇒ o7 ]
106 [ o0 ⇒ o5 | o1 ⇒ o5 | o2 ⇒ o7 | o3 ⇒ o7
107 | o4 ⇒ o5 | o5 ⇒ o5 | o6 ⇒ o7 | o7 ⇒ o7 ]
109 [ o0 ⇒ o6 | o1 ⇒ o7 | o2 ⇒ o6 | o3 ⇒ o7
110 | o4 ⇒ o6 | o5 ⇒ o7 | o6 ⇒ o6 | o7 ⇒ o7 ]
112 [ o0 ⇒ o7 | o1 ⇒ o7 | o2 ⇒ o7 | o3 ⇒ o7
113 | o4 ⇒ o7 | o5 ⇒ o7 | o6 ⇒ o7 | o7 ⇒ o7 ]
117 ndefinition xor_oct ≝
118 λe1,e2:oct.match e1 with
120 [ o0 ⇒ o0 | o1 ⇒ o1 | o2 ⇒ o2 | o3 ⇒ o3
121 | o4 ⇒ o4 | o5 ⇒ o5 | o6 ⇒ o6 | o7 ⇒ o7 ]
123 [ o0 ⇒ o1 | o1 ⇒ o0 | o2 ⇒ o3 | o3 ⇒ o2
124 | o4 ⇒ o5 | o5 ⇒ o4 | o6 ⇒ o7 | o7 ⇒ o6 ]
126 [ o0 ⇒ o2 | o1 ⇒ o3 | o2 ⇒ o0 | o3 ⇒ o1
127 | o4 ⇒ o6 | o5 ⇒ o7 | o6 ⇒ o4 | o7 ⇒ o5 ]
129 [ o0 ⇒ o3 | o1 ⇒ o2 | o2 ⇒ o1 | o3 ⇒ o0
130 | o4 ⇒ o7 | o5 ⇒ o6 | o6 ⇒ o5 | o7 ⇒ o4 ]
132 [ o0 ⇒ o4 | o1 ⇒ o5 | o2 ⇒ o6 | o3 ⇒ o7
133 | o4 ⇒ o0 | o5 ⇒ o1 | o6 ⇒ o2 | o7 ⇒ o3 ]
135 [ o0 ⇒ o5 | o1 ⇒ o4 | o2 ⇒ o7 | o3 ⇒ o6
136 | o4 ⇒ o1 | o5 ⇒ o0 | o6 ⇒ o3 | o7 ⇒ o2 ]
138 [ o0 ⇒ o6 | o1 ⇒ o7 | o2 ⇒ o4 | o3 ⇒ o5
139 | o4 ⇒ o2 | o5 ⇒ o3 | o6 ⇒ o0 | o7 ⇒ o1 ]
141 [ o0 ⇒ o7 | o1 ⇒ o6 | o2 ⇒ o5 | o3 ⇒ o4
142 | o4 ⇒ o3 | o5 ⇒ o2 | o6 ⇒ o1 | o7 ⇒ o0 ]
145 (* operatore predecessore *)
146 ndefinition pred_oct ≝
148 [ o0 ⇒ o7 | o1 ⇒ o0 | o2 ⇒ o1 | o3 ⇒ o2 | o4 ⇒ o3 | o5 ⇒ o4 | o6 ⇒ o5 | o7 ⇒ o6 ].
150 (* operatore successore *)
151 ndefinition succ_oct ≝
153 [ o0 ⇒ o1 | o1 ⇒ o2 | o2 ⇒ o3 | o3 ⇒ o4 | o4 ⇒ o5 | o5 ⇒ o6 | o6 ⇒ o7 | o7 ⇒ o0 ].
155 (* ottali ricorsivi *)
156 ninductive rec_oct : oct → Type ≝
158 | oc_S : ∀n.rec_oct n → rec_oct (succ_oct n).
160 (* ottali → ottali ricorsivi *)
161 ndefinition oct_to_recoct ≝
162 λn.match n return λx.rec_oct x with
165 | o2 ⇒ oc_S ? (oc_S ? oc_O)
166 | o3 ⇒ oc_S ? (oc_S ? (oc_S ? oc_O))
167 | o4 ⇒ oc_S ? (oc_S ? (oc_S ? (oc_S ? oc_O)))
168 | o5 ⇒ oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? oc_O))))
169 | o6 ⇒ oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? oc_O)))))
170 | o7 ⇒ oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? (oc_S ? oc_O))))))
173 ndefinition oct_destruct_aux ≝
174 Πn1,n2:oct.ΠP:Prop.n1 = n2 →
175 match eq_oct n1 n2 with [ true ⇒ P → P | false ⇒ P ].
177 ndefinition oct_destruct : oct_destruct_aux.
185 nlemma eq_to_eqoct : ∀n1,n2.n1 = n2 → eq_oct n1 n2 = true.
193 nlemma neqoct_to_neq : ∀n1,n2.eq_oct n1 n2 = false → n1 ≠ n2.
195 napply (not_to_not (n1 = n2) (eq_oct n1 n2 = true) …);
196 ##[ ##1: napply (eq_to_eqoct n1 n2)
197 ##| ##2: napply (eqfalse_to_neqtrue … H)
201 nlemma eqoct_to_eq : ∀n1,n2.eq_oct n1 n2 = true → n1 = n2.
206 ##[ ##1,10,19,28,37,46,55,64: #H; napply refl_eq
207 ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*)
211 nlemma neq_to_neqoct : ∀n1,n2.n1 ≠ n2 → eq_oct n1 n2 = false.
213 napply (neqtrue_to_eqfalse (eq_oct n1 n2));
214 napply (not_to_not (eq_oct n1 n2 = true) (n1 = n2) ? H);
215 napply (eqoct_to_eq n1 n2).
218 nlemma decidable_oct : ∀x,y:oct.decidable (x = y).
220 napply (or2_elim (eq_oct x y = true) (eq_oct x y = false) ? (decidable_bexpr ?));
221 ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqoct_to_eq … H))
222 ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqoct_to_neq … H))
226 nlemma symmetric_eqoct : symmetricT oct bool eq_oct.
228 napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_oct n1 n2));
229 ##[ ##1: #H; nrewrite > H; napply refl_eq
230 ##| ##2: #H; nrewrite > (neq_to_neqoct n1 n2 H);
231 napply (symmetric_eq ? (eq_oct n2 n1) false);
232 napply (neq_to_neqoct n2 n1 (symmetric_neq ? n1 n2 H))
236 nlemma oct_is_comparable : comparable.
239 ##| napply forall_oct
241 ##| napply eqoct_to_eq
242 ##| napply eq_to_eqoct
243 ##| napply neqoct_to_neq
244 ##| napply neq_to_neqoct
245 ##| napply decidable_oct
246 ##| napply symmetric_eqoct
250 unification hint 0 ≔ ⊢ carr oct_is_comparable ≡ oct.