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 bitrigesim : Type ≝
68 [ t00 ⇒ match t2 with [ t00 ⇒ true | _ ⇒ false ] | t01 ⇒ match t2 with [ t01 ⇒ true | _ ⇒ false ]
69 | t02 ⇒ match t2 with [ t02 ⇒ true | _ ⇒ false ] | t03 ⇒ match t2 with [ t03 ⇒ true | _ ⇒ false ]
70 | t04 ⇒ match t2 with [ t04 ⇒ true | _ ⇒ false ] | t05 ⇒ match t2 with [ t05 ⇒ true | _ ⇒ false ]
71 | t06 ⇒ match t2 with [ t06 ⇒ true | _ ⇒ false ] | t07 ⇒ match t2 with [ t07 ⇒ true | _ ⇒ false ]
72 | t08 ⇒ match t2 with [ t08 ⇒ true | _ ⇒ false ] | t09 ⇒ match t2 with [ t09 ⇒ true | _ ⇒ false ]
73 | t0A ⇒ match t2 with [ t0A ⇒ true | _ ⇒ false ] | t0B ⇒ match t2 with [ t0B ⇒ true | _ ⇒ false ]
74 | t0C ⇒ match t2 with [ t0C ⇒ true | _ ⇒ false ] | t0D ⇒ match t2 with [ t0D ⇒ true | _ ⇒ false ]
75 | t0E ⇒ match t2 with [ t0E ⇒ true | _ ⇒ false ] | t0F ⇒ match t2 with [ t0F ⇒ true | _ ⇒ false ]
76 | t10 ⇒ match t2 with [ t10 ⇒ true | _ ⇒ false ] | t11 ⇒ match t2 with [ t11 ⇒ true | _ ⇒ false ]
77 | t12 ⇒ match t2 with [ t12 ⇒ true | _ ⇒ false ] | t13 ⇒ match t2 with [ t13 ⇒ true | _ ⇒ false ]
78 | t14 ⇒ match t2 with [ t14 ⇒ true | _ ⇒ false ] | t15 ⇒ match t2 with [ t15 ⇒ true | _ ⇒ false ]
79 | t16 ⇒ match t2 with [ t16 ⇒ true | _ ⇒ false ] | t17 ⇒ match t2 with [ t17 ⇒ true | _ ⇒ false ]
80 | t18 ⇒ match t2 with [ t18 ⇒ true | _ ⇒ false ] | t19 ⇒ match t2 with [ t19 ⇒ true | _ ⇒ false ]
81 | t1A ⇒ match t2 with [ t1A ⇒ true | _ ⇒ false ] | t1B ⇒ match t2 with [ t1B ⇒ true | _ ⇒ false ]
82 | t1C ⇒ match t2 with [ t1C ⇒ true | _ ⇒ false ] | t1D ⇒ match t2 with [ t1D ⇒ true | _ ⇒ false ]
83 | t1E ⇒ match t2 with [ t1E ⇒ true | _ ⇒ false ] | t1F ⇒ match t2 with [ t1F ⇒ true | _ ⇒ false ]
86 (* iteratore sui bitrigesimali *)
87 ndefinition forall_bit ≝ λP.
88 P t00 ⊗ P t01 ⊗ P t02 ⊗ P t03 ⊗ P t04 ⊗ P t05 ⊗ P t06 ⊗ P t07 ⊗
89 P t08 ⊗ P t09 ⊗ P t0A ⊗ P t0B ⊗ P t0C ⊗ P t0D ⊗ P t0E ⊗ P t0F ⊗
90 P t10 ⊗ P t11 ⊗ P t12 ⊗ P t13 ⊗ P t14 ⊗ P t15 ⊗ P t16 ⊗ P t17 ⊗
91 P t18 ⊗ P t19 ⊗ P t1A ⊗ P t1B ⊗ P t1C ⊗ P t1D ⊗ P t1E ⊗ P t1F.
93 (* operatore successore *)
94 ndefinition succ_bit ≝
96 [ t00 ⇒ t01 | t01 ⇒ t02 | t02 ⇒ t03 | t03 ⇒ t04 | t04 ⇒ t05 | t05 ⇒ t06 | t06 ⇒ t07 | t07 ⇒ t08
97 | t08 ⇒ t09 | t09 ⇒ t0A | t0A ⇒ t0B | t0B ⇒ t0C | t0C ⇒ t0D | t0D ⇒ t0E | t0E ⇒ t0F | t0F ⇒ t10
98 | t10 ⇒ t11 | t11 ⇒ t12 | t12 ⇒ t13 | t13 ⇒ t14 | t14 ⇒ t15 | t15 ⇒ t16 | t16 ⇒ t17 | t17 ⇒ t18
99 | t18 ⇒ t19 | t19 ⇒ t1A | t1A ⇒ t1B | t1B ⇒ t1C | t1C ⇒ t1D | t1D ⇒ t1E | t1E ⇒ t1F | t1F ⇒ t00
102 (* bitrigesimali ricorsivi *)
103 ninductive rec_bitrigesim : bitrigesim → Type ≝
104 bi_O : rec_bitrigesim t00
105 | bi_S : ∀n.rec_bitrigesim n → rec_bitrigesim (succ_bit n).
107 (* bitrigesimali → bitrigesimali ricorsivi *)
108 ndefinition bit_to_recbit ≝
109 λn.match n return λx.rec_bitrigesim x with
112 | t02 ⇒ bi_S ? (bi_S ? bi_O)
113 | t03 ⇒ bi_S ? (bi_S ? (bi_S ? bi_O))
114 | t04 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))
115 | t05 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))
116 | t06 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))
117 | t07 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))
118 | t08 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
120 | t09 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
122 | t0A ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
123 (bi_S ? (bi_S ? bi_O)))))))))
124 | t0B ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
125 (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))
126 | t0C ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
127 (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))
128 | t0D ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
129 (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))
130 | t0E ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
131 (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))))
132 | t0F ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
133 (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))
134 | t10 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
135 (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
137 | t11 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
138 (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
139 (bi_S ? bi_O))))))))))))))))
140 | t12 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
141 (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
142 (bi_S ? (bi_S ? bi_O)))))))))))))))))
143 | t13 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
144 (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
145 (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))
146 | t14 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
147 (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
148 (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))))))))))
149 | t15 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
150 (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
151 (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))))
152 | t16 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
153 (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
154 (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))))))))))))
155 | t17 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
156 (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
157 (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))))))
158 | t18 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
159 (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
160 (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
161 bi_O)))))))))))))))))))))))
162 | t19 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
163 (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
164 (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
165 (bi_S ? bi_O))))))))))))))))))))))))
166 | t1A ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
167 (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
168 (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
169 (bi_S ? (bi_S ? bi_O)))))))))))))))))))))))))
170 | t1B ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
171 (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
172 (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
173 (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))))))))))
174 | t1C ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
175 (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
176 (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
177 (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))))))))))))))))))
178 | t1D ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
179 (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
180 (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
181 (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))))))))))))
182 | t1E ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
183 (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
184 (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
185 (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))))))))))))))))))))
186 | t1F ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
187 (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
188 (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ?
189 (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))))))))))))))
192 ndefinition bitrigesim_destruct_aux ≝
193 Πt1,t2:bitrigesim.ΠP:Prop.t1 = t2 →
194 match eq_bit t1 t2 with [ true ⇒ P → P | false ⇒ P ].
196 ndefinition bitrigesim_destruct : bitrigesim_destruct_aux.
204 nlemma eq_to_eqbit : ∀n1,n2.n1 = n2 → eq_bit n1 n2 = true.
212 nlemma neqbit_to_neq : ∀n1,n2.eq_bit n1 n2 = false → n1 ≠ n2.
214 napply (not_to_not (n1 = n2) (eq_bit n1 n2 = true) …);
215 ##[ ##1: napply (eq_to_eqbit n1 n2)
216 ##| ##2: napply (eqfalse_to_neqtrue … H)
220 (* !!! per brevita... *)
221 naxiom eqbit_to_eq : ∀t1,t2.eq_bit t1 t2 = true → t1 = t2.
223 nlemma neq_to_neqbit : ∀n1,n2.n1 ≠ n2 → eq_bit n1 n2 = false.
225 napply (neqtrue_to_eqfalse (eq_bit n1 n2));
226 napply (not_to_not (eq_bit n1 n2 = true) (n1 = n2) ? H);
227 napply (eqbit_to_eq n1 n2).
230 nlemma decidable_bit : ∀x,y:bitrigesim.decidable (x = y).
232 napply (or2_elim (eq_bit x y = true) (eq_bit x y = false) ? (decidable_bexpr ?));
233 ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqbit_to_eq … H))
234 ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqbit_to_neq … H))
238 nlemma symmetric_eqbit : symmetricT bitrigesim bool eq_bit.
240 napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_bit n1 n2));
241 ##[ ##1: #H; nrewrite > H; napply refl_eq
242 ##| ##2: #H; nrewrite > (neq_to_neqbit n1 n2 H);
243 napply (symmetric_eq ? (eq_bit n2 n1) false);
244 napply (neq_to_neqbit n2 n1 (symmetric_neq ? n1 n2 H))
248 nlemma bitrigesim_is_comparable : comparable.
251 ##| napply forall_bit
253 ##| napply eqbit_to_eq
254 ##| napply eq_to_eqbit
255 ##| napply neqbit_to_neq
256 ##| napply neq_to_neqbit
257 ##| napply decidable_bit
258 ##| napply symmetric_eqbit
262 unification hint 0 ≔ ⊢ carr bitrigesim_is_comparable ≡ bitrigesim.