From b1c174cffd3c1d10383a52d63a6e662156fb0bb7 Mon Sep 17 00:00:00 2001 From: Cosimo Oliboni Date: Tue, 4 Aug 2009 16:24:31 +0000 Subject: [PATCH] freescle porting, work in progress --- .../ng_assembly/common/option_lemmas.ma | 33 - .../contribs/ng_assembly/common/theory.ma | 50 - .../matita/contribs/ng_assembly/depends | 8 + .../contribs/ng_assembly/num/bitrigesim.ma | 205 +++++ .../ng_assembly/num/bitrigesim_lemmas.ma | 857 ++++++++++++++++++ .../contribs/ng_assembly/num/bool_lemmas.ma | 27 +- .../matita/contribs/ng_assembly/num/byte8.ma | 363 ++++++++ .../contribs/ng_assembly/num/byte8_lemmas.ma | 288 ++++++ .../ng_assembly/num/exadecim_lemmas.ma | 20 - .../contribs/ng_assembly/num/oct_lemmas.ma | 20 - .../ng_assembly/num/quatern_lemmas.ma | 20 - .../matita/contribs/ng_assembly/num/word16.ma | 495 ++++++++++ .../contribs/ng_assembly/num/word16_lemmas.ma | 327 +++++++ .../matita/contribs/ng_assembly/num/word32.ma | 238 +++++ .../contribs/ng_assembly/num/word32_lemmas.ma | 327 +++++++ 15 files changed, 3117 insertions(+), 161 deletions(-) create mode 100755 helm/software/matita/contribs/ng_assembly/num/bitrigesim.ma create mode 100755 helm/software/matita/contribs/ng_assembly/num/bitrigesim_lemmas.ma create mode 100755 helm/software/matita/contribs/ng_assembly/num/byte8.ma create mode 100755 helm/software/matita/contribs/ng_assembly/num/byte8_lemmas.ma create mode 100755 helm/software/matita/contribs/ng_assembly/num/word16.ma create mode 100755 helm/software/matita/contribs/ng_assembly/num/word16_lemmas.ma create mode 100755 helm/software/matita/contribs/ng_assembly/num/word32.ma create mode 100755 helm/software/matita/contribs/ng_assembly/num/word32_lemmas.ma diff --git a/helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma index c157bfa11..34d63c601 100644 --- a/helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma @@ -99,36 +99,3 @@ nlemma eqoption_to_eq : napply refl_eq ##] nqed. - -nlemma neq_to_neqoption : -∀T.∀op1,op2:option T.∀f:T → T → bool. - (∀x1,x2:T.x1 ≠ x2 → f x1 x2 = false) → - (op1 ≠ op2 → eq_option T op1 op2 f = false). - #T; #op1; #op2; #f; #H; - nelim op1; - nelim op2; - nnormalize; - ##[ ##1: #H1; napply False_ind; napply (H1 (refl_eq …)) - ##| ##2,3: #a; #H1; napply refl_eq - ##| ##4: #a; #a0; #H1; - napply H; - napply (neqf_to_neq … a0 a (λx.Some ? x) H1) - ##] -nqed. - -nlemma neqoption_to_neq : -∀T.∀op1,op2:option T.∀f:T → T → bool. - (∀x1,x2:T.f x1 x2 = false → x1 ≠ x2) → - (eq_option T op1 op2 f = false → op1 ≠ op2). - #T; #op1; #op2; #f; #H; - nelim op1; - nelim op2; - nnormalize; - ##[ ##1: #H1; napply (bool_destruct … H1) - ##| ##2: #a; #H1; #H2; napply (option_destruct_none_some ? a H2) - ##| ##3: #a; #H1; #H2; napply (option_destruct_some_none ? a H2) - ##| ##4: #a; #a0; #H1; #H2; - napply (H a0 a H1); - napply (option_destruct_some_some ? a0 a H2) - ##] -nqed. diff --git a/helm/software/matita/contribs/ng_assembly/common/theory.ma b/helm/software/matita/contribs/ng_assembly/common/theory.ma index 0cdc02a4c..2bf08ce48 100644 --- a/helm/software/matita/contribs/ng_assembly/common/theory.ma +++ b/helm/software/matita/contribs/ng_assembly/common/theory.ma @@ -57,15 +57,6 @@ nlemma prop_to_nnprop : ∀P.P → ¬¬P. napply (H1 H). nqed. -(* -naxiom RAA : ∀P:Prop.∀f:(¬P) → False.P. - -nlemma nnprop_to_prop : ∀P.(¬¬P) → P. - #P; nchange with (((¬P) → False) → P); - #H; napply (RAA P H). -nqed. -*) - ninductive And (A,B:Prop) : Prop ≝ conj : A → B → (And A B). @@ -94,32 +85,6 @@ interpretation "logical or" 'or x y = (Or x y). ndefinition decidable : Prop → Prop ≝ λA:Prop.A ∨ ¬A. -(* -nlemma decidable_prop : ∀P:Prop.decidable P. - #P; nnormalize; - napply RAA; - #H; - napply (absurd (P ∨ (¬P)) …); - ##[ ##2: napply H - ##| ##1: napply (or_intror P (¬P)); - napply RAA; - #H1; - napply (absurd (P ∨ (¬P)) …); - ##[ ##2: napply H - ##| ##1: napply (or_introl P (¬P)); - napply (nnprop_to_prop P H1) - ##] - ##] -nqed. - -nlemma terzo_escluso : ∀P,G:Prop.∀ft:P → G.∀ff:(¬P) → G.G. - #P; #G; nnormalize; - #H; #H1; - napply (Or_ind P (P → False) ? H H1 ?); - napply (decidable_prop P). -nqed. -*) - nlemma or_elim : ∀P,Q,G:Prop.Or P Q → ∀fp:P → G.∀fq:Q → G.G. #P; #Q; #G; #H; #H1; #H2; napply (Or_ind P Q ? H1 H2 ?); @@ -191,21 +156,6 @@ nlemma neqf_to_neq : ∀T1,T2:Type.∀x,y:T1.∀f:T1 → T2.((f x) ≠ (f y)) napply (H (eq_f … H1)). nqed. -(* -nlemma neqf2_to_neq : ∀T1,T2,T3:Type.∀x1,y1:T1.∀x2,y2:T2.∀f:T1 → T2 → T3.f x1 x2 ≠ f y1 y2 → (x1 ≠ y1) ∨ (x2 ≠ y2). - #T1; #T2; #T3; #x1; #y1; #x2; #y2; #f; nnormalize; #H; - napply (terzo_escluso (x1 = y1) …); - ##[ ##2: #H1; napply (or_introl … H1) - ##| ##1: #H1; napply (terzo_escluso (x2 = y2) …) - ##[ ##2: #H2; napply (or_intror … H2) - ##| ##1: #H2; nrewrite < H1 in H:(%); - nrewrite < H2; #H; - nelim (H (refl_eq …)) - ##] - ##] -nqed. -*) - nlemma symmetric_eq: ∀A:Type. symmetric A (eq A). #A; nnormalize; diff --git a/helm/software/matita/contribs/ng_assembly/depends b/helm/software/matita/contribs/ng_assembly/depends index 8e0fddce2..b365c9fe8 100644 --- a/helm/software/matita/contribs/ng_assembly/depends +++ b/helm/software/matita/contribs/ng_assembly/depends @@ -1,14 +1,22 @@ +num/word32.ma num/word16.ma num/exadecim.ma common/prod.ma num/bool.ma num/oct.ma num/quatern.ma common/option.ma num/bool.ma +num/word16.ma num/byte8.ma +num/byte8_lemmas.ma num/byte8.ma num/exadecim_lemmas.ma +num/word16_lemmas.ma num/byte8_lemmas.ma num/word16.ma test_errori.ma common/theory.ma +num/bitrigesim_lemmas.ma num/bitrigesim.ma num/bool_lemmas.ma num/quatern.ma num/bool.ma common/prod.ma num/bool.ma +num/byte8.ma num/bitrigesim.ma num/exadecim.ma num/bool.ma common/theory.ma num/quatern_lemmas.ma num/bool_lemmas.ma num/quatern.ma +num/word32_lemmas.ma num/word16_lemmas.ma num/word32.ma common/option_lemmas.ma common/option.ma num/bool_lemmas.ma common/prod_lemmas.ma common/prod.ma num/bool_lemmas.ma num/oct_lemmas.ma num/bool_lemmas.ma num/oct.ma +num/bitrigesim.ma num/bool.ma num/bool_lemmas.ma num/bool.ma num/exadecim_lemmas.ma num/bool_lemmas.ma num/exadecim.ma num/oct.ma num/bool.ma diff --git a/helm/software/matita/contribs/ng_assembly/num/bitrigesim.ma b/helm/software/matita/contribs/ng_assembly/num/bitrigesim.ma new file mode 100755 index 000000000..943d2cb84 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/num/bitrigesim.ma @@ -0,0 +1,205 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* ********************************************************************** *) + +include "num/bool.ma". + +(* ************* *) +(* BITRIGESIMALI *) +(* ************* *) + +ninductive bitrigesim : Type ≝ + t00: bitrigesim +| t01: bitrigesim +| t02: bitrigesim +| t03: bitrigesim +| t04: bitrigesim +| t05: bitrigesim +| t06: bitrigesim +| t07: bitrigesim +| t08: bitrigesim +| t09: bitrigesim +| t0A: bitrigesim +| t0B: bitrigesim +| t0C: bitrigesim +| t0D: bitrigesim +| t0E: bitrigesim +| t0F: bitrigesim +| t10: bitrigesim +| t11: bitrigesim +| t12: bitrigesim +| t13: bitrigesim +| t14: bitrigesim +| t15: bitrigesim +| t16: bitrigesim +| t17: bitrigesim +| t18: bitrigesim +| t19: bitrigesim +| t1A: bitrigesim +| t1B: bitrigesim +| t1C: bitrigesim +| t1D: bitrigesim +| t1E: bitrigesim +| t1F: bitrigesim. + +(* operatore = *) +ndefinition eq_bit ≝ +λt1,t2:bitrigesim. + match t1 with + [ t00 ⇒ match t2 with [ t00 ⇒ true | _ ⇒ false ] + | t01 ⇒ match t2 with [ t01 ⇒ true | _ ⇒ false ] + | t02 ⇒ match t2 with [ t02 ⇒ true | _ ⇒ false ] + | t03 ⇒ match t2 with [ t03 ⇒ true | _ ⇒ false ] + | t04 ⇒ match t2 with [ t04 ⇒ true | _ ⇒ false ] + | t05 ⇒ match t2 with [ t05 ⇒ true | _ ⇒ false ] + | t06 ⇒ match t2 with [ t06 ⇒ true | _ ⇒ false ] + | t07 ⇒ match t2 with [ t07 ⇒ true | _ ⇒ false ] + | t08 ⇒ match t2 with [ t08 ⇒ true | _ ⇒ false ] + | t09 ⇒ match t2 with [ t09 ⇒ true | _ ⇒ false ] + | t0A ⇒ match t2 with [ t0A ⇒ true | _ ⇒ false ] + | t0B ⇒ match t2 with [ t0B ⇒ true | _ ⇒ false ] + | t0C ⇒ match t2 with [ t0C ⇒ true | _ ⇒ false ] + | t0D ⇒ match t2 with [ t0D ⇒ true | _ ⇒ false ] + | t0E ⇒ match t2 with [ t0E ⇒ true | _ ⇒ false ] + | t0F ⇒ match t2 with [ t0F ⇒ true | _ ⇒ false ] + | t10 ⇒ match t2 with [ t10 ⇒ true | _ ⇒ false ] + | t11 ⇒ match t2 with [ t11 ⇒ true | _ ⇒ false ] + | t12 ⇒ match t2 with [ t12 ⇒ true | _ ⇒ false ] + | t13 ⇒ match t2 with [ t13 ⇒ true | _ ⇒ false ] + | t14 ⇒ match t2 with [ t14 ⇒ true | _ ⇒ false ] + | t15 ⇒ match t2 with [ t15 ⇒ true | _ ⇒ false ] + | t16 ⇒ match t2 with [ t16 ⇒ true | _ ⇒ false ] + | t17 ⇒ match t2 with [ t17 ⇒ true | _ ⇒ false ] + | t18 ⇒ match t2 with [ t18 ⇒ true | _ ⇒ false ] + | t19 ⇒ match t2 with [ t19 ⇒ true | _ ⇒ false ] + | t1A ⇒ match t2 with [ t1A ⇒ true | _ ⇒ false ] + | t1B ⇒ match t2 with [ t1B ⇒ true | _ ⇒ false ] + | t1C ⇒ match t2 with [ t1C ⇒ true | _ ⇒ false ] + | t1D ⇒ match t2 with [ t1D ⇒ true | _ ⇒ false ] + | t1E ⇒ match t2 with [ t1E ⇒ true | _ ⇒ false ] + | t1F ⇒ match t2 with [ t1F ⇒ true | _ ⇒ false ] + ]. + +(* iteratore sui bitrigesimali *) +ndefinition forall_bit ≝ λP. + P t00 ⊗ P t01 ⊗ P t02 ⊗ P t03 ⊗ P t04 ⊗ P t05 ⊗ P t06 ⊗ P t07 ⊗ + P t08 ⊗ P t09 ⊗ P t0A ⊗ P t0B ⊗ P t0C ⊗ P t0D ⊗ P t0E ⊗ P t0F ⊗ + P t10 ⊗ P t11 ⊗ P t12 ⊗ P t13 ⊗ P t14 ⊗ P t15 ⊗ P t16 ⊗ P t17 ⊗ + P t18 ⊗ P t19 ⊗ P t1A ⊗ P t1B ⊗ P t1C ⊗ P t1D ⊗ P t1E ⊗ P t1F. + +(* operatore successore *) +ndefinition succ_bit ≝ +λn.match n with + [ t00 ⇒ t01 | t01 ⇒ t02 | t02 ⇒ t03 | t03 ⇒ t04 | t04 ⇒ t05 | t05 ⇒ t06 | t06 ⇒ t07 | t07 ⇒ t08 + | t08 ⇒ t09 | t09 ⇒ t0A | t0A ⇒ t0B | t0B ⇒ t0C | t0C ⇒ t0D | t0D ⇒ t0E | t0E ⇒ t0F | t0F ⇒ t10 + | t10 ⇒ t11 | t11 ⇒ t12 | t12 ⇒ t13 | t13 ⇒ t14 | t14 ⇒ t15 | t15 ⇒ t16 | t16 ⇒ t17 | t17 ⇒ t18 + | t18 ⇒ t19 | t19 ⇒ t1A | t1A ⇒ t1B | t1B ⇒ t1C | t1C ⇒ t1D | t1D ⇒ t1E | t1E ⇒ t1F | t1F ⇒ t00 + ]. + +(* bitrigesimali ricorsivi *) +ninductive rec_bitrigesim : bitrigesim → Type ≝ + bi_O : rec_bitrigesim t00 +| bi_S : ∀n.rec_bitrigesim n → rec_bitrigesim (succ_bit n). + +(* bitrigesimali → bitrigesimali ricorsivi *) +ndefinition bit_to_recbit ≝ +λn.match n return λx.rec_bitrigesim x with + [ t00 ⇒ bi_O + | t01 ⇒ bi_S ? bi_O + | t02 ⇒ bi_S ? (bi_S ? bi_O) + | t03 ⇒ bi_S ? (bi_S ? (bi_S ? bi_O)) + | t04 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))) + | t05 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))) + | t06 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))) + | t07 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))) + | t08 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + bi_O))))))) + | t09 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? bi_O)))))))) + | t0A ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? bi_O))))))))) + | t0B ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))) + | t0C ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))) + | t0D ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))) + | t0E ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))) + | t0F ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))))) + | t10 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + bi_O))))))))))))))) + | t11 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? bi_O)))))))))))))))) + | t12 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? bi_O))))))))))))))))) + | t13 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))))))))) + | t14 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))) + | t15 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))))))))))) + | t16 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))))) + | t17 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))))))))))))) + | t18 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + bi_O))))))))))))))))))))))) + | t19 ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? bi_O)))))))))))))))))))))))) + | t1A ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? bi_O))))))))))))))))))))))))) + | t1B ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))))))))))))))))) + | t1C ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))))))))))) + | t1D ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))))))))))))))))))) + | t1E ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O))))))))))))))))))))))))))))) + | t1F ⇒ bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? + (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? (bi_S ? bi_O)))))))))))))))))))))))))))))) + ]. diff --git a/helm/software/matita/contribs/ng_assembly/num/bitrigesim_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/bitrigesim_lemmas.ma new file mode 100755 index 000000000..675f14fb3 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/num/bitrigesim_lemmas.ma @@ -0,0 +1,857 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* ********************************************************************** *) + +include "num/bitrigesim.ma". +include "num/bool_lemmas.ma". + +(* ************* *) +(* BITRIGESIMALI *) +(* ************* *) + +ndefinition bitrigesim_destruct1 : +Πt2:bitrigesim.ΠP:Prop.t00 = t2 → match t2 with [ t00 ⇒ P → P | _ ⇒ P ]. + #t2; #P; + ncases t2; + nnormalize; #H; + ##[ ##1: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match t00 with [ t00 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition bitrigesim_destruct2 : +Πt2:bitrigesim.ΠP:Prop.t01 = t2 → match t2 with [ t01 ⇒ P → P | _ ⇒ P ]. + #t2; #P; + ncases t2; + nnormalize; #H; + ##[ ##2: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match t01 with [ t01 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition bitrigesim_destruct3 : +Πt2:bitrigesim.ΠP:Prop.t02 = t2 → match t2 with [ t02 ⇒ P → P | _ ⇒ P ]. + #t2; #P; + ncases t2; + nnormalize; #H; + ##[ ##3: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match t02 with [ t02 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition bitrigesim_destruct4 : +Πt2:bitrigesim.ΠP:Prop.t03 = t2 → match t2 with [ t03 ⇒ P → P | _ ⇒ P ]. + #t2; #P; + ncases t2; + nnormalize; #H; + ##[ ##4: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match t03 with [ t03 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition bitrigesim_destruct5 : +Πt2:bitrigesim.ΠP:Prop.t04 = t2 → match t2 with [ t04 ⇒ P → P | _ ⇒ P ]. + #t2; #P; + ncases t2; + nnormalize; #H; + ##[ ##5: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match t04 with [ t04 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition bitrigesim_destruct6 : +Πt2:bitrigesim.ΠP:Prop.t05 = t2 → match t2 with [ t05 ⇒ P → P | _ ⇒ P ]. + #t2; #P; + ncases t2; + nnormalize; #H; + ##[ ##6: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match t05 with [ t05 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition bitrigesim_destruct7 : +Πt2:bitrigesim.ΠP:Prop.t06 = t2 → match t2 with [ t06 ⇒ P → P | _ ⇒ P ]. + #t2; #P; + ncases t2; + nnormalize; #H; + ##[ ##7: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match t06 with [ t06 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition bitrigesim_destruct8 : +Πt2:bitrigesim.ΠP:Prop.t07 = t2 → match t2 with [ t07 ⇒ P → P | _ ⇒ P ]. + #t2; #P; + ncases t2; + nnormalize; #H; + ##[ ##8: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match t07 with [ t07 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition bitrigesim_destruct9 : +Πt2:bitrigesim.ΠP:Prop.t08 = t2 → match t2 with [ t08 ⇒ P → P | _ ⇒ P ]. + #t2; #P; + ncases t2; + nnormalize; #H; + ##[ ##9: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match t08 with [ t08 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition bitrigesim_destruct10 : +Πt2:bitrigesim.ΠP:Prop.t09 = t2 → match t2 with [ t09 ⇒ P → P | _ ⇒ P ]. + #t2; #P; + ncases t2; + nnormalize; #H; + ##[ ##10: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match t09 with [ t09 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition bitrigesim_destruct11 : +Πt2:bitrigesim.ΠP:Prop.t0A = t2 → match t2 with [ t0A ⇒ P → P | _ ⇒ P ]. + #t2; #P; + ncases t2; + nnormalize; #H; + ##[ ##11: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match t0A with [ t0A ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition bitrigesim_destruct12 : +Πt2:bitrigesim.ΠP:Prop.t0B = t2 → match t2 with [ t0B ⇒ P → P | _ ⇒ P ]. + #t2; #P; + ncases t2; + nnormalize; #H; + ##[ ##12: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match t0B with [ t0B ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition bitrigesim_destruct13 : +Πt2:bitrigesim.ΠP:Prop.t0C = t2 → match t2 with [ t0C ⇒ P → P | _ ⇒ P ]. + #t2; #P; + ncases t2; + nnormalize; #H; + ##[ ##13: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match t0C with [ t0C ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition bitrigesim_destruct14 : +Πt2:bitrigesim.ΠP:Prop.t0D = t2 → match t2 with [ t0D ⇒ P → P | _ ⇒ P ]. + #t2; #P; + ncases t2; + nnormalize; #H; + ##[ ##14: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match t0D with [ t0D ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition bitrigesim_destruct15 : +Πt2:bitrigesim.ΠP:Prop.t0E = t2 → match t2 with [ t0E ⇒ P → P | _ ⇒ P ]. + #t2; #P; + ncases t2; + nnormalize; #H; + ##[ ##15: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match t0E with [ t0E ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition bitrigesim_destruct16 : +Πt2:bitrigesim.ΠP:Prop.t0F = t2 → match t2 with [ t0F ⇒ P → P | _ ⇒ P ]. + #t2; #P; + ncases t2; + nnormalize; #H; + ##[ ##16: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match t0F with [ t0F ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition bitrigesim_destruct17 : +Πt2:bitrigesim.ΠP:Prop.t10 = t2 → match t2 with [ t10 ⇒ P → P | _ ⇒ P ]. + #t2; #P; + ncases t2; + nnormalize; #H; + ##[ ##17: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match t10 with [ t10 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition bitrigesim_destruct18 : +Πt2:bitrigesim.ΠP:Prop.t11 = t2 → match t2 with [ t11 ⇒ P → P | _ ⇒ P ]. + #t2; #P; + ncases t2; + nnormalize; #H; + ##[ ##18: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match t11 with [ t11 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition bitrigesim_destruct19 : +Πt2:bitrigesim.ΠP:Prop.t12 = t2 → match t2 with [ t12 ⇒ P → P | _ ⇒ P ]. + #t2; #P; + ncases t2; + nnormalize; #H; + ##[ ##19: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match t12 with [ t12 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition bitrigesim_destruct20 : +Πt2:bitrigesim.ΠP:Prop.t13 = t2 → match t2 with [ t13 ⇒ P → P | _ ⇒ P ]. + #t2; #P; + ncases t2; + nnormalize; #H; + ##[ ##20: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match t13 with [ t13 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition bitrigesim_destruct21 : +Πt2:bitrigesim.ΠP:Prop.t14 = t2 → match t2 with [ t14 ⇒ P → P | _ ⇒ P ]. + #t2; #P; + ncases t2; + nnormalize; #H; + ##[ ##21: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match t14 with [ t14 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition bitrigesim_destruct22 : +Πt2:bitrigesim.ΠP:Prop.t15 = t2 → match t2 with [ t15 ⇒ P → P | _ ⇒ P ]. + #t2; #P; + ncases t2; + nnormalize; #H; + ##[ ##22: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match t15 with [ t15 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition bitrigesim_destruct23 : +Πt2:bitrigesim.ΠP:Prop.t16 = t2 → match t2 with [ t16 ⇒ P → P | _ ⇒ P ]. + #t2; #P; + ncases t2; + nnormalize; #H; + ##[ ##23: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match t16 with [ t16 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition bitrigesim_destruct24 : +Πt2:bitrigesim.ΠP:Prop.t17 = t2 → match t2 with [ t17 ⇒ P → P | _ ⇒ P ]. + #t2; #P; + ncases t2; + nnormalize; #H; + ##[ ##24: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match t17 with [ t17 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition bitrigesim_destruct25 : +Πt2:bitrigesim.ΠP:Prop.t18 = t2 → match t2 with [ t18 ⇒ P → P | _ ⇒ P ]. + #t2; #P; + ncases t2; + nnormalize; #H; + ##[ ##25: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match t18 with [ t18 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition bitrigesim_destruct26 : +Πt2:bitrigesim.ΠP:Prop.t19 = t2 → match t2 with [ t19 ⇒ P → P | _ ⇒ P ]. + #t2; #P; + ncases t2; + nnormalize; #H; + ##[ ##26: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match t19 with [ t19 ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition bitrigesim_destruct27 : +Πt2:bitrigesim.ΠP:Prop.t1A = t2 → match t2 with [ t1A ⇒ P → P | _ ⇒ P ]. + #t2; #P; + ncases t2; + nnormalize; #H; + ##[ ##27: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match t1A with [ t1A ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition bitrigesim_destruct28 : +Πt2:bitrigesim.ΠP:Prop.t1B = t2 → match t2 with [ t1B ⇒ P → P | _ ⇒ P ]. + #t2; #P; + ncases t2; + nnormalize; #H; + ##[ ##28: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match t1B with [ t1B ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition bitrigesim_destruct29 : +Πt2:bitrigesim.ΠP:Prop.t1C = t2 → match t2 with [ t1C ⇒ P → P | _ ⇒ P ]. + #t2; #P; + ncases t2; + nnormalize; #H; + ##[ ##29: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match t1C with [ t1C ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition bitrigesim_destruct30 : +Πt2:bitrigesim.ΠP:Prop.t1D = t2 → match t2 with [ t1D ⇒ P → P | _ ⇒ P ]. + #t2; #P; + ncases t2; + nnormalize; #H; + ##[ ##30: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match t1D with [ t1D ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition bitrigesim_destruct31 : +Πt2:bitrigesim.ΠP:Prop.t1E = t2 → match t2 with [ t1E ⇒ P → P | _ ⇒ P ]. + #t2; #P; + ncases t2; + nnormalize; #H; + ##[ ##31: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match t1E with [ t1E ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition bitrigesim_destruct32 : +Πt2:bitrigesim.ΠP:Prop.t1F = t2 → match t2 with [ t1F ⇒ P → P | _ ⇒ P ]. + #t2; #P; + ncases t2; + nnormalize; #H; + ##[ ##32: napply (λx:P.x) + ##| ##*: napply False_ind; + nchange with (match t1F with [ t1F ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +ndefinition bitrigesim_destruct_aux ≝ +Πt1,t2:bitrigesim.ΠP:Prop.t1 = t2 → + match t1 with + [ t00 ⇒ match t2 with [ t00 ⇒ P → P | _ ⇒ P ] + | t01 ⇒ match t2 with [ t01 ⇒ P → P | _ ⇒ P ] + | t02 ⇒ match t2 with [ t02 ⇒ P → P | _ ⇒ P ] + | t03 ⇒ match t2 with [ t03 ⇒ P → P | _ ⇒ P ] + | t04 ⇒ match t2 with [ t04 ⇒ P → P | _ ⇒ P ] + | t05 ⇒ match t2 with [ t05 ⇒ P → P | _ ⇒ P ] + | t06 ⇒ match t2 with [ t06 ⇒ P → P | _ ⇒ P ] + | t07 ⇒ match t2 with [ t07 ⇒ P → P | _ ⇒ P ] + | t08 ⇒ match t2 with [ t08 ⇒ P → P | _ ⇒ P ] + | t09 ⇒ match t2 with [ t09 ⇒ P → P | _ ⇒ P ] + | t0A ⇒ match t2 with [ t0A ⇒ P → P | _ ⇒ P ] + | t0B ⇒ match t2 with [ t0B ⇒ P → P | _ ⇒ P ] + | t0C ⇒ match t2 with [ t0C ⇒ P → P | _ ⇒ P ] + | t0D ⇒ match t2 with [ t0D ⇒ P → P | _ ⇒ P ] + | t0E ⇒ match t2 with [ t0E ⇒ P → P | _ ⇒ P ] + | t0F ⇒ match t2 with [ t0F ⇒ P → P | _ ⇒ P ] + | t10 ⇒ match t2 with [ t10 ⇒ P → P | _ ⇒ P ] + | t11 ⇒ match t2 with [ t11 ⇒ P → P | _ ⇒ P ] + | t12 ⇒ match t2 with [ t12 ⇒ P → P | _ ⇒ P ] + | t13 ⇒ match t2 with [ t13 ⇒ P → P | _ ⇒ P ] + | t14 ⇒ match t2 with [ t14 ⇒ P → P | _ ⇒ P ] + | t15 ⇒ match t2 with [ t15 ⇒ P → P | _ ⇒ P ] + | t16 ⇒ match t2 with [ t16 ⇒ P → P | _ ⇒ P ] + | t17 ⇒ match t2 with [ t17 ⇒ P → P | _ ⇒ P ] + | t18 ⇒ match t2 with [ t18 ⇒ P → P | _ ⇒ P ] + | t19 ⇒ match t2 with [ t19 ⇒ P → P | _ ⇒ P ] + | t1A ⇒ match t2 with [ t1A ⇒ P → P | _ ⇒ P ] + | t1B ⇒ match t2 with [ t1B ⇒ P → P | _ ⇒ P ] + | t1C ⇒ match t2 with [ t1C ⇒ P → P | _ ⇒ P ] + | t1D ⇒ match t2 with [ t1D ⇒ P → P | _ ⇒ P ] + | t1E ⇒ match t2 with [ t1E ⇒ P → P | _ ⇒ P ] + | t1F ⇒ match t2 with [ t1F ⇒ P → P | _ ⇒ P ] + ]. + +ndefinition bitrigesim_destruct : bitrigesim_destruct_aux. + #t1; + ncases t1; + ##[ ##1: napply bitrigesim_destruct1 + ##| ##2: napply bitrigesim_destruct2 + ##| ##3: napply bitrigesim_destruct3 + ##| ##4: napply bitrigesim_destruct4 + ##| ##5: napply bitrigesim_destruct5 + ##| ##6: napply bitrigesim_destruct6 + ##| ##7: napply bitrigesim_destruct7 + ##| ##8: napply bitrigesim_destruct8 + ##| ##9: napply bitrigesim_destruct9 + ##| ##10: napply bitrigesim_destruct10 + ##| ##11: napply bitrigesim_destruct11 + ##| ##12: napply bitrigesim_destruct12 + ##| ##13: napply bitrigesim_destruct13 + ##| ##14: napply bitrigesim_destruct14 + ##| ##15: napply bitrigesim_destruct15 + ##| ##16: napply bitrigesim_destruct16 + ##| ##17: napply bitrigesim_destruct17 + ##| ##18: napply bitrigesim_destruct18 + ##| ##19: napply bitrigesim_destruct19 + ##| ##20: napply bitrigesim_destruct20 + ##| ##21: napply bitrigesim_destruct21 + ##| ##22: napply bitrigesim_destruct22 + ##| ##23: napply bitrigesim_destruct23 + ##| ##24: napply bitrigesim_destruct24 + ##| ##25: napply bitrigesim_destruct25 + ##| ##26: napply bitrigesim_destruct26 + ##| ##27: napply bitrigesim_destruct27 + ##| ##28: napply bitrigesim_destruct28 + ##| ##29: napply bitrigesim_destruct29 + ##| ##30: napply bitrigesim_destruct30 + ##| ##31: napply bitrigesim_destruct31 + ##| ##32: napply bitrigesim_destruct32 + ##] +nqed. + +nlemma symmetric_eqbit : symmetricT bitrigesim bool eq_bit. + #t1; + nelim t1; + ##[ ##1: #t2; nelim t2; nnormalize; napply refl_eq + ##| ##2: #t2; nelim t2; nnormalize; napply refl_eq + ##| ##3: #t2; nelim t2; nnormalize; napply refl_eq + ##| ##4: #t2; nelim t2; nnormalize; napply refl_eq + ##| ##5: #t2; nelim t2; nnormalize; napply refl_eq + ##| ##6: #t2; nelim t2; nnormalize; napply refl_eq + ##| ##7: #t2; nelim t2; nnormalize; napply refl_eq + ##| ##8: #t2; nelim t2; nnormalize; napply refl_eq + ##| ##9: #t2; nelim t2; nnormalize; napply refl_eq + ##| ##10: #t2; nelim t2; nnormalize; napply refl_eq + ##| ##11: #t2; nelim t2; nnormalize; napply refl_eq + ##| ##12: #t2; nelim t2; nnormalize; napply refl_eq + ##| ##13: #t2; nelim t2; nnormalize; napply refl_eq + ##| ##14: #t2; nelim t2; nnormalize; napply refl_eq + ##| ##15: #t2; nelim t2; nnormalize; napply refl_eq + ##| ##16: #t2; nelim t2; nnormalize; napply refl_eq + ##| ##17: #t2; nelim t2; nnormalize; napply refl_eq + ##| ##18: #t2; nelim t2; nnormalize; napply refl_eq + ##| ##19: #t2; nelim t2; nnormalize; napply refl_eq + ##| ##20: #t2; nelim t2; nnormalize; napply refl_eq + ##| ##21: #t2; nelim t2; nnormalize; napply refl_eq + ##| ##22: #t2; nelim t2; nnormalize; napply refl_eq + ##| ##23: #t2; nelim t2; nnormalize; napply refl_eq + ##| ##24: #t2; nelim t2; nnormalize; napply refl_eq + ##| ##25: #t2; nelim t2; nnormalize; napply refl_eq + ##| ##26: #t2; nelim t2; nnormalize; napply refl_eq + ##| ##27: #t2; nelim t2; nnormalize; napply refl_eq + ##| ##28: #t2; nelim t2; nnormalize; napply refl_eq + ##| ##29: #t2; nelim t2; nnormalize; napply refl_eq + ##| ##30: #t2; nelim t2; nnormalize; napply refl_eq + ##| ##31: #t2; nelim t2; nnormalize; napply refl_eq + ##| ##32: #t2; nelim t2; nnormalize; napply refl_eq + ##] +nqed. + +nlemma eqbit_to_eq1 : ∀t2.eq_bit t00 t2 = true → t00 = t2. + #t2; ncases t2; nnormalize; #H; ##[ ##1: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] +nqed. + +nlemma eqbit_to_eq2 : ∀t2.eq_bit t01 t2 = true → t01 = t2. + #t2; ncases t2; nnormalize; #H; ##[ ##2: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] +nqed. + +nlemma eqbit_to_eq3 : ∀t2.eq_bit t02 t2 = true → t02 = t2. + #t2; ncases t2; nnormalize; #H; ##[ ##3: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] +nqed. + +nlemma eqbit_to_eq4 : ∀t2.eq_bit t03 t2 = true → t03 = t2. + #t2; ncases t2; nnormalize; #H; ##[ ##4: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] +nqed. + +nlemma eqbit_to_eq5 : ∀t2.eq_bit t04 t2 = true → t04 = t2. + #t2; ncases t2; nnormalize; #H; ##[ ##5: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] +nqed. + +nlemma eqbit_to_eq6 : ∀t2.eq_bit t05 t2 = true → t05 = t2. + #t2; ncases t2; nnormalize; #H; ##[ ##6: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] +nqed. + +nlemma eqbit_to_eq7 : ∀t2.eq_bit t06 t2 = true → t06 = t2. + #t2; ncases t2; nnormalize; #H; ##[ ##7: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] +nqed. + +nlemma eqbit_to_eq8 : ∀t2.eq_bit t07 t2 = true → t07 = t2. + #t2; ncases t2; nnormalize; #H; ##[ ##8: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] +nqed. + +nlemma eqbit_to_eq9 : ∀t2.eq_bit t08 t2 = true → t08 = t2. + #t2; ncases t2; nnormalize; #H; ##[ ##9: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] +nqed. + +nlemma eqbit_to_eq10 : ∀t2.eq_bit t09 t2 = true → t09 = t2. + #t2; ncases t2; nnormalize; #H; ##[ ##10: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] +nqed. + +nlemma eqbit_to_eq11 : ∀t2.eq_bit t0A t2 = true → t0A = t2. + #t2; ncases t2; nnormalize; #H; ##[ ##11: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] +nqed. + +nlemma eqbit_to_eq12 : ∀t2.eq_bit t0B t2 = true → t0B = t2. + #t2; ncases t2; nnormalize; #H; ##[ ##12: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] +nqed. + +nlemma eqbit_to_eq13 : ∀t2.eq_bit t0C t2 = true → t0C = t2. + #t2; ncases t2; nnormalize; #H; ##[ ##13: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] +nqed. + +nlemma eqbit_to_eq14 : ∀t2.eq_bit t0D t2 = true → t0D = t2. + #t2; ncases t2; nnormalize; #H; ##[ ##14: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] +nqed. + +nlemma eqbit_to_eq15 : ∀t2.eq_bit t0E t2 = true → t0E = t2. + #t2; ncases t2; nnormalize; #H; ##[ ##15: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] +nqed. + +nlemma eqbit_to_eq16 : ∀t2.eq_bit t0F t2 = true → t0F = t2. + #t2; ncases t2; nnormalize; #H; ##[ ##16: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] +nqed. + +nlemma eqbit_to_eq17 : ∀t2.eq_bit t10 t2 = true → t10 = t2. + #t2; ncases t2; nnormalize; #H; ##[ ##17: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] +nqed. + +nlemma eqbit_to_eq18 : ∀t2.eq_bit t11 t2 = true → t11 = t2. + #t2; ncases t2; nnormalize; #H; ##[ ##18: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] +nqed. + +nlemma eqbit_to_eq19 : ∀t2.eq_bit t12 t2 = true → t12 = t2. + #t2; ncases t2; nnormalize; #H; ##[ ##19: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] +nqed. + +nlemma eqbit_to_eq20 : ∀t2.eq_bit t13 t2 = true → t13 = t2. + #t2; ncases t2; nnormalize; #H; ##[ ##20: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] +nqed. + +nlemma eqbit_to_eq21 : ∀t2.eq_bit t14 t2 = true → t14 = t2. + #t2; ncases t2; nnormalize; #H; ##[ ##21: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] +nqed. + +nlemma eqbit_to_eq22 : ∀t2.eq_bit t15 t2 = true → t15 = t2. + #t2; ncases t2; nnormalize; #H; ##[ ##22: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] +nqed. + +nlemma eqbit_to_eq23 : ∀t2.eq_bit t16 t2 = true → t16 = t2. + #t2; ncases t2; nnormalize; #H; ##[ ##23: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] +nqed. + +nlemma eqbit_to_eq24 : ∀t2.eq_bit t17 t2 = true → t17 = t2. + #t2; ncases t2; nnormalize; #H; ##[ ##24: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] +nqed. + +nlemma eqbit_to_eq25 : ∀t2.eq_bit t18 t2 = true → t18 = t2. + #t2; ncases t2; nnormalize; #H; ##[ ##25: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] +nqed. + +nlemma eqbit_to_eq26 : ∀t2.eq_bit t19 t2 = true → t19 = t2. + #t2; ncases t2; nnormalize; #H; ##[ ##26: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] +nqed. + +nlemma eqbit_to_eq27 : ∀t2.eq_bit t1A t2 = true → t1A = t2. + #t2; ncases t2; nnormalize; #H; ##[ ##27: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] +nqed. + +nlemma eqbit_to_eq28 : ∀t2.eq_bit t1B t2 = true → t1B = t2. + #t2; ncases t2; nnormalize; #H; ##[ ##28: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] +nqed. + +nlemma eqbit_to_eq29 : ∀t2.eq_bit t1C t2 = true → t1C = t2. + #t2; ncases t2; nnormalize; #H; ##[ ##29: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] +nqed. + +nlemma eqbit_to_eq30 : ∀t2.eq_bit t1D t2 = true → t1D = t2. + #t2; ncases t2; nnormalize; #H; ##[ ##30: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] +nqed. + +nlemma eqbit_to_eq31 : ∀t2.eq_bit t1E t2 = true → t1E = t2. + #t2; ncases t2; nnormalize; #H; ##[ ##31: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] +nqed. + +nlemma eqbit_to_eq32 : ∀t2.eq_bit t1F t2 = true → t1F = t2. + #t2; ncases t2; nnormalize; #H; ##[ ##32: napply refl_eq ##| ##*: napply (bool_destruct … H) ##] +nqed. + +nlemma eqbit_to_eq : ∀t1,t2.eq_bit t1 t2 = true → t1 = t2. + #t1; + ncases t1; + ##[ ##1: napply eqbit_to_eq1 + ##| ##2: napply eqbit_to_eq2 + ##| ##3: napply eqbit_to_eq3 + ##| ##4: napply eqbit_to_eq4 + ##| ##5: napply eqbit_to_eq5 + ##| ##6: napply eqbit_to_eq6 + ##| ##7: napply eqbit_to_eq7 + ##| ##8: napply eqbit_to_eq8 + ##| ##9: napply eqbit_to_eq9 + ##| ##10: napply eqbit_to_eq10 + ##| ##11: napply eqbit_to_eq11 + ##| ##12: napply eqbit_to_eq12 + ##| ##13: napply eqbit_to_eq13 + ##| ##14: napply eqbit_to_eq14 + ##| ##15: napply eqbit_to_eq15 + ##| ##16: napply eqbit_to_eq16 + ##| ##17: napply eqbit_to_eq17 + ##| ##18: napply eqbit_to_eq18 + ##| ##19: napply eqbit_to_eq19 + ##| ##20: napply eqbit_to_eq20 + ##| ##21: napply eqbit_to_eq21 + ##| ##22: napply eqbit_to_eq22 + ##| ##23: napply eqbit_to_eq23 + ##| ##24: napply eqbit_to_eq24 + ##| ##25: napply eqbit_to_eq25 + ##| ##26: napply eqbit_to_eq26 + ##| ##27: napply eqbit_to_eq27 + ##| ##28: napply eqbit_to_eq28 + ##| ##29: napply eqbit_to_eq29 + ##| ##30: napply eqbit_to_eq30 + ##| ##31: napply eqbit_to_eq31 + ##| ##32: napply eqbit_to_eq32 + ##] +nqed. + +nlemma eq_to_eqbit1 : ∀t2.t00 = t2 → eq_bit t00 t2 = true. + #t2; ncases t2; nnormalize; #H; ##[ ##1: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##] +nqed. + +nlemma eq_to_eqbit2 : ∀t2.t01 = t2 → eq_bit t01 t2 = true. + #t2; ncases t2; nnormalize; #H; ##[ ##2: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##] +nqed. + +nlemma eq_to_eqbit3 : ∀t2.t02 = t2 → eq_bit t02 t2 = true. + #t2; ncases t2; nnormalize; #H; ##[ ##3: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##] +nqed. + +nlemma eq_to_eqbit4 : ∀t2.t03 = t2 → eq_bit t03 t2 = true. + #t2; ncases t2; nnormalize; #H; ##[ ##4: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##] +nqed. + +nlemma eq_to_eqbit5 : ∀t2.t04 = t2 → eq_bit t04 t2 = true. + #t2; ncases t2; nnormalize; #H; ##[ ##5: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##] +nqed. + +nlemma eq_to_eqbit6 : ∀t2.t05 = t2 → eq_bit t05 t2 = true. + #t2; ncases t2; nnormalize; #H; ##[ ##6: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##] +nqed. + +nlemma eq_to_eqbit7 : ∀t2.t06 = t2 → eq_bit t06 t2 = true. + #t2; ncases t2; nnormalize; #H; ##[ ##7: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##] +nqed. + +nlemma eq_to_eqbit8 : ∀t2.t07 = t2 → eq_bit t07 t2 = true. + #t2; ncases t2; nnormalize; #H; ##[ ##8: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##] +nqed. + +nlemma eq_to_eqbit9 : ∀t2.t08 = t2 → eq_bit t08 t2 = true. + #t2; ncases t2; nnormalize; #H; ##[ ##9: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##] +nqed. + +nlemma eq_to_eqbit10 : ∀t2.t09 = t2 → eq_bit t09 t2 = true. + #t2; ncases t2; nnormalize; #H; ##[ ##10: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##] +nqed. + +nlemma eq_to_eqbit11 : ∀t2.t0A = t2 → eq_bit t0A t2 = true. + #t2; ncases t2; nnormalize; #H; ##[ ##11: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##] +nqed. + +nlemma eq_to_eqbit12 : ∀t2.t0B = t2 → eq_bit t0B t2 = true. + #t2; ncases t2; nnormalize; #H; ##[ ##12: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##] +nqed. + +nlemma eq_to_eqbit13 : ∀t2.t0C = t2 → eq_bit t0C t2 = true. + #t2; ncases t2; nnormalize; #H; ##[ ##13: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##] +nqed. + +nlemma eq_to_eqbit14 : ∀t2.t0D = t2 → eq_bit t0D t2 = true. + #t2; ncases t2; nnormalize; #H; ##[ ##14: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##] +nqed. + +nlemma eq_to_eqbit15 : ∀t2.t0E = t2 → eq_bit t0E t2 = true. + #t2; ncases t2; nnormalize; #H; ##[ ##15: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##] +nqed. + +nlemma eq_to_eqbit16 : ∀t2.t0F = t2 → eq_bit t0F t2 = true. + #t2; ncases t2; nnormalize; #H; ##[ ##16: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##] +nqed. + +nlemma eq_to_eqbit17 : ∀t2.t10 = t2 → eq_bit t10 t2 = true. + #t2; ncases t2; nnormalize; #H; ##[ ##17: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##] +nqed. + +nlemma eq_to_eqbit18 : ∀t2.t11 = t2 → eq_bit t11 t2 = true. + #t2; ncases t2; nnormalize; #H; ##[ ##18: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##] +nqed. + +nlemma eq_to_eqbit19 : ∀t2.t12 = t2 → eq_bit t12 t2 = true. + #t2; ncases t2; nnormalize; #H; ##[ ##19: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##] +nqed. + +nlemma eq_to_eqbit20 : ∀t2.t13 = t2 → eq_bit t13 t2 = true. + #t2; ncases t2; nnormalize; #H; ##[ ##20: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##] +nqed. + +nlemma eq_to_eqbit21 : ∀t2.t14 = t2 → eq_bit t14 t2 = true. + #t2; ncases t2; nnormalize; #H; ##[ ##21: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##] +nqed. + +nlemma eq_to_eqbit22 : ∀t2.t15 = t2 → eq_bit t15 t2 = true. + #t2; ncases t2; nnormalize; #H; ##[ ##22: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##] +nqed. + +nlemma eq_to_eqbit23 : ∀t2.t16 = t2 → eq_bit t16 t2 = true. + #t2; ncases t2; nnormalize; #H; ##[ ##23: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##] +nqed. + +nlemma eq_to_eqbit24 : ∀t2.t17 = t2 → eq_bit t17 t2 = true. + #t2; ncases t2; nnormalize; #H; ##[ ##24: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##] +nqed. + +nlemma eq_to_eqbit25 : ∀t2.t18 = t2 → eq_bit t18 t2 = true. + #t2; ncases t2; nnormalize; #H; ##[ ##25: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##] +nqed. + +nlemma eq_to_eqbit26 : ∀t2.t19 = t2 → eq_bit t19 t2 = true. + #t2; ncases t2; nnormalize; #H; ##[ ##26: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##] +nqed. + +nlemma eq_to_eqbit27 : ∀t2.t1A = t2 → eq_bit t1A t2 = true. + #t2; ncases t2; nnormalize; #H; ##[ ##27: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##] +nqed. + +nlemma eq_to_eqbit28 : ∀t2.t1B = t2 → eq_bit t1B t2 = true. + #t2; ncases t2; nnormalize; #H; ##[ ##28: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##] +nqed. + +nlemma eq_to_eqbit29 : ∀t2.t1C = t2 → eq_bit t1C t2 = true. + #t2; ncases t2; nnormalize; #H; ##[ ##29: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##] +nqed. + +nlemma eq_to_eqbit30 : ∀t2.t1D = t2 → eq_bit t1D t2 = true. + #t2; ncases t2; nnormalize; #H; ##[ ##30: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##] +nqed. + +nlemma eq_to_eqbit31 : ∀t2.t1E = t2 → eq_bit t1E t2 = true. + #t2; ncases t2; nnormalize; #H; ##[ ##31: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##] +nqed. + +nlemma eq_to_eqbit32 : ∀t2.t1F = t2 → eq_bit t1F t2 = true. + #t2; ncases t2; nnormalize; #H; ##[ ##32: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##] +nqed. + +nlemma eq_to_eqbit : ∀t1,t2.t1 = t2 → eq_bit t1 t2 = true. + #t1; + ncases t1; + ##[ ##1: napply eq_to_eqbit1 + ##| ##2: napply eq_to_eqbit2 + ##| ##3: napply eq_to_eqbit3 + ##| ##4: napply eq_to_eqbit4 + ##| ##5: napply eq_to_eqbit5 + ##| ##6: napply eq_to_eqbit6 + ##| ##7: napply eq_to_eqbit7 + ##| ##8: napply eq_to_eqbit8 + ##| ##9: napply eq_to_eqbit9 + ##| ##10: napply eq_to_eqbit10 + ##| ##11: napply eq_to_eqbit11 + ##| ##12: napply eq_to_eqbit12 + ##| ##13: napply eq_to_eqbit13 + ##| ##14: napply eq_to_eqbit14 + ##| ##15: napply eq_to_eqbit15 + ##| ##16: napply eq_to_eqbit16 + ##| ##17: napply eq_to_eqbit17 + ##| ##18: napply eq_to_eqbit18 + ##| ##19: napply eq_to_eqbit19 + ##| ##20: napply eq_to_eqbit20 + ##| ##21: napply eq_to_eqbit21 + ##| ##22: napply eq_to_eqbit22 + ##| ##23: napply eq_to_eqbit23 + ##| ##24: napply eq_to_eqbit24 + ##| ##25: napply eq_to_eqbit25 + ##| ##26: napply eq_to_eqbit26 + ##| ##27: napply eq_to_eqbit27 + ##| ##28: napply eq_to_eqbit28 + ##| ##29: napply eq_to_eqbit29 + ##| ##30: napply eq_to_eqbit30 + ##| ##31: napply eq_to_eqbit31 + ##| ##32: napply eq_to_eqbit32 + ##] +nqed. diff --git a/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma index 25d855d31..3549148de 100755 --- a/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma @@ -132,43 +132,34 @@ nlemma eq_to_eqbool : ∀b1,b2.b1 = b2 → eq_bool b1 b2 = true. ##] nqed. -nlemma neqbool_to_neq : ∀b1,b2:bool.(eq_bool b1 b2 = false) → (b1 ≠ b2). - #b1; #b2; - ncases b1; - ncases b2; - nnormalize; - ##[ ##1,4: #H; napply (bool_destruct … H) - ##| ##*: #H; #H1; napply (bool_destruct … H1) - ##] -nqed. - -nlemma neq_to_neqbool : ∀b1,b2.b1 ≠ b2 → eq_bool b1 b2 = false. +nlemma andb_true_true_l: ∀b1,b2.(b1 ⊗ b2) = true → b1 = true. #b1; #b2; ncases b1; ncases b2; nnormalize; - ##[ ##1,4: #H; napply False_ind; napply (H (refl_eq …)) - ##| ##*: #H; napply refl_eq + ##[ ##1,2: #H; napply refl_eq + ##| ##*: #H; napply (bool_destruct … H) ##] nqed. -nlemma andb_true_true_l: ∀b1,b2.(b1 ⊗ b2) = true → b1 = true. +nlemma andb_true_true_r: ∀b1,b2.(b1 ⊗ b2) = true → b2 = true. #b1; #b2; ncases b1; ncases b2; nnormalize; - ##[ ##1,2: #H; napply refl_eq + ##[ ##1,3: #H; napply refl_eq ##| ##*: #H; napply (bool_destruct … H) ##] nqed. -nlemma andb_true_true_r: ∀b1,b2.(b1 ⊗ b2) = true → b2 = true. +nlemma andb_false : ∀b1,b2.(b1 ⊗ b2) = false → (b1 = false) ∨ (b2 = false). #b1; #b2; ncases b1; ncases b2; nnormalize; - ##[ ##1,3: #H; napply refl_eq - ##| ##*: #H; napply (bool_destruct … H) + ##[ ##1: #H; napply (bool_destruct … H) + ##| ##2,4: #H; napply (or_intror … H) + ##| ##3: #H; napply (or_introl … H) ##] nqed. diff --git a/helm/software/matita/contribs/ng_assembly/num/byte8.ma b/helm/software/matita/contribs/ng_assembly/num/byte8.ma new file mode 100755 index 000000000..f2cbdb758 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/num/byte8.ma @@ -0,0 +1,363 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* ********************************************************************** *) + +include "num/exadecim.ma". +include "num/bitrigesim.ma". + +(* **** *) +(* BYTE *) +(* **** *) + +nrecord byte8 : Type ≝ + { + b8h: exadecim; + b8l: exadecim + }. + +(* \langle \rangle *) +notation "〈x,y〉" non associative with precedence 80 + for @{ 'mk_byte8 $x $y }. +interpretation "mk_byte8" 'mk_byte8 x y = (mk_byte8 x y). + +(* operatore = *) +ndefinition eq_b8 ≝ λb1,b2:byte8.(eq_ex (b8h b1) (b8h b2)) ⊗ (eq_ex (b8l b1) (b8l b2)). + +(* operatore < *) +ndefinition lt_b8 ≝ +λb1,b2:byte8.match lt_ex (b8h b1) (b8h b2) with + [ true ⇒ true + | false ⇒ match gt_ex (b8h b1) (b8h b2) with + [ true ⇒ false + | false ⇒ lt_ex (b8l b1) (b8l b2) ]]. + +(* operatore ≤ *) +ndefinition le_b8 ≝ λb1,b2:byte8.(eq_b8 b1 b2) ⊕ (lt_b8 b1 b2). + +(* operatore > *) +ndefinition gt_b8 ≝ λb1,b2:byte8.⊖ (le_b8 b1 b2). + +(* operatore ≥ *) +ndefinition ge_b8 ≝ λb1,b2:byte8.⊖ (lt_b8 b1 b2). + +(* operatore and *) +ndefinition and_b8 ≝ +λb1,b2:byte8.mk_byte8 (and_ex (b8h b1) (b8h b2)) (and_ex (b8l b1) (b8l b2)). + +(* operatore or *) +ndefinition or_b8 ≝ +λb1,b2:byte8.mk_byte8 (or_ex (b8h b1) (b8h b2)) (or_ex (b8l b1) (b8l b2)). + +(* operatore xor *) +ndefinition xor_b8 ≝ +λb1,b2:byte8.mk_byte8 (xor_ex (b8h b1) (b8h b2)) (xor_ex (b8l b1) (b8l b2)). + +(* operatore rotazione destra con carry *) +ndefinition rcr_b8 ≝ +λb:byte8.λc:bool.match rcr_ex (b8h b) c with + [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with + [ pair bl' c'' ⇒ pair … (mk_byte8 bh' bl') c'' ]]. + +(* operatore shift destro *) +ndefinition shr_b8 ≝ +λb:byte8.match rcr_ex (b8h b) false with + [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with + [ pair bl' c'' ⇒ pair … (mk_byte8 bh' bl') c'' ]]. + +(* operatore rotazione destra *) +ndefinition ror_b8 ≝ +λb:byte8.match rcr_ex (b8h b) false with + [ pair bh' c' ⇒ match rcr_ex (b8l b) c' with + [ pair bl' c'' ⇒ match c'' with + [ true ⇒ mk_byte8 (or_ex x8 bh') bl' + | false ⇒ mk_byte8 bh' bl' ]]]. + +(* operatore rotazione destra n-volte *) +nlet rec ror_b8_n (b:byte8) (n:oct) (r:rec_oct n) on r ≝ + match r with + [ oc_O ⇒ b + | oc_S t n' ⇒ ror_b8_n (ror_b8 b) t n' ]. + +(* operatore rotazione sinistra con carry *) +ndefinition rcl_b8 ≝ +λb:byte8.λc:bool.match rcl_ex (b8l b) c with + [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with + [ pair bh' c'' ⇒ pair … (mk_byte8 bh' bl') c'' ]]. + +(* operatore shift sinistro *) +ndefinition shl_b8 ≝ +λb:byte8.match rcl_ex (b8l b) false with + [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with + [ pair bh' c'' ⇒ pair … (mk_byte8 bh' bl') c'' ]]. + +(* operatore rotazione sinistra *) +ndefinition rol_b8 ≝ +λb:byte8.match rcl_ex (b8l b) false with + [ pair bl' c' ⇒ match rcl_ex (b8h b) c' with + [ pair bh' c'' ⇒ match c'' with + [ true ⇒ mk_byte8 bh' (or_ex x1 bl') + | false ⇒ mk_byte8 bh' bl' ]]]. + +(* operatore rotazione sinistra n-volte *) +nlet rec rol_b8_n (b:byte8) (n:oct) (r:rec_oct n) on r ≝ + match r with + [ oc_O ⇒ b + | oc_S t n' ⇒ rol_b8_n (rol_b8 b) t n' ]. + +(* operatore not/complemento a 1 *) +ndefinition not_b8 ≝ +λb:byte8.mk_byte8 (not_ex (b8h b)) (not_ex (b8l b)). + +(* operatore somma con data+carry → data+carry *) +ndefinition plus_b8_dc_dc ≝ +λb1,b2:byte8.λc:bool. + match plus_ex_dc_dc (b8l b1) (b8l b2) c with + [ pair l c ⇒ match plus_ex_dc_dc (b8h b1) (b8h b2) c with + [ pair h c' ⇒ pair … 〈h,l〉 c' ]]. + +(* operatore somma con data+carry → data *) +ndefinition plus_b8_dc_d ≝ +λb1,b2:byte8.λc:bool. + match plus_ex_dc_dc (b8l b1) (b8l b2) c with + [ pair l c ⇒ 〈plus_ex_dc_d (b8h b1) (b8h b2) c,l〉 ]. + +(* operatore somma con data+carry → c *) +ndefinition plus_b8_dc_c ≝ +λb1,b2:byte8.λc:bool. + plus_ex_dc_c (b8h b1) (b8h b2) (plus_ex_dc_c (b8l b1) (b8l b2) c). + +(* operatore somma con data → data+carry *) +ndefinition plus_b8_d_dc ≝ +λb1,b2:byte8. + match plus_ex_d_dc (b8l b1) (b8l b2) with + [ pair l c ⇒ match plus_ex_dc_dc (b8h b1) (b8h b2) c with + [ pair h c' ⇒ pair … 〈h,l〉 c' ]]. + +(* operatore somma con data → data *) +ndefinition plus_b8_d_d ≝ +λb1,b2:byte8. + match plus_ex_d_dc (b8l b1) (b8l b2) with + [ pair l c ⇒ 〈plus_ex_dc_d (b8h b1) (b8h b2) c,l〉 ]. + +(* operatore somma con data → c *) +ndefinition plus_b8_d_c ≝ +λb1,b2:byte8. + plus_ex_dc_c (b8h b1) (b8h b2) (plus_ex_d_c (b8l b1) (b8l b2)). + +(* operatore Most Significant Bit *) +ndefinition MSB_b8 ≝ λb:byte8.eq_ex x8 (and_ex x8 (b8h b)). + +(* operatore predecessore *) +ndefinition pred_b8 ≝ +λb:byte8.match eq_ex (b8l b) x0 with + [ true ⇒ mk_byte8 (pred_ex (b8h b)) (pred_ex (b8l b)) + | false ⇒ mk_byte8 (b8h b) (pred_ex (b8l b)) ]. + +(* operatore successore *) +ndefinition succ_b8 ≝ +λb:byte8.match eq_ex (b8l b) xF with + [ true ⇒ mk_byte8 (succ_ex (b8h b)) (succ_ex (b8l b)) + | false ⇒ mk_byte8 (b8h b) (succ_ex (b8l b)) ]. + +(* operatore neg/complemento a 2 *) +ndefinition compl_b8 ≝ +λb:byte8.match MSB_b8 b with + [ true ⇒ succ_b8 (not_b8 b) + | false ⇒ not_b8 (pred_b8 b) ]. + +(* operatore moltiplicazione senza segno: e*e=[0x00,0xE1] *) +ndefinition mul_ex ≝ +λe1,e2:exadecim.match e1 with + [ x0 ⇒ match e2 with + [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x0〉 | x2 ⇒ 〈x0,x0〉 | x3 ⇒ 〈x0,x0〉 + | x4 ⇒ 〈x0,x0〉 | x5 ⇒ 〈x0,x0〉 | x6 ⇒ 〈x0,x0〉 | x7 ⇒ 〈x0,x0〉 + | x8 ⇒ 〈x0,x0〉 | x9 ⇒ 〈x0,x0〉 | xA ⇒ 〈x0,x0〉 | xB ⇒ 〈x0,x0〉 + | xC ⇒ 〈x0,x0〉 | xD ⇒ 〈x0,x0〉 | xE ⇒ 〈x0,x0〉 | xF ⇒ 〈x0,x0〉 ] + | x1 ⇒ match e2 with + [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x1〉 | x2 ⇒ 〈x0,x2〉 | x3 ⇒ 〈x0,x3〉 + | x4 ⇒ 〈x0,x4〉 | x5 ⇒ 〈x0,x5〉 | x6 ⇒ 〈x0,x6〉 | x7 ⇒ 〈x0,x7〉 + | x8 ⇒ 〈x0,x8〉 | x9 ⇒ 〈x0,x9〉 | xA ⇒ 〈x0,xA〉 | xB ⇒ 〈x0,xB〉 + | xC ⇒ 〈x0,xC〉 | xD ⇒ 〈x0,xD〉 | xE ⇒ 〈x0,xE〉 | xF ⇒ 〈x0,xF〉 ] + | x2 ⇒ match e2 with + [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x2〉 | x2 ⇒ 〈x0,x4〉 | x3 ⇒ 〈x0,x6〉 + | x4 ⇒ 〈x0,x8〉 | x5 ⇒ 〈x0,xA〉 | x6 ⇒ 〈x0,xC〉 | x7 ⇒ 〈x0,xE〉 + | x8 ⇒ 〈x1,x0〉 | x9 ⇒ 〈x1,x2〉 | xA ⇒ 〈x1,x4〉 | xB ⇒ 〈x1,x6〉 + | xC ⇒ 〈x1,x8〉 | xD ⇒ 〈x1,xA〉 | xE ⇒ 〈x1,xC〉 | xF ⇒ 〈x1,xE〉 ] + | x3 ⇒ match e2 with + [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x3〉 | x2 ⇒ 〈x0,x6〉 | x3 ⇒ 〈x0,x9〉 + | x4 ⇒ 〈x0,xC〉 | x5 ⇒ 〈x0,xF〉 | x6 ⇒ 〈x1,x2〉 | x7 ⇒ 〈x1,x5〉 + | x8 ⇒ 〈x1,x8〉 | x9 ⇒ 〈x1,xB〉 | xA ⇒ 〈x1,xE〉 | xB ⇒ 〈x2,x1〉 + | xC ⇒ 〈x2,x4〉 | xD ⇒ 〈x2,x7〉 | xE ⇒ 〈x2,xA〉 | xF ⇒ 〈x2,xD〉 ] + | x4 ⇒ match e2 with + [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x4〉 | x2 ⇒ 〈x0,x8〉 | x3 ⇒ 〈x0,xC〉 + | x4 ⇒ 〈x1,x0〉 | x5 ⇒ 〈x1,x4〉 | x6 ⇒ 〈x1,x8〉 | x7 ⇒ 〈x1,xC〉 + | x8 ⇒ 〈x2,x0〉 | x9 ⇒ 〈x2,x4〉 | xA ⇒ 〈x2,x8〉 | xB ⇒ 〈x2,xC〉 + | xC ⇒ 〈x3,x0〉 | xD ⇒ 〈x3,x4〉 | xE ⇒ 〈x3,x8〉 | xF ⇒ 〈x3,xC〉 ] + | x5 ⇒ match e2 with + [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x5〉 | x2 ⇒ 〈x0,xA〉 | x3 ⇒ 〈x0,xF〉 + | x4 ⇒ 〈x1,x4〉 | x5 ⇒ 〈x1,x9〉 | x6 ⇒ 〈x1,xE〉 | x7 ⇒ 〈x2,x3〉 + | x8 ⇒ 〈x2,x8〉 | x9 ⇒ 〈x2,xD〉 | xA ⇒ 〈x3,x2〉 | xB ⇒ 〈x3,x7〉 + | xC ⇒ 〈x3,xC〉 | xD ⇒ 〈x4,x1〉 | xE ⇒ 〈x4,x6〉 | xF ⇒ 〈x4,xB〉 ] + | x6 ⇒ match e2 with + [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x6〉 | x2 ⇒ 〈x0,xC〉 | x3 ⇒ 〈x1,x2〉 + | x4 ⇒ 〈x1,x8〉 | x5 ⇒ 〈x1,xE〉 | x6 ⇒ 〈x2,x4〉 | x7 ⇒ 〈x2,xA〉 + | x8 ⇒ 〈x3,x0〉 | x9 ⇒ 〈x3,x6〉 | xA ⇒ 〈x3,xC〉 | xB ⇒ 〈x4,x2〉 + | xC ⇒ 〈x4,x8〉 | xD ⇒ 〈x4,xE〉 | xE ⇒ 〈x5,x4〉 | xF ⇒ 〈x5,xA〉 ] + | x7 ⇒ match e2 with + [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x7〉 | x2 ⇒ 〈x0,xE〉 | x3 ⇒ 〈x1,x5〉 + | x4 ⇒ 〈x1,xC〉 | x5 ⇒ 〈x2,x3〉 | x6 ⇒ 〈x2,xA〉 | x7 ⇒ 〈x3,x1〉 + | x8 ⇒ 〈x3,x8〉 | x9 ⇒ 〈x3,xF〉 | xA ⇒ 〈x4,x6〉 | xB ⇒ 〈x4,xD〉 + | xC ⇒ 〈x5,x4〉 | xD ⇒ 〈x5,xB〉 | xE ⇒ 〈x6,x2〉 | xF ⇒ 〈x6,x9〉 ] + | x8 ⇒ match e2 with + [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x8〉 | x2 ⇒ 〈x1,x0〉 | x3 ⇒ 〈x1,x8〉 + | x4 ⇒ 〈x2,x0〉 | x5 ⇒ 〈x2,x8〉 | x6 ⇒ 〈x3,x0〉 | x7 ⇒ 〈x3,x8〉 + | x8 ⇒ 〈x4,x0〉 | x9 ⇒ 〈x4,x8〉 | xA ⇒ 〈x5,x0〉 | xB ⇒ 〈x5,x8〉 + | xC ⇒ 〈x6,x0〉 | xD ⇒ 〈x6,x8〉 | xE ⇒ 〈x7,x0〉 | xF ⇒ 〈x7,x8〉 ] + | x9 ⇒ match e2 with + [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,x9〉 | x2 ⇒ 〈x1,x2〉 | x3 ⇒ 〈x1,xB〉 + | x4 ⇒ 〈x2,x4〉 | x5 ⇒ 〈x2,xD〉 | x6 ⇒ 〈x3,x6〉 | x7 ⇒ 〈x3,xF〉 + | x8 ⇒ 〈x4,x8〉 | x9 ⇒ 〈x5,x1〉 | xA ⇒ 〈x5,xA〉 | xB ⇒ 〈x6,x3〉 + | xC ⇒ 〈x6,xC〉 | xD ⇒ 〈x7,x5〉 | xE ⇒ 〈x7,xE〉 | xF ⇒ 〈x8,x7〉 ] + | xA ⇒ match e2 with + [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xA〉 | x2 ⇒ 〈x1,x4〉 | x3 ⇒ 〈x1,xE〉 + | x4 ⇒ 〈x2,x8〉 | x5 ⇒ 〈x3,x2〉 | x6 ⇒ 〈x3,xC〉 | x7 ⇒ 〈x4,x6〉 + | x8 ⇒ 〈x5,x0〉 | x9 ⇒ 〈x5,xA〉 | xA ⇒ 〈x6,x4〉 | xB ⇒ 〈x6,xE〉 + | xC ⇒ 〈x7,x8〉 | xD ⇒ 〈x8,x2〉 | xE ⇒ 〈x8,xC〉 | xF ⇒ 〈x9,x6〉 ] + | xB ⇒ match e2 with + [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xB〉 | x2 ⇒ 〈x1,x6〉 | x3 ⇒ 〈x2,x1〉 + | x4 ⇒ 〈x2,xC〉 | x5 ⇒ 〈x3,x7〉 | x6 ⇒ 〈x4,x2〉 | x7 ⇒ 〈x4,xD〉 + | x8 ⇒ 〈x5,x8〉 | x9 ⇒ 〈x6,x3〉 | xA ⇒ 〈x6,xE〉 | xB ⇒ 〈x7,x9〉 + | xC ⇒ 〈x8,x4〉 | xD ⇒ 〈x8,xF〉 | xE ⇒ 〈x9,xA〉 | xF ⇒ 〈xA,x5〉 ] + | xC ⇒ match e2 with + [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xC〉 | x2 ⇒ 〈x1,x8〉 | x3 ⇒ 〈x2,x4〉 + | x4 ⇒ 〈x3,x0〉 | x5 ⇒ 〈x3,xC〉 | x6 ⇒ 〈x4,x8〉 | x7 ⇒ 〈x5,x4〉 + | x8 ⇒ 〈x6,x0〉 | x9 ⇒ 〈x6,xC〉 | xA ⇒ 〈x7,x8〉 | xB ⇒ 〈x8,x4〉 + | xC ⇒ 〈x9,x0〉 | xD ⇒ 〈x9,xC〉 | xE ⇒ 〈xA,x8〉 | xF ⇒ 〈xB,x4〉 ] + | xD ⇒ match e2 with + [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xD〉 | x2 ⇒ 〈x1,xA〉 | x3 ⇒ 〈x2,x7〉 + | x4 ⇒ 〈x3,x4〉 | x5 ⇒ 〈x4,x1〉 | x6 ⇒ 〈x4,xE〉 | x7 ⇒ 〈x5,xB〉 + | x8 ⇒ 〈x6,x8〉 | x9 ⇒ 〈x7,x5〉 | xA ⇒ 〈x8,x2〉 | xB ⇒ 〈x8,xF〉 + | xC ⇒ 〈x9,xC〉 | xD ⇒ 〈xA,x9〉 | xE ⇒ 〈xB,x6〉 | xF ⇒ 〈xC,x3〉 ] + | xE ⇒ match e2 with + [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xE〉 | x2 ⇒ 〈x1,xC〉 | x3 ⇒ 〈x2,xA〉 + | x4 ⇒ 〈x3,x8〉 | x5 ⇒ 〈x4,x6〉 | x6 ⇒ 〈x5,x4〉 | x7 ⇒ 〈x6,x2〉 + | x8 ⇒ 〈x7,x0〉 | x9 ⇒ 〈x7,xE〉 | xA ⇒ 〈x8,xC〉 | xB ⇒ 〈x9,xA〉 + | xC ⇒ 〈xA,x8〉 | xD ⇒ 〈xB,x6〉 | xE ⇒ 〈xC,x4〉 | xF ⇒ 〈xD,x2〉 ] + | xF ⇒ match e2 with + [ x0 ⇒ 〈x0,x0〉 | x1 ⇒ 〈x0,xF〉 | x2 ⇒ 〈x1,xE〉 | x3 ⇒ 〈x2,xD〉 + | x4 ⇒ 〈x3,xC〉 | x5 ⇒ 〈x4,xB〉 | x6 ⇒ 〈x5,xA〉 | x7 ⇒ 〈x6,x9〉 + | x8 ⇒ 〈x7,x8〉 | x9 ⇒ 〈x8,x7〉 | xA ⇒ 〈x9,x6〉 | xB ⇒ 〈xA,x5〉 + | xC ⇒ 〈xB,x4〉 | xD ⇒ 〈xC,x3〉 | xE ⇒ 〈xD,x2〉 | xF ⇒ 〈xE,x1〉 ] + ]. + +(* correzione per somma su BCD *) +(* input: halfcarry,carry,X(BCD+BCD) *) +(* output: X',carry' *) +ndefinition daa_b8 ≝ +λh,c:bool.λX:byte8. + match lt_b8 X 〈x9,xA〉 with + (* [X:0x00-0x99] *) + (* c' = c *) + (* X' = [(b16l X):0x0-0x9] X + [h=1 ? 0x06 : 0x00] + [c=1 ? 0x60 : 0x00] + [(b16l X):0xA-0xF] X + 0x06 + [c=1 ? 0x60 : 0x00] *) + [ true ⇒ + let X' ≝ match (lt_ex (b8l X) xA) ⊗ (⊖h) with + [ true ⇒ X + | false ⇒ plus_b8_d_d X 〈x0,x6〉 ] in + let X'' ≝ match c with + [ true ⇒ plus_b8_d_d X' 〈x6,x0〉 + | false ⇒ X' ] in + pair … X'' c + (* [X:0x9A-0xFF] *) + (* c' = 1 *) + (* X' = [X:0x9A-0xFF] + [(b16l X):0x0-0x9] X + [h=1 ? 0x06 : 0x00] + 0x60 + [(b16l X):0xA-0xF] X + 0x6 + 0x60 *) + | false ⇒ + let X' ≝ match (lt_ex (b8l X) xA) ⊗ (⊖h) with + [ true ⇒ X + | false ⇒ plus_b8_d_d X 〈x0,x6〉 ] in + let X'' ≝ plus_b8_d_d X' 〈x6,x0〉 in + pair … X'' true + ]. + +(* iteratore sui byte *) +ndefinition forall_b8 ≝ + λP. + forall_ex (λbh. + forall_ex (λbl. + P (mk_byte8 bh bl))). + +(* byte ricorsivi *) +ninductive rec_byte8 : byte8 → Type ≝ + b8_O : rec_byte8 〈x0,x0〉 +| b8_S : ∀n.rec_byte8 n → rec_byte8 (succ_b8 n). + +(* byte → byte ricorsivi *) +ndefinition b8_to_recb8_aux1 : Πn.rec_byte8 〈n,x0〉 → rec_byte8 〈succ_ex n,x0〉 ≝ +λn.λrecb:rec_byte8 〈n,x0〉. + b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? ( + b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb))))))))))))))). + +(* ... cifra esadecimale superiore *) +nlet rec b8_to_recb8_aux2 (n:exadecim) (r:rec_exadecim n) on r ≝ + match r return λx.λy:rec_exadecim x.rec_byte8 〈x,x0〉 with + [ ex_O ⇒ b8_O + | ex_S t n' ⇒ b8_to_recb8_aux1 ? (b8_to_recb8_aux2 t n') + ]. + +(* ... cifra esadecimale inferiore *) +ndefinition b8_to_recb8_aux3 : Πn1,n2.rec_byte8 〈n1,x0〉 → rec_byte8 〈n1,n2〉 ≝ +λn1,n2.λrecb:rec_byte8 〈n1,x0〉. + match n2 return λx.rec_byte8 〈n1,x〉 with + [ x0 ⇒ recb + | x1 ⇒ b8_S ? recb + | x2 ⇒ b8_S ? (b8_S ? recb) + | x3 ⇒ b8_S ? (b8_S ? (b8_S ? recb)) + | x4 ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? recb))) + | x5 ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb)))) + | x6 ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb))))) + | x7 ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb)))))) + | x8 ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb))))))) + | x9 ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb)))))))) + | xA ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb))))))))) + | xB ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb)))))))))) + | xC ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb))))))))))) + | xD ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb)))))))))))) + | xE ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb))))))))))))) + | xF ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb)))))))))))))) + ]. + +ndefinition b8_to_recb8 ≝ +λn.b8_to_recb8_aux3 (b8h n) (b8l n) (b8_to_recb8_aux2 (b8h n) (ex_to_recex (b8h n))). + +(* ottali → esadecimali *) +ndefinition b8_of_bit ≝ +λn.match n with + [ t00 ⇒ 〈x0,x0〉 | t01 ⇒ 〈x0,x1〉 | t02 ⇒ 〈x0,x2〉 | t03 ⇒ 〈x0,x3〉 + | t04 ⇒ 〈x0,x4〉 | t05 ⇒ 〈x0,x5〉 | t06 ⇒ 〈x0,x6〉 | t07 ⇒ 〈x0,x7〉 + | t08 ⇒ 〈x0,x8〉 | t09 ⇒ 〈x0,x9〉 | t0A ⇒ 〈x0,xA〉 | t0B ⇒ 〈x0,xB〉 + | t0C ⇒ 〈x0,xC〉 | t0D ⇒ 〈x0,xD〉 | t0E ⇒ 〈x0,xE〉 | t0F ⇒ 〈x0,xF〉 + | t10 ⇒ 〈x1,x0〉 | t11 ⇒ 〈x1,x1〉 | t12 ⇒ 〈x1,x2〉 | t13 ⇒ 〈x1,x3〉 + | t14 ⇒ 〈x1,x4〉 | t15 ⇒ 〈x1,x5〉 | t16 ⇒ 〈x1,x6〉 | t17 ⇒ 〈x1,x7〉 + | t18 ⇒ 〈x1,x8〉 | t19 ⇒ 〈x1,x9〉 | t1A ⇒ 〈x1,xA〉 | t1B ⇒ 〈x1,xB〉 + | t1C ⇒ 〈x1,xC〉 | t1D ⇒ 〈x1,xD〉 | t1E ⇒ 〈x1,xE〉 | t1F ⇒ 〈x1,xF〉 + ]. diff --git a/helm/software/matita/contribs/ng_assembly/num/byte8_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/byte8_lemmas.ma new file mode 100755 index 000000000..99d1b5227 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/num/byte8_lemmas.ma @@ -0,0 +1,288 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* ********************************************************************** *) + +include "num/byte8.ma". +include "num/exadecim_lemmas.ma". + +(* **** *) +(* BYTE *) +(* **** *) + +nlemma byte8_destruct_1 : +∀x1,x2,y1,y2. + mk_byte8 x1 y1 = mk_byte8 x2 y2 → x1 = x2. + #x1; #x2; #y1; #y2; #H; + nchange with (match mk_byte8 x2 y2 with [ mk_byte8 a _ ⇒ x1 = a ]); + nrewrite < H; + nnormalize; + napply refl_eq. +nqed. + +nlemma byte8_destruct_2 : +∀x1,x2,y1,y2. + mk_byte8 x1 y1 = mk_byte8 x2 y2 → y1 = y2. + #x1; #x2; #y1; #y2; #H; + nchange with (match mk_byte8 x2 y2 with [ mk_byte8 _ b ⇒ y1 = b ]); + nrewrite < H; + nnormalize; + napply refl_eq. +nqed. + +nlemma symmetric_eqb8 : symmetricT byte8 bool eq_b8. + #b1; #b2; + nelim b1; + nelim b2; + #e1; #e2; #e3; #e4; + nchange with (((eq_ex e3 e1)⊗(eq_ex e4 e2)) = ((eq_ex e1 e3)⊗(eq_ex e2 e4))); + nrewrite > (symmetric_eqex e1 e3); + nrewrite > (symmetric_eqex e2 e4); + napply refl_eq. +nqed. + +nlemma symmetric_andb8 : symmetricT byte8 byte8 and_b8. + #b1; #b2; + nelim b1; + nelim b2; + #e1; #e2; #e3; #e4; + nchange with ((mk_byte8 (and_ex e3 e1) (and_ex e4 e2)) = (mk_byte8 (and_ex e1 e3) (and_ex e2 e4))); + nrewrite > (symmetric_andex e1 e3); + nrewrite > (symmetric_andex e2 e4); + napply refl_eq. +nqed. + +nlemma associative_andb8 : ∀b1,b2,b3.(and_b8 (and_b8 b1 b2) b3) = (and_b8 b1 (and_b8 b2 b3)). + #b1; #b2; #b3; + nelim b1; + #e1; #e2; + nelim b2; + #e3; #e4; + nelim b3; + #e5; #e6; + nchange with (mk_byte8 (and_ex (and_ex e1 e3) e5) (and_ex (and_ex e2 e4) e6) = + mk_byte8 (and_ex e1 (and_ex e3 e5)) (and_ex e2 (and_ex e4 e6))); + nrewrite < (associative_andex e1 e3 e5); + nrewrite < (associative_andex e2 e4 e6); + napply refl_eq. +nqed. + +nlemma symmetric_orb8 : symmetricT byte8 byte8 or_b8. + #b1; #b2; + nelim b1; + nelim b2; + #e1; #e2; #e3; #e4; + nchange with ((mk_byte8 (or_ex e3 e1) (or_ex e4 e2)) = (mk_byte8 (or_ex e1 e3) (or_ex e2 e4))); + nrewrite > (symmetric_orex e1 e3); + nrewrite > (symmetric_orex e2 e4); + napply refl_eq. +nqed. + +nlemma associative_orb8 : ∀b1,b2,b3.(or_b8 (or_b8 b1 b2) b3) = (or_b8 b1 (or_b8 b2 b3)). + #b1; #b2; #b3; + nelim b1; + #e1; #e2; + nelim b2; + #e3; #e4; + nelim b3; + #e5; #e6; + nchange with (mk_byte8 (or_ex (or_ex e1 e3) e5) (or_ex (or_ex e2 e4) e6) = + mk_byte8 (or_ex e1 (or_ex e3 e5)) (or_ex e2 (or_ex e4 e6))); + nrewrite < (associative_orex e1 e3 e5); + nrewrite < (associative_orex e2 e4 e6); + napply refl_eq. +nqed. + +nlemma symmetric_xorb8 : symmetricT byte8 byte8 xor_b8. + #b1; #b2; + nelim b1; + nelim b2; + #e1; #e2; #e3; #e4; + nchange with ((mk_byte8 (xor_ex e3 e1) (xor_ex e4 e2)) = (mk_byte8 (xor_ex e1 e3) (xor_ex e2 e4))); + nrewrite > (symmetric_xorex e1 e3); + nrewrite > (symmetric_xorex e2 e4); + napply refl_eq. +nqed. + +nlemma associative_xorb8 : ∀b1,b2,b3.(xor_b8 (xor_b8 b1 b2) b3) = (xor_b8 b1 (xor_b8 b2 b3)). + #b1; #b2; #b3; + nelim b1; + #e1; #e2; + nelim b2; + #e3; #e4; + nelim b3; + #e5; #e6; + nchange with (mk_byte8 (xor_ex (xor_ex e1 e3) e5) (xor_ex (xor_ex e2 e4) e6) = + mk_byte8 (xor_ex e1 (xor_ex e3 e5)) (xor_ex e2 (xor_ex e4 e6))); + nrewrite < (associative_xorex e1 e3 e5); + nrewrite < (associative_xorex e2 e4 e6); + napply refl_eq. +nqed. + +nlemma symmetric_plusb8_dc_dc : ∀b1,b2,c.plus_b8_dc_dc b1 b2 c = plus_b8_dc_dc b2 b1 c. + #b1; #b2; #c; + nelim b1; + #e1; #e2; + nelim b2; + #e3; #e4; + nchange with ( + match plus_ex_dc_dc e2 e4 c with + [ pair l c ⇒ match plus_ex_dc_dc e1 e3 c with + [ pair h c' ⇒ pair … 〈h,l〉 c' ]] = + match plus_ex_dc_dc e4 e2 c with + [ pair l c ⇒ match plus_ex_dc_dc e3 e1 c with + [ pair h c' ⇒ pair … 〈h,l〉 c' ]]); + nrewrite > (symmetric_plusex_dc_dc e4 e2 c); + ncases (plus_ex_dc_dc e2 e4 c); + #e5; #c1; + nchange with ( + match plus_ex_dc_dc e1 e3 c1 with + [ pair h c' ⇒ pair … 〈h,e5〉 c' ] = + match plus_ex_dc_dc e3 e1 c1 with + [ pair h c' ⇒ pair … 〈h,e5〉 c' ]); + nrewrite > (symmetric_plusex_dc_dc e1 e3 c1); + napply refl_eq. +nqed. + +nlemma symmetric_plusb8_dc_d : ∀b1,b2,c.plus_b8_dc_d b1 b2 c = plus_b8_dc_d b2 b1 c. + #b1; #b2; #c; + nelim b1; + #e1; #e2; + nelim b2; + #e3; #e4; + nchange with ( + match plus_ex_dc_dc e2 e4 c with + [ pair l c ⇒ 〈plus_ex_dc_d e1 e3 c,l〉 ] = + match plus_ex_dc_dc e4 e2 c with + [ pair l c ⇒ 〈plus_ex_dc_d e3 e1 c,l〉 ]); + nrewrite > (symmetric_plusex_dc_dc e4 e2 c); + ncases (plus_ex_dc_dc e2 e4 c); + #e5; #c1; + nchange with (〈plus_ex_dc_d e1 e3 c1,e5〉 = 〈plus_ex_dc_d e3 e1 c1,e5〉); + nrewrite > (symmetric_plusex_dc_d e1 e3 c1); + napply refl_eq. +nqed. + +nlemma symmetric_plusb8_dc_c : ∀b1,b2,c.plus_b8_dc_c b1 b2 c = plus_b8_dc_c b2 b1 c. + #b1; #b2; #c; + nelim b1; + #e1; #e2; + nelim b2; + #e3; #e4; + nchange with ( + plus_ex_dc_c e1 e3 (plus_ex_dc_c e2 e4 c) = + plus_ex_dc_c e3 e1 (plus_ex_dc_c e4 e2 c)); + nrewrite > (symmetric_plusex_dc_c e4 e2 c); + nrewrite > (symmetric_plusex_dc_c e3 e1 (plus_ex_dc_c e2 e4 c)); + napply refl_eq. +nqed. + +nlemma symmetric_plusb8_d_dc : ∀b1,b2.plus_b8_d_dc b1 b2 = plus_b8_d_dc b2 b1. + #b1; #b2; + nelim b1; + #e1; #e2; + nelim b2; + #e3; #e4; + nchange with ( + match plus_ex_d_dc e2 e4 with + [ pair l c ⇒ match plus_ex_dc_dc e1 e3 c with + [ pair h c' ⇒ pair … 〈h,l〉 c' ]] = + match plus_ex_d_dc e4 e2 with + [ pair l c ⇒ match plus_ex_dc_dc e3 e1 c with + [ pair h c' ⇒ pair … 〈h,l〉 c' ]]); + nrewrite > (symmetric_plusex_d_dc e4 e2); + ncases (plus_ex_d_dc e2 e4); + #e5; #c; + nchange with ( + match plus_ex_dc_dc e1 e3 c with + [ pair h c' ⇒ pair … 〈h,e5〉 c' ] = + match plus_ex_dc_dc e3 e1 c with + [ pair h c' ⇒ pair … 〈h,e5〉 c' ]); + nrewrite > (symmetric_plusex_dc_dc e1 e3 c); + napply refl_eq. +nqed. + +nlemma symmetric_plusb8_d_d : ∀b1,b2.plus_b8_d_d b1 b2 = plus_b8_d_d b2 b1. + #b1; #b2; + nelim b1; + #e1; #e2; + nelim b2; + #e3; #e4; + nchange with ( + match plus_ex_d_dc e2 e4 with + [ pair l c ⇒ 〈plus_ex_dc_d e1 e3 c,l〉 ] = + match plus_ex_d_dc e4 e2 with + [ pair l c ⇒ 〈plus_ex_dc_d e3 e1 c,l〉 ]); + nrewrite > (symmetric_plusex_d_dc e4 e2); + ncases (plus_ex_d_dc e2 e4); + #e5; #c; + nchange with (〈plus_ex_dc_d e1 e3 c,e5〉 = 〈plus_ex_dc_d e3 e1 c,e5〉); + nrewrite > (symmetric_plusex_dc_d e1 e3 c); + napply refl_eq. +nqed. + +nlemma symmetric_plusb8_d_c : ∀b1,b2.plus_b8_d_c b1 b2 = plus_b8_d_c b2 b1. + #b1; #b2; + nelim b1; + #e1; #e2; + nelim b2; + #e3; #e4; + nchange with ( + plus_ex_dc_c e1 e3 (plus_ex_d_c e2 e4) = + plus_ex_dc_c e3 e1 (plus_ex_d_c e4 e2)); + nrewrite > (symmetric_plusex_d_c e4 e2); + nrewrite > (symmetric_plusex_dc_c e3 e1 (plus_ex_d_c e2 e4)); + napply refl_eq. +nqed. + +nlemma symmetric_mulex : symmetricT exadecim byte8 mul_ex. + #e1; #e2; + nelim e1; + nelim e2; + nnormalize; + napply refl_eq. +nqed. + +nlemma eqb8_to_eq : ∀b1,b2:byte8.(eq_b8 b1 b2 = true) → (b1 = b2). + #b1; #b2; + nelim b1; + nelim b2; + #e1; #e2; #e3; #e4; + nchange in ⊢ (% → ?) with (((eq_ex e3 e1)⊗(eq_ex e4 e2)) = true); + #H; + nrewrite < (eqex_to_eq … (andb_true_true_l … H)); + nrewrite < (eqex_to_eq … (andb_true_true_r … H)); + napply refl_eq. +nqed. + +nlemma eq_to_eqb8 : ∀b1,b2.b1 = b2 → eq_b8 b1 b2 = true. + #b1; #b2; + nelim b1; + nelim b2; + #e1; #e2; #e3; #e4; + #H; + nrewrite < (byte8_destruct_1 … H); + nrewrite < (byte8_destruct_2 … H); + nchange with (((eq_ex e3 e3)⊗(eq_ex e4 e4)) = true); + nrewrite > (eq_to_eqex e3 e3 (refl_eq …)); + nrewrite > (eq_to_eqex e4 e4 (refl_eq …)); + nnormalize; + napply refl_eq. +nqed. diff --git a/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma index a556b2d9e..7d2c418cf 100755 --- a/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma @@ -461,23 +461,3 @@ nlemma eq_to_eqex : ∀e1,e2.e1 = e2 → eq_ex e1 e2 = true. ##| ##*: #H; napply (exadecim_destruct … H) ##] nqed. - -nlemma neqex_to_neq : ∀e1,e2:exadecim.(eq_ex e1 e2 = false) → (e1 ≠ e2). - #e1; #e2; - ncases e1; - ncases e2; - nnormalize; - ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply (bool_destruct … H) - ##| ##*: #H; #H1; napply (exadecim_destruct … H1) - ##] -nqed. - -nlemma neq_to_neqex : ∀e1,e2.e1 ≠ e2 → eq_ex e1 e2 = false. - #e1; #e2; - ncases e1; - ncases e2; - nnormalize; - ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply False_ind; napply (H (refl_eq …)) - ##| ##*: #H; napply refl_eq - ##] -nqed. diff --git a/helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma index 7aa0ff208..2aca1babc 100755 --- a/helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma @@ -121,23 +121,3 @@ nlemma eq_to_eqoct : ∀n1,n2.n1 = n2 → eq_oct n1 n2 = true. ##| ##*: #H; napply (oct_destruct … H) ##] nqed. - -nlemma neqoct_to_neq : ∀n1,n2.eq_oct n1 n2 = false → n1 ≠ n2. - #n1; #n2; - ncases n1; - ncases n2; - nnormalize; - ##[ ##1,10,19,28,37,46,55,64: #H; napply (bool_destruct … H) - ##| ##*: #H; #H1; napply (oct_destruct … H1) - ##] -nqed. - -nlemma neq_to_neqoct : ∀n1,n2.n1 ≠ n2 → eq_oct n1 n2 = false. - #n1; #n2; - ncases n1; - ncases n2; - nnormalize; - ##[ ##1,10,19,28,37,46,55,64: #H; napply False_ind; napply (H (refl_eq …)) - ##| ##*: #H; napply refl_eq - ##] -nqed. diff --git a/helm/software/matita/contribs/ng_assembly/num/quatern_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/quatern_lemmas.ma index 66a75cc53..49b70b81a 100755 --- a/helm/software/matita/contribs/ng_assembly/num/quatern_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/num/quatern_lemmas.ma @@ -93,23 +93,3 @@ nlemma eq_to_eqqu : ∀n1,n2.n1 = n2 → eq_qu n1 n2 = true. ##| ##*: #H; napply (quatern_destruct … H) ##] nqed. - -nlemma neqqu_to_neq : ∀n1,n2.eq_qu n1 n2 = false → n1 ≠ n2. - #n1; #n2; - ncases n1; - ncases n2; - nnormalize; - ##[ ##1,6,11,16: #H; napply (bool_destruct … H) - ##| ##*: #H; #H1; napply (quatern_destruct … H1) - ##] -nqed. - -nlemma neq_to_neqqu : ∀n1,n2.n1 ≠ n2 → eq_qu n1 n2 = false. - #n1; #n2; - ncases n1; - ncases n2; - nnormalize; - ##[ ##1,6,11,16: #H; napply False_ind; napply (H (refl_eq …)) - ##| ##*: #H; napply refl_eq - ##] -nqed. diff --git a/helm/software/matita/contribs/ng_assembly/num/word16.ma b/helm/software/matita/contribs/ng_assembly/num/word16.ma new file mode 100755 index 000000000..b078169d7 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/num/word16.ma @@ -0,0 +1,495 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* ********************************************************************** *) + +include "num/byte8.ma". + +(* **** *) +(* WORD *) +(* **** *) + +nrecord word16 : Type ≝ + { + w16h: byte8; + w16l: byte8 + }. + +(* \langle \rangle *) +notation "〈x:y〉" non associative with precedence 80 + for @{ 'mk_word16 $x $y }. +interpretation "mk_word16" 'mk_word16 x y = (mk_word16 x y). + +(* operatore = *) +ndefinition eq_w16 ≝ λw1,w2.(eq_b8 (w16h w1) (w16h w2)) ⊗ (eq_b8 (w16l w1) (w16l w2)). + +(* operatore < *) +ndefinition lt_w16 ≝ +λw1,w2:word16.match lt_b8 (w16h w1) (w16h w2) with + [ true ⇒ true + | false ⇒ match gt_b8 (w16h w1) (w16h w2) with + [ true ⇒ false + | false ⇒ lt_b8 (w16l w1) (w16l w2) ]]. + +(* operatore ≤ *) +ndefinition le_w16 ≝ λw1,w2:word16.(eq_w16 w1 w2) ⊕ (lt_w16 w1 w2). + +(* operatore > *) +ndefinition gt_w16 ≝ λw1,w2:word16.⊖ (le_w16 w1 w2). + +(* operatore ≥ *) +ndefinition ge_w16 ≝ λw1,w2:word16.⊖ (lt_w16 w1 w2). + +(* operatore and *) +ndefinition and_w16 ≝ +λw1,w2:word16.mk_word16 (and_b8 (w16h w1) (w16h w2)) (and_b8 (w16l w1) (w16l w2)). + +(* operatore or *) +ndefinition or_w16 ≝ +λw1,w2:word16.mk_word16 (or_b8 (w16h w1) (w16h w2)) (or_b8 (w16l w1) (w16l w2)). + +(* operatore xor *) +ndefinition xor_w16 ≝ +λw1,w2:word16.mk_word16 (xor_b8 (w16h w1) (w16h w2)) (xor_b8 (w16l w1) (w16l w2)). + +(* operatore rotazione destra con carry *) +ndefinition rcr_w16 ≝ +λw:word16.λc:bool.match rcr_b8 (w16h w) c with + [ pair wh' c' ⇒ match rcr_b8 (w16l w) c' with + [ pair wl' c'' ⇒ pair … (mk_word16 wh' wl') c'' ]]. + +(* operatore shift destro *) +ndefinition shr_w16 ≝ +λw:word16.match rcr_b8 (w16h w) false with + [ pair wh' c' ⇒ match rcr_b8 (w16l w) c' with + [ pair wl' c'' ⇒ pair … (mk_word16 wh' wl') c'' ]]. + +(* operatore rotazione destra *) +ndefinition ror_w16 ≝ +λw:word16.match rcr_b8 (w16h w) false with + [ pair wh' c' ⇒ match rcr_b8 (w16l w) c' with + [ pair wl' c'' ⇒ match c'' with + [ true ⇒ mk_word16 (or_b8 (mk_byte8 x8 x0) wh') wl' + | false ⇒ mk_word16 wh' wl' ]]]. + +(* operatore rotazione destra n-volte *) +nlet rec ror_w16_n (w:word16) (n:exadecim) (r:rec_exadecim n) on r ≝ + match r with + [ ex_O ⇒ w + | ex_S t n' ⇒ ror_w16_n (ror_w16 w) t n' ]. + +(* operatore rotazione sinistra con carry *) +ndefinition rcl_w16 ≝ +λw:word16.λc:bool.match rcl_b8 (w16l w) c with + [ pair wl' c' ⇒ match rcl_b8 (w16h w) c' with + [ pair wh' c'' ⇒ pair … (mk_word16 wh' wl') c'' ]]. + +(* operatore shift sinistro *) +ndefinition shl_w16 ≝ +λw:word16.match rcl_b8 (w16l w) false with + [ pair wl' c' ⇒ match rcl_b8 (w16h w) c' with + [ pair wh' c'' ⇒ pair … (mk_word16 wh' wl') c'' ]]. + +(* operatore rotazione sinistra *) +ndefinition rol_w16 ≝ +λw:word16.match rcl_b8 (w16l w) false with + [ pair wl' c' ⇒ match rcl_b8 (w16h w) c' with + [ pair wh' c'' ⇒ match c'' with + [ true ⇒ mk_word16 wh' (or_b8 (mk_byte8 x0 x1) wl') + | false ⇒ mk_word16 wh' wl' ]]]. + +(* operatore rotazione sinistra n-volte *) +nlet rec rol_w16_n (w:word16) (n:exadecim) (r:rec_exadecim n) on r ≝ + match r with + [ ex_O ⇒ w + | ex_S t n' ⇒ rol_w16_n (rol_w16 w) t n' ]. + +(* operatore not/complemento a 1 *) +ndefinition not_w16 ≝ +λw:word16.mk_word16 (not_b8 (w16h w)) (not_b8 (w16l w)). + +(* operatore somma con data+carry → data+carry *) +ndefinition plus_w16_dc_dc ≝ +λw1,w2:word16.λc:bool. + match plus_b8_dc_dc (w16l w1) (w16l w2) c with + [ pair l c ⇒ match plus_b8_dc_dc (w16h w1) (w16h w2) c with + [ pair h c' ⇒ pair … 〈h:l〉 c' ]]. + +(* operatore somma con data+carry → data *) +ndefinition plus_w16_dc_d ≝ +λw1,w2:word16.λc:bool. + match plus_b8_dc_dc (w16l w1) (w16l w2) c with + [ pair l c ⇒ 〈plus_b8_dc_d (w16h w1) (w16h w2) c:l〉 ]. + +(* operatore somma con data+carry → c *) +ndefinition plus_w16_dc_c ≝ +λw1,w2:word16.λc:bool. + plus_b8_dc_c (w16h w1) (w16h w2) (plus_b8_dc_c (w16l w1) (w16l w2) c). + +(* operatore somma con data → data+carry *) +ndefinition plus_w16_d_dc ≝ +λw1,w2:word16. + match plus_b8_d_dc (w16l w1) (w16l w2) with + [ pair l c ⇒ match plus_b8_dc_dc (w16h w1) (w16h w2) c with + [ pair h c' ⇒ pair … 〈h:l〉 c' ]]. + +(* operatore somma con data → data *) +ndefinition plus_w16_d_d ≝ +λw1,w2:word16. + match plus_b8_d_dc (w16l w1) (w16l w2) with + [ pair l c ⇒ 〈plus_b8_dc_d (w16h w1) (w16h w2) c:l〉 ]. + +(* operatore somma con data → c *) +ndefinition plus_w16_d_c ≝ +λw1,w2:word16. + plus_b8_dc_c (w16h w1) (w16h w2) (plus_b8_d_c (w16l w1) (w16l w2)). + +(* operatore Most Significant Bit *) +ndefinition MSB_w16 ≝ λw:word16.eq_ex x8 (and_ex x8 (b8h (w16h w))). + +(* operatore predecessore *) +ndefinition pred_w16 ≝ +λw:word16.match eq_b8 (w16l w) (mk_byte8 x0 x0) with + [ true ⇒ mk_word16 (pred_b8 (w16h w)) (pred_b8 (w16l w)) + | false ⇒ mk_word16 (w16h w) (pred_b8 (w16l w)) ]. + +(* operatore successore *) +ndefinition succ_w16 ≝ +λw:word16.match eq_b8 (w16l w) (mk_byte8 xF xF) with + [ true ⇒ mk_word16 (succ_b8 (w16h w)) (succ_b8 (w16l w)) + | false ⇒ mk_word16 (w16h w) (succ_b8 (w16l w)) ]. + +(* operatore neg/complemento a 2 *) +ndefinition compl_w16 ≝ +λw:word16.match MSB_w16 w with + [ true ⇒ succ_w16 (not_w16 w) + | false ⇒ not_w16 (pred_w16 w) ]. + +(* + operatore moltiplicazione senza segno: b*b=[0x0000,0xFE01] + ... in pratica (〈a,b〉*〈c,d〉) = (a*c)<<8+(a*d)<<4+(b*c)<<4+(b*d) +*) +ndefinition mul_b8 ≝ +λb1,b2:byte8.match b1 with +[ mk_byte8 b1h b1l ⇒ match b2 with +[ mk_byte8 b2h b2l ⇒ match mul_ex b1l b2l with +[ mk_byte8 t1_h t1_l ⇒ match mul_ex b1h b2l with +[ mk_byte8 t2_h t2_l ⇒ match mul_ex b2h b1l with +[ mk_byte8 t3_h t3_l ⇒ match mul_ex b1h b2h with +[ mk_byte8 t4_h t4_l ⇒ + plus_w16_d_d + (plus_w16_d_d + (plus_w16_d_d 〈〈x0,t3_h〉:〈t3_l,x0〉〉 〈〈x0,t2_h〉:〈t2_l,x0〉〉) 〈〈t4_h,t4_l〉:〈x0,x0〉〉)〈〈x0,x0〉:〈t1_h,t1_l〉〉 +]]]]]]. + +(* divisione senza segno (secondo la logica delle ALU): (quoziente resto) overflow *) +nlet rec div_b8_aux (divd:word16) (divs:word16) (molt:byte8) (q:byte8) (c:oct) (rc:rec_oct c) on rc ≝ + let w' ≝ plus_w16_d_d divd (compl_w16 divs) in + match rc with + [ oc_O ⇒ match le_w16 divs divd with + [ true ⇒ triple … (or_b8 molt q) (w16l w') (⊖ (eq_b8 (w16h w') 〈x0,x0〉)) + | false ⇒ triple … q (w16l divd) (⊖ (eq_b8 (w16h divd) 〈x0,x0〉)) ] + | oc_S t c' ⇒ match le_w16 divs divd with + [ true ⇒ div_b8_aux w' (ror_w16 divs) (ror_b8 molt) (or_b8 molt q) t c' + | false ⇒ div_b8_aux divd (ror_w16 divs) (ror_b8 molt) q t c' ]]. + +ndefinition div_b8 ≝ +λw:word16.λb:byte8.match eq_b8 b 〈x0,x0〉 with +(* + la combinazione n/0 e' illegale, segnala solo overflow senza dare risultato +*) + [ true ⇒ triple … 〈xF,xF〉 (w16l w) true + | false ⇒ match eq_w16 w 〈〈x0,x0〉:〈x0,x0〉〉 with +(* 0 diviso qualsiasi cosa diverso da 0 da' q=0 r=0 o=false *) + [ true ⇒ triple … 〈x0,x0〉 〈x0,x0〉 false +(* 1) e' una divisione sensata che produrra' overflow/risultato *) +(* 2) parametri: dividendo, divisore, moltiplicatore, quoziente, contatore *) +(* 3) ad ogni ciclo il divisore e il moltiplicatore vengono scalati di 1 a dx *) +(* 4) il moltiplicatore e' la quantita' aggiunta al quoziente se il divisore *) +(* puo' essere sottratto al dividendo *) + | false ⇒ div_b8_aux w (rol_w16_n 〈〈x0,x0〉:b〉 ? (ex_to_recex x7)) 〈x8,x0〉 〈x0,x0〉 ? (oct_to_recoct o7) ]]. + +(* operatore x in [inf,sup] *) +ndefinition inrange_w16 ≝ +λx,inf,sup:word16.(le_w16 inf sup) ⊗ (ge_w16 x inf) ⊗ (le_w16 x sup). + +(* iteratore sulle word *) +ndefinition forall_w16 ≝ + λP. + forall_b8 (λbh. + forall_b8 (λbl. + P (mk_word16 bh bl ))). + +(* word16 ricorsive *) +ninductive rec_word16 : word16 → Type ≝ + w16_O : rec_word16 〈〈x0,x0〉:〈x0,x0〉〉 +| w16_S : ∀n.rec_word16 n → rec_word16 (succ_w16 n). + +(* word16 → word16 ricorsive *) +ndefinition w16_to_recw16_aux1_1 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x1,x0〉〉 ≝ +λn.λrecw:rec_word16 〈n:〈x0,x0〉〉. + w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? ( + w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? recw + ))))))))))))))). + +ndefinition w16_to_recw16_aux1_2 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x2,x0〉〉 ≝ +λn.λrecw:rec_word16 〈n:〈x0,x0〉〉. + w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? ( + w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_1 ? recw) + ))))))))))))))). + +ndefinition w16_to_recw16_aux1_3 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x3,x0〉〉 ≝ +λn.λrecw:rec_word16 〈n:〈x0,x0〉〉. + w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? ( + w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_2 ? recw) + ))))))))))))))). + +ndefinition w16_to_recw16_aux1_4 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x4,x0〉〉 ≝ +λn.λrecw:rec_word16 〈n:〈x0,x0〉〉. + w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? ( + w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_3 ? recw) + ))))))))))))))). + +ndefinition w16_to_recw16_aux1_5 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x5,x0〉〉 ≝ +λn.λrecw:rec_word16 〈n:〈x0,x0〉〉. + w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? ( + w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_4 ? recw) + ))))))))))))))). + +ndefinition w16_to_recw16_aux1_6 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x6,x0〉〉 ≝ +λn.λrecw:rec_word16 〈n:〈x0,x0〉〉. + w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? ( + w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_5 ? recw) + ))))))))))))))). + +ndefinition w16_to_recw16_aux1_7 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x7,x0〉〉 ≝ +λn.λrecw:rec_word16 〈n:〈x0,x0〉〉. + w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? ( + w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_6 ? recw) + ))))))))))))))). + +ndefinition w16_to_recw16_aux1_8 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x8,x0〉〉 ≝ +λn.λrecw:rec_word16 〈n:〈x0,x0〉〉. + w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? ( + w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_7 ? recw) + ))))))))))))))). + +ndefinition w16_to_recw16_aux1_9 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x9,x0〉〉 ≝ +λn.λrecw:rec_word16 〈n:〈x0,x0〉〉. + w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? ( + w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_8 ? recw) + ))))))))))))))). + +ndefinition w16_to_recw16_aux1_10 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈xA,x0〉〉 ≝ +λn.λrecw:rec_word16 〈n:〈x0,x0〉〉. + w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? ( + w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_9 ? recw) + ))))))))))))))). + +ndefinition w16_to_recw16_aux1_11 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈xB,x0〉〉 ≝ +λn.λrecw:rec_word16 〈n:〈x0,x0〉〉. + w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? ( + w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_10 ? recw) + ))))))))))))))). + +ndefinition w16_to_recw16_aux1_12 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈xC,x0〉〉 ≝ +λn.λrecw:rec_word16 〈n:〈x0,x0〉〉. + w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? ( + w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_11 ? recw) + ))))))))))))))). + +ndefinition w16_to_recw16_aux1_13 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈xD,x0〉〉 ≝ +λn.λrecw:rec_word16 〈n:〈x0,x0〉〉. + w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? ( + w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_12 ? recw) + ))))))))))))))). + +ndefinition w16_to_recw16_aux1_14 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈xE,x0〉〉 ≝ +λn.λrecw:rec_word16 〈n:〈x0,x0〉〉. + w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? ( + w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_13 ? recw) + ))))))))))))))). + +ndefinition w16_to_recw16_aux1_15 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈xF,x0〉〉 ≝ +λn.λrecw:rec_word16 〈n:〈x0,x0〉〉. + w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? ( + w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_14 ? recw) + ))))))))))))))). + +ndefinition w16_to_recw16_aux1 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈(succ_b8 n):〈x0,x0〉〉 ≝ +λn.λrecw:rec_word16 〈n:〈x0,x0〉〉. + w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? ( + w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_15 ? recw) + ))))))))))))))). + +(* ... cifra byte superiore *) +nlet rec w16_to_recw16_aux2 (n:byte8) (r:rec_byte8 n) on r ≝ + match r return λx.λy:rec_byte8 x.rec_word16 〈x:〈x0,x0〉〉 with + [ b8_O ⇒ w16_O + | b8_S t n' ⇒ w16_to_recw16_aux1 ? (w16_to_recw16_aux2 t n') + ]. + +(* ... cifra esadecimale n.2 *) +ndefinition w16_to_recw16_aux3 ≝ +λb,n.λrecw:rec_word16 〈b:〈x0,x0〉〉. + match n return λx.rec_word16 〈b:〈x,x0〉〉 with + [ x0 ⇒ recw + | x1 ⇒ w16_to_recw16_aux1_1 ? recw + | x2 ⇒ w16_to_recw16_aux1_2 ? recw + | x3 ⇒ w16_to_recw16_aux1_3 ? recw + | x4 ⇒ w16_to_recw16_aux1_4 ? recw + | x5 ⇒ w16_to_recw16_aux1_5 ? recw + | x6 ⇒ w16_to_recw16_aux1_6 ? recw + | x7 ⇒ w16_to_recw16_aux1_7 ? recw + | x8 ⇒ w16_to_recw16_aux1_8 ? recw + | x9 ⇒ w16_to_recw16_aux1_9 ? recw + | xA ⇒ w16_to_recw16_aux1_10 ? recw + | xB ⇒ w16_to_recw16_aux1_11 ? recw + | xC ⇒ w16_to_recw16_aux1_12 ? recw + | xD ⇒ w16_to_recw16_aux1_13 ? recw + | xE ⇒ w16_to_recw16_aux1_14 ? recw + | xF ⇒ w16_to_recw16_aux1_15 ? recw + ]. + +nlemma w16_to_recw16_aux4_1 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x1〉〉. + #n; #e; + (* non funziona nelim e *) + #H; + nelim e in H:(%) ⊢ %; + #input; napply (w16_S ? input). +nqed. + +nlemma w16_to_recw16_aux4_2 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x2〉〉. + #n; #e; #H; + nelim e in H:(%) ⊢ %; + #input; napply (w16_S ? (w16_to_recw16_aux4_1 … input)). +nqed. + +nlemma w16_to_recw16_aux4_3 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x3〉〉. + #n; #e; #H; + nelim e in H:(%) ⊢ %; + #input; napply (w16_S ? (w16_to_recw16_aux4_2 … input)). +nqed. + +nlemma w16_to_recw16_aux4_4 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x4〉〉. + #n; #e; #H; + nelim e in H:(%) ⊢ %; + #input; napply (w16_S ? (w16_to_recw16_aux4_3 … input)). +nqed. + +nlemma w16_to_recw16_aux4_5 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x5〉〉. + #n; #e; #H; + nelim e in H:(%) ⊢ %; + #input; napply (w16_S ? (w16_to_recw16_aux4_4 … input)). +nqed. + +nlemma w16_to_recw16_aux4_6 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x6〉〉. + #n; #e; #H; + nelim e in H:(%) ⊢ %; + #input; napply (w16_S ? (w16_to_recw16_aux4_5 … input)). +nqed. + +nlemma w16_to_recw16_aux4_7 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x7〉〉. + #n; #e; #H; + nelim e in H:(%) ⊢ %; + #input; napply (w16_S ? (w16_to_recw16_aux4_6 … input)). +nqed. + +nlemma w16_to_recw16_aux4_8 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x8〉〉. + #n; #e; #H; + nelim e in H:(%) ⊢ %; + #input; napply (w16_S ? (w16_to_recw16_aux4_7 … input)). +nqed. + +nlemma w16_to_recw16_aux4_9 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x9〉〉. + #n; #e; #H; + nelim e in H:(%) ⊢ %; + #input; napply (w16_S ? (w16_to_recw16_aux4_8 … input)). +nqed. + +nlemma w16_to_recw16_aux4_10 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,xA〉〉. + #n; #e; #H; + nelim e in H:(%) ⊢ %; + #input; napply (w16_S ? (w16_to_recw16_aux4_9 … input)). +nqed. + +nlemma w16_to_recw16_aux4_11 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,xB〉〉. + #n; #e; #H; + nelim e in H:(%) ⊢ %; + #input; napply (w16_S ? (w16_to_recw16_aux4_10 … input)). +nqed. + +nlemma w16_to_recw16_aux4_12 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,xC〉〉. + #n; #e; #H; + nelim e in H:(%) ⊢ %; + #input; napply (w16_S ? (w16_to_recw16_aux4_11 … input)). +nqed. + +nlemma w16_to_recw16_aux4_13 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,xD〉〉. + #n; #e; #H; + nelim e in H:(%) ⊢ %; + #input; napply (w16_S ? (w16_to_recw16_aux4_12 … input)). +nqed. + +nlemma w16_to_recw16_aux4_14 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,xE〉〉. + #n; #e; #H; + nelim e in H:(%) ⊢ %; + #input; napply (w16_S ? (w16_to_recw16_aux4_13 … input)). +nqed. + +nlemma w16_to_recw16_aux4_15 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,xF〉〉. + #n; #e; #H; + nelim e in H:(%) ⊢ %; + #input; napply (w16_S ? (w16_to_recw16_aux4_14 … input)). +nqed. + +(* ... cifra esadecimale n.1 *) +ndefinition w16_to_recw16_aux4 ≝ +λb,e,n.λrecw:rec_word16 〈b:〈e,x0〉〉. + match n return λx.rec_word16 〈b:〈e,x〉〉 with + [ x0 ⇒ recw + | x1 ⇒ w16_to_recw16_aux4_1 … recw + | x2 ⇒ w16_to_recw16_aux4_2 … recw + | x3 ⇒ w16_to_recw16_aux4_3 … recw + | x4 ⇒ w16_to_recw16_aux4_4 … recw + | x5 ⇒ w16_to_recw16_aux4_5 … recw + | x6 ⇒ w16_to_recw16_aux4_6 … recw + | x7 ⇒ w16_to_recw16_aux4_7 … recw + | x8 ⇒ w16_to_recw16_aux4_8 … recw + | x9 ⇒ w16_to_recw16_aux4_9 … recw + | xA ⇒ w16_to_recw16_aux4_10 … recw + | xB ⇒ w16_to_recw16_aux4_11 … recw + | xC ⇒ w16_to_recw16_aux4_12 … recw + | xD ⇒ w16_to_recw16_aux4_13 … recw + | xE ⇒ w16_to_recw16_aux4_14 … recw + | xF ⇒ w16_to_recw16_aux4_15 … recw + ]. + +nlemma w16_to_recw16_aux5 : ∀b.rec_byte8 (〈b8h b,b8l b〉) → rec_byte8 b. + #b; nelim b; #e1; #e2; nnormalize; #input; napply input. nqed. + +ndefinition w16_to_recw16 ≝ +λn.w16_to_recw16_aux4 (w16h n) (b8h (w16l n)) (b8l (w16l n)) + (w16_to_recw16_aux3 (w16h n) (b8h (w16l n)) (w16_to_recw16_aux2 (w16h n) ?)). + nelim n; #b1; #b2; + nchange with (rec_byte8 b1); + napply (w16_to_recw16_aux5 b1); + napply (b8_to_recb8 b1). +nqed. diff --git a/helm/software/matita/contribs/ng_assembly/num/word16_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/word16_lemmas.ma new file mode 100755 index 000000000..3e53841ae --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/num/word16_lemmas.ma @@ -0,0 +1,327 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* ********************************************************************** *) + +include "num/word16.ma". +include "num/byte8_lemmas.ma". + +(* **** *) +(* WORD *) +(* **** *) + +nlemma word16_destruct_1 : +∀x1,x2,y1,y2. + mk_word16 x1 y1 = mk_word16 x2 y2 → x1 = x2. + #x1; #x2; #y1; #y2; #H; + nchange with (match mk_word16 x2 y2 with [ mk_word16 a _ ⇒ x1 = a ]); + nrewrite < H; + nnormalize; + napply refl_eq. +nqed. + +nlemma word16_destruct_2 : +∀x1,x2,y1,y2. + mk_word16 x1 y1 = mk_word16 x2 y2 → y1 = y2. + #x1; #x2; #y1; #y2; #H; + nchange with (match mk_word16 x2 y2 with [ mk_word16 _ b ⇒ y1 = b ]); + nrewrite < H; + nnormalize; + napply refl_eq. +nqed. + +nlemma symmetric_eqw16 : symmetricT word16 bool eq_w16. + #w1; #w2; + nelim w1; + nelim w2; + #b1; #b2; #b3; #b4; + nchange with (((eq_b8 b3 b1)⊗(eq_b8 b4 b2)) = ((eq_b8 b1 b3)⊗(eq_b8 b2 b4))); + nrewrite > (symmetric_eqb8 b1 b3); + nrewrite > (symmetric_eqb8 b2 b4); + napply refl_eq. +nqed. + +nlemma symmetric_andw16 : symmetricT word16 word16 and_w16. + #w1; #w2; + nelim w1; + nelim w2; + #b1; #b2; #b3; #b4; + nchange with ((mk_word16 (and_b8 b3 b1) (and_b8 b4 b2)) = (mk_word16 (and_b8 b1 b3) (and_b8 b2 b4))); + nrewrite > (symmetric_andb8 b1 b3); + nrewrite > (symmetric_andb8 b2 b4); + napply refl_eq. +nqed. + +nlemma associative_andw16 : ∀w1,w2,w3.(and_w16 (and_w16 w1 w2) w3) = (and_w16 w1 (and_w16 w2 w3)). + #w1; #w2; #w3; + nelim w1; + #b1; #b2; + nelim w2; + #b3; #b4; + nelim w3; + #b5; #b6; + nchange with (mk_word16 (and_b8 (and_b8 b1 b3) b5) (and_b8 (and_b8 b2 b4) b6) = + mk_word16 (and_b8 b1 (and_b8 b3 b5)) (and_b8 b2 (and_b8 b4 b6))); + nrewrite < (associative_andb8 b1 b3 b5); + nrewrite < (associative_andb8 b2 b4 b6); + napply refl_eq. +nqed. + +nlemma symmetric_orw16 : symmetricT word16 word16 or_w16. + #w1; #w2; + nelim w1; + nelim w2; + #b1; #b2; #b3; #b4; + nchange with ((mk_word16 (or_b8 b3 b1) (or_b8 b4 b2)) = (mk_word16 (or_b8 b1 b3) (or_b8 b2 b4))); + nrewrite > (symmetric_orb8 b1 b3); + nrewrite > (symmetric_orb8 b2 b4); + napply refl_eq. +nqed. + +nlemma associative_orw16 : ∀w1,w2,w3.(or_w16 (or_w16 w1 w2) w3) = (or_w16 w1 (or_w16 w2 w3)). + #w1; #w2; #w3; + nelim w1; + #b1; #b2; + nelim w2; + #b3; #b4; + nelim w3; + #b5; #b6; + nchange with (mk_word16 (or_b8 (or_b8 b1 b3) b5) (or_b8 (or_b8 b2 b4) b6) = + mk_word16 (or_b8 b1 (or_b8 b3 b5)) (or_b8 b2 (or_b8 b4 b6))); + nrewrite < (associative_orb8 b1 b3 b5); + nrewrite < (associative_orb8 b2 b4 b6); + napply refl_eq. +nqed. + +nlemma symmetric_xorw16 : symmetricT word16 word16 xor_w16. + #w1; #w2; + nelim w1; + nelim w2; + #b1; #b2; #b3; #b4; + nchange with ((mk_word16 (xor_b8 b3 b1) (xor_b8 b4 b2)) = (mk_word16 (xor_b8 b1 b3) (xor_b8 b2 b4))); + nrewrite > (symmetric_xorb8 b1 b3); + nrewrite > (symmetric_xorb8 b2 b4); + napply refl_eq. +nqed. + +nlemma associative_xorw16 : ∀w1,w2,w3.(xor_w16 (xor_w16 w1 w2) w3) = (xor_w16 w1 (xor_w16 w2 w3)). + #w1; #w2; #w3; + nelim w1; + #b1; #b2; + nelim w2; + #b3; #b4; + nelim w3; + #b5; #b6; + nchange with (mk_word16 (xor_b8 (xor_b8 b1 b3) b5) (xor_b8 (xor_b8 b2 b4) b6) = + mk_word16 (xor_b8 b1 (xor_b8 b3 b5)) (xor_b8 b2 (xor_b8 b4 b6))); + nrewrite < (associative_xorb8 b1 b3 b5); + nrewrite < (associative_xorb8 b2 b4 b6); + napply refl_eq. +nqed. + +nlemma symmetric_plusw16_dc_dc : ∀w1,w2,c.plus_w16_dc_dc w1 w2 c = plus_w16_dc_dc w2 w1 c. + #w1; #w2; #c; + nelim w1; + #b1; #b2; + nelim w2; + #b3; #b4; + nchange with ( + match plus_b8_dc_dc b2 b4 c with + [ pair l c ⇒ match plus_b8_dc_dc b1 b3 c with + [ pair h c' ⇒ pair … 〈h:l〉 c' ]] = + match plus_b8_dc_dc b4 b2 c with + [ pair l c ⇒ match plus_b8_dc_dc b3 b1 c with + [ pair h c' ⇒ pair … 〈h:l〉 c' ]]); + nrewrite > (symmetric_plusb8_dc_dc b4 b2 c); + ncases (plus_b8_dc_dc b2 b4 c); + #b5; #c1; + nchange with ( + match plus_b8_dc_dc b1 b3 c1 with + [ pair h c' ⇒ pair … 〈h:b5〉 c' ] = + match plus_b8_dc_dc b3 b1 c1 with + [ pair h c' ⇒ pair … 〈h:b5〉 c' ]); + nrewrite > (symmetric_plusb8_dc_dc b1 b3 c1); + napply refl_eq. +nqed. + +nlemma symmetric_plusw16_dc_d : ∀w1,w2,c.plus_w16_dc_d w1 w2 c = plus_w16_dc_d w2 w1 c. + #w1; #w2; #c; + nelim w1; + #b1; #b2; + nelim w2; + #b3; #b4; + nchange with ( + match plus_b8_dc_dc b2 b4 c with + [ pair l c ⇒ 〈plus_b8_dc_d b1 b3 c:l〉 ] = + match plus_b8_dc_dc b4 b2 c with + [ pair l c ⇒ 〈plus_b8_dc_d b3 b1 c:l〉 ]); + nrewrite > (symmetric_plusb8_dc_dc b4 b2 c); + ncases (plus_b8_dc_dc b2 b4 c); + #b5; #c1; + nchange with (〈plus_b8_dc_d b1 b3 c1:b5〉 = 〈plus_b8_dc_d b3 b1 c1:b5〉); + nrewrite > (symmetric_plusb8_dc_d b1 b3 c1); + napply refl_eq. +nqed. + +nlemma symmetric_plusw16_dc_c : ∀w1,w2,c.plus_w16_dc_c w1 w2 c = plus_w16_dc_c w2 w1 c. + #w1; #w2; #c; + nelim w1; + #b1; #b2; + nelim w2; + #b3; #b4; + nchange with ( + plus_b8_dc_c b1 b3 (plus_b8_dc_c b2 b4 c) = + plus_b8_dc_c b3 b1 (plus_b8_dc_c b4 b2 c)); + nrewrite > (symmetric_plusb8_dc_c b4 b2 c); + nrewrite > (symmetric_plusb8_dc_c b3 b1 (plus_b8_dc_c b2 b4 c)); + napply refl_eq. +nqed. + +nlemma symmetric_plusw16_d_dc : ∀w1,w2.plus_w16_d_dc w1 w2 = plus_w16_d_dc w2 w1. + #w1; #w2; + nelim w1; + #b1; #b2; + nelim w2; + #b3; #b4; + nchange with ( + match plus_b8_d_dc b2 b4 with + [ pair l c ⇒ match plus_b8_dc_dc b1 b3 c with + [ pair h c' ⇒ pair … 〈h:l〉 c' ]] = + match plus_b8_d_dc b4 b2 with + [ pair l c ⇒ match plus_b8_dc_dc b3 b1 c with + [ pair h c' ⇒ pair … 〈h:l〉 c' ]]); + nrewrite > (symmetric_plusb8_d_dc b4 b2); + ncases (plus_b8_d_dc b2 b4); + #b5; #c; + nchange with ( + match plus_b8_dc_dc b1 b3 c with + [ pair h c' ⇒ pair … 〈h:b5〉 c' ] = + match plus_b8_dc_dc b3 b1 c with + [ pair h c' ⇒ pair … 〈h:b5〉 c' ]); + nrewrite > (symmetric_plusb8_dc_dc b1 b3 c); + napply refl_eq. +nqed. + +nlemma symmetric_plusw16_d_d : ∀w1,w2.plus_w16_d_d w1 w2 = plus_w16_d_d w2 w1. + #w1; #w2; + nelim w1; + #b1; #b2; + nelim w2; + #b3; #b4; + nchange with ( + match plus_b8_d_dc b2 b4 with + [ pair l c ⇒ 〈plus_b8_dc_d b1 b3 c:l〉 ] = + match plus_b8_d_dc b4 b2 with + [ pair l c ⇒ 〈plus_b8_dc_d b3 b1 c:l〉 ]); + nrewrite > (symmetric_plusb8_d_dc b4 b2); + ncases (plus_b8_d_dc b2 b4); + #b5; #c; + nchange with (〈plus_b8_dc_d b1 b3 c:b5〉 = 〈plus_b8_dc_d b3 b1 c:b5〉); + nrewrite > (symmetric_plusb8_dc_d b1 b3 c); + napply refl_eq. +nqed. + +nlemma symmetric_plusw16_d_c : ∀w1,w2.plus_w16_d_c w1 w2 = plus_w16_d_c w2 w1. + #w1; #w2; + nelim w1; + #b1; #b2; + nelim w2; + #b3; #b4; + nchange with ( + plus_b8_dc_c b1 b3 (plus_b8_d_c b2 b4) = + plus_b8_dc_c b3 b1 (plus_b8_d_c b4 b2)); + nrewrite > (symmetric_plusb8_d_c b4 b2); + nrewrite > (symmetric_plusb8_dc_c b3 b1 (plus_b8_d_c b2 b4)); + napply refl_eq. +nqed. + +nlemma symmetric_mulb8 : symmetricT byte8 word16 mul_b8. + #b1; #b2; + nelim b1; + #e1; #e2; + nelim b2; + #e3; #e4; + nchange with (match mul_ex e2 e4 with + [ mk_byte8 t1_h t1_l ⇒ match mul_ex e1 e4 with + [ mk_byte8 t2_h t2_l ⇒ match mul_ex e3 e2 with + [ mk_byte8 t3_h t3_l ⇒ match mul_ex e1 e3 with + [ mk_byte8 t4_h t4_l ⇒ plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,t3_h〉:〈t3_l,x0〉〉 〈〈x0,t2_h〉:〈t2_l,x0〉〉) 〈〈t4_h,t4_l〉:〈x0,x0〉〉)〈〈x0,x0〉:〈t1_h,t1_l〉〉 + ]]]] = match mul_ex e4 e2 with + [ mk_byte8 t1_h t1_l ⇒ match mul_ex e3 e2 with + [ mk_byte8 t2_h t2_l ⇒ match mul_ex e1 e4 with + [ mk_byte8 t3_h t3_l ⇒ match mul_ex e3 e1 with + [ mk_byte8 t4_h t4_l ⇒ plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,t3_h〉:〈t3_l,x0〉〉 〈〈x0,t2_h〉:〈t2_l,x0〉〉) 〈〈t4_h,t4_l〉:〈x0,x0〉〉)〈〈x0,x0〉:〈t1_h,t1_l〉〉 + ]]]]); + nrewrite < (symmetric_mulex e2 e4); + ncases (mul_ex e2 e4); + #e5; #e6; + nchange with (match mul_ex e1 e4 with + [ mk_byte8 t2_h t2_l ⇒ match mul_ex e3 e2 with + [ mk_byte8 t3_h t3_l ⇒ match mul_ex e1 e3 with + [ mk_byte8 t4_h t4_l ⇒ plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,t3_h〉:〈t3_l,x0〉〉 〈〈x0,t2_h〉:〈t2_l,x0〉〉) 〈〈t4_h,t4_l〉:〈x0,x0〉〉)〈〈x0,x0〉:〈e5,e6〉〉 + ]]] = match mul_ex e3 e2 with + [ mk_byte8 t2_h t2_l ⇒ match mul_ex e1 e4 with + [ mk_byte8 t3_h t3_l ⇒ match mul_ex e3 e1 with + [ mk_byte8 t4_h t4_l ⇒ plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,t3_h〉:〈t3_l,x0〉〉 〈〈x0,t2_h〉:〈t2_l,x0〉〉) 〈〈t4_h,t4_l〉:〈x0,x0〉〉)〈〈x0,x0〉:〈e5,e6〉〉 + ]]]); + ncases (mul_ex e3 e2); + #e7; #e8; + ncases (mul_ex e1 e4); + #e9; #e10; + nchange with (match mul_ex e1 e3 with + [ mk_byte8 t4_h t4_l ⇒ plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,e7〉:〈e8,x0〉〉 〈〈x0,e9〉:〈e10,x0〉〉) 〈〈t4_h,t4_l〉:〈x0,x0〉〉)〈〈x0,x0〉:〈e5,e6〉〉 + ] = match mul_ex e3 e1 with + [ mk_byte8 t4_h t4_l ⇒ plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,e9〉:〈e10,x0〉〉 〈〈x0,e7〉:〈e8,x0〉〉) 〈〈t4_h,t4_l〉:〈x0,x0〉〉)〈〈x0,x0〉:〈e5,e6〉〉 + ]); + nrewrite < (symmetric_mulex e1 e3); + ncases (mul_ex e1 e3); + #e11; #e12; + nchange with ((plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,e7〉:〈e8,x0〉〉 〈〈x0,e9〉:〈e10,x0〉〉) 〈〈e11,e12〉:〈x0,x0〉〉)〈〈x0,x0〉:〈e5,e6〉〉) = + (plus_w16_d_d (plus_w16_d_d (plus_w16_d_d 〈〈x0,e9〉:〈e10,x0〉〉 〈〈x0,e7〉:〈e8,x0〉〉) 〈〈e11,e12〉:〈x0,x0〉〉)〈〈x0,x0〉:〈e5,e6〉〉)); + nrewrite > (symmetric_plusw16_d_d 〈〈x0,e7〉:〈e8,x0〉〉 〈〈x0,e9〉:〈e10,x0〉〉); + napply refl_eq. +nqed. + +nlemma eqw16_to_eq : ∀w1,w2:word16.(eq_w16 w1 w2 = true) → (w1 = w2). + #w1; #w2; + nelim w1; + nelim w2; + #b1; #b2; #b3; #b4; + nchange in ⊢ (% → ?) with (((eq_b8 b3 b1)⊗(eq_b8 b4 b2)) = true); + #H; + nrewrite < (eqb8_to_eq … (andb_true_true_l … H)); + nrewrite < (eqb8_to_eq … (andb_true_true_r … H)); + napply refl_eq. +nqed. + +nlemma eq_to_eqw16 : ∀w1,w2.w1 = w2 → eq_w16 w1 w2 = true. + #w1; #w2; + nelim w1; + nelim w2; + #b1; #b2; #b3; #b4; + #H; + nrewrite < (word16_destruct_1 … H); + nrewrite < (word16_destruct_2 … H); + nchange with (((eq_b8 b3 b3)⊗(eq_b8 b4 b4)) = true); + nrewrite > (eq_to_eqb8 b3 b3 (refl_eq …)); + nrewrite > (eq_to_eqb8 b4 b4 (refl_eq …)); + nnormalize; + napply refl_eq. +nqed. diff --git a/helm/software/matita/contribs/ng_assembly/num/word32.ma b/helm/software/matita/contribs/ng_assembly/num/word32.ma new file mode 100755 index 000000000..091d0f73c --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/num/word32.ma @@ -0,0 +1,238 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* ********************************************************************** *) + +include "num/word16.ma". + +(* ***** *) +(* DWORD *) +(* ***** *) + +nrecord word32 : Type ≝ + { + w32h: word16; + w32l: word16 + }. + +(* \langle \rangle *) +notation "〈x.y〉" non associative with precedence 80 + for @{ 'mk_word32 $x $y }. +interpretation "mk_word32" 'mk_word32 x y = (mk_word32 x y). + +(* operatore = *) +ndefinition eq_w32 ≝ λdw1,dw2.(eq_w16 (w32h dw1) (w32h dw2)) ⊗ (eq_w16 (w32l dw1) (w32l dw2)). + +(* operatore < *) +ndefinition lt_w32 ≝ +λdw1,dw2:word32.match lt_w16 (w32h dw1) (w32h dw2) with + [ true ⇒ true + | false ⇒ match gt_w16 (w32h dw1) (w32h dw2) with + [ true ⇒ false + | false ⇒ lt_w16 (w32l dw1) (w32l dw2) ]]. + +(* operatore ≤ *) +ndefinition le_w32 ≝ λdw1,dw2:word32.(eq_w32 dw1 dw2) ⊕ (lt_w32 dw1 dw2). + +(* operatore > *) +ndefinition gt_w32 ≝ λdw1,dw2:word32.⊖ (le_w32 dw1 dw2). + +(* operatore ≥ *) +ndefinition ge_w32 ≝ λdw1,dw2:word32.⊖ (lt_w32 dw1 dw2). + +(* operatore and *) +ndefinition and_w32 ≝ +λdw1,dw2:word32.mk_word32 (and_w16 (w32h dw1) (w32h dw2)) (and_w16 (w32l dw1) (w32l dw2)). + +(* operatore or *) +ndefinition or_w32 ≝ +λdw1,dw2:word32.mk_word32 (or_w16 (w32h dw1) (w32h dw2)) (or_w16 (w32l dw1) (w32l dw2)). + +(* operatore xor *) +ndefinition xor_w32 ≝ +λdw1,dw2:word32.mk_word32 (xor_w16 (w32h dw1) (w32h dw2)) (xor_w16 (w32l dw1) (w32l dw2)). + +(* operatore rotazione destra con carry *) +ndefinition rcr_w32 ≝ +λdw:word32.λc:bool.match rcr_w16 (w32h dw) c with + [ pair wh' c' ⇒ match rcr_w16 (w32l dw) c' with + [ pair wl' c'' ⇒ pair … (mk_word32 wh' wl') c'' ]]. + +(* operatore shift destro *) +ndefinition shr_w32 ≝ +λdw:word32.match rcr_w16 (w32h dw) false with + [ pair wh' c' ⇒ match rcr_w16 (w32l dw) c' with + [ pair wl' c'' ⇒ pair … (mk_word32 wh' wl') c'' ]]. + +(* operatore rotazione destra *) +ndefinition ror_w32 ≝ +λdw:word32.match rcr_w16 (w32h dw) false with + [ pair wh' c' ⇒ match rcr_w16 (w32l dw) c' with + [ pair wl' c'' ⇒ match c'' with + [ true ⇒ mk_word32 (or_w16 (mk_word16 (mk_byte8 x8 x0) (mk_byte8 x0 x0)) wh') wl' + | false ⇒ mk_word32 wh' wl' ]]]. + +(* operatore rotazione destra n-volte *) +nlet rec ror_w32_n (dw:word32) (n:bitrigesim) (r:rec_bitrigesim n) on r ≝ + match r with + [ bi_O ⇒ dw + | bi_S t n' ⇒ ror_w32_n (ror_w32 dw) t n' ]. + +(* operatore rotazione sinistra con carry *) +ndefinition rcl_w32 ≝ +λdw:word32.λc:bool.match rcl_w16 (w32l dw) c with + [ pair wl' c' ⇒ match rcl_w16 (w32h dw) c' with + [ pair wh' c'' ⇒ pair … (mk_word32 wh' wl') c'' ]]. + +(* operatore shift sinistro *) +ndefinition shl_w32 ≝ +λdw:word32.match rcl_w16 (w32l dw) false with + [ pair wl' c' ⇒ match rcl_w16 (w32h dw) c' with + [ pair wh' c'' ⇒ pair … (mk_word32 wh' wl') c'' ]]. + +(* operatore rotazione sinistra *) +ndefinition rol_w32 ≝ +λdw:word32.match rcl_w16 (w32l dw) false with + [ pair wl' c' ⇒ match rcl_w16 (w32h dw) c' with + [ pair wh' c'' ⇒ match c'' with + [ true ⇒ mk_word32 wh' (or_w16 (mk_word16 (mk_byte8 x0 x0) (mk_byte8 x0 x1)) wl') + | false ⇒ mk_word32 wh' wl' ]]]. + +(* operatore rotazione sinistra n-volte *) +nlet rec rol_w32_n (dw:word32) (n:bitrigesim) (r:rec_bitrigesim n) on r ≝ + match r with + [ bi_O ⇒ dw + | bi_S t n' ⇒ rol_w32_n (rol_w32 dw) t n' ]. + +(* operatore not/complemento a 1 *) +ndefinition not_w32 ≝ +λdw:word32.mk_word32 (not_w16 (w32h dw)) (not_w16 (w32l dw)). + +(* operatore somma con data+carry → data+carry *) +ndefinition plus_w32_dc_dc ≝ +λdw1,dw2:word32.λc:bool. + match plus_w16_dc_dc (w32l dw1) (w32l dw2) c with + [ pair l c ⇒ match plus_w16_dc_dc (w32h dw1) (w32h dw2) c with + [ pair h c' ⇒ pair … 〈h.l〉 c' ]]. + +(* operatore somma con data+carry → data *) +ndefinition plus_w32_dc_d ≝ +λdw1,dw2:word32.λc:bool. + match plus_w16_dc_dc (w32l dw1) (w32l dw2) c with + [ pair l c ⇒ 〈plus_w16_dc_d (w32h dw1) (w32h dw2) c.l〉 ]. + +(* operatore somma con data+carry → c *) +ndefinition plus_w32_dc_c ≝ +λdw1,dw2:word32.λc:bool. + plus_w16_dc_c (w32h dw1) (w32h dw2) (plus_w16_dc_c (w32l dw1) (w32l dw2) c). + +(* operatore somma con data → data+carry *) +ndefinition plus_w32_d_dc ≝ +λdw1,dw2:word32. + match plus_w16_d_dc (w32l dw1) (w32l dw2) with + [ pair l c ⇒ match plus_w16_dc_dc (w32h dw1) (w32h dw2) c with + [ pair h c' ⇒ pair … 〈h.l〉 c' ]]. + +(* operatore somma con data → data *) +ndefinition plus_w32_d_d ≝ +λdw1,dw2:word32. + match plus_w16_d_dc (w32l dw1) (w32l dw2) with + [ pair l c ⇒ 〈plus_w16_dc_d (w32h dw1) (w32h dw2) c.l〉 ]. + +(* operatore somma con data → c *) +ndefinition plus_w32_d_c ≝ +λdw1,dw2:word32. + plus_w16_dc_c (w32h dw1) (w32h dw2) (plus_w16_d_c (w32l dw1) (w32l dw2)). + +(* operatore Most Significant Bit *) +ndefinition MSB_w32 ≝ λdw:word32.eq_ex x8 (and_ex x8 (b8h (w16h (w32h dw)))). + +(* operatore predecessore *) +ndefinition pred_w32 ≝ +λdw:word32.match eq_w16 (w32l dw) (mk_word16 (mk_byte8 x0 x0) (mk_byte8 x0 x0)) with + [ true ⇒ mk_word32 (pred_w16 (w32h dw)) (pred_w16 (w32l dw)) + | false ⇒ mk_word32 (w32h dw) (pred_w16 (w32l dw)) ]. + +(* operatore successore *) +ndefinition succ_w32 ≝ +λdw:word32.match eq_w16 (w32l dw) (mk_word16 (mk_byte8 xF xF) (mk_byte8 xF xF)) with + [ true ⇒ mk_word32 (succ_w16 (w32h dw)) (succ_w16 (w32l dw)) + | false ⇒ mk_word32 (w32h dw) (succ_w16 (w32l dw)) ]. + +(* operatore neg/complemento a 2 *) +ndefinition compl_w32 ≝ +λdw:word32.match MSB_w32 dw with + [ true ⇒ succ_w32 (not_w32 dw) + | false ⇒ not_w32 (pred_w32 dw) ]. + +(* + operatore moltiplicazione senza segno: b*b=[0x00000000,0xFFFE0001] + ... in pratica (〈a:b〉*〈c:d〉) = (a*c)<<16+(a*d)<<8+(b*c)<<8+(b*d) +*) +ndefinition mul_w16 ≝ +λw1,w2:word16.match w1 with +[ mk_word16 b1h b1l ⇒ match w2 with +[ mk_word16 b2h b2l ⇒ match mul_b8 b1l b2l with +[ mk_word16 t1_h t1_l ⇒ match mul_b8 b1h b2l with +[ mk_word16 t2_h t2_l ⇒ match mul_b8 b2h b1l with +[ mk_word16 t3_h t3_l ⇒ match mul_b8 b1h b2h with +[ mk_word16 t4_h t4_l ⇒ + plus_w32_d_d + (plus_w32_d_d + (plus_w32_d_d 〈〈〈x0,x0〉:t3_h〉.〈t3_l:〈x0,x0〉〉〉 〈〈〈x0,x0〉:t2_h〉.〈t2_l:〈x0,x0〉〉〉) 〈〈t4_h:t4_l〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈t1_h:t1_l〉〉 +]]]]]]. + +(* divisione senza segno (secondo la logica delle ALU): (quoziente resto) overflow *) +nlet rec div_w16_aux (divd:word32) (divs:word32) (molt:word16) (q:word16) (c:exadecim) (rc:rec_exadecim c) on rc ≝ + let w' ≝ plus_w32_d_d divd (compl_w32 divs) in + match rc with + [ ex_O ⇒ match le_w32 divs divd with + [ true ⇒ triple … (or_w16 molt q) (w32l w') (⊖ (eq_w16 (w32h w') 〈〈x0,x0〉:〈x0,x0〉〉)) + | false ⇒ triple … q (w32l divd) (⊖ (eq_w16 (w32h divd) 〈〈x0,x0〉:〈x0,x0〉〉)) ] + | ex_S t c' ⇒ match le_w32 divs divd with + [ true ⇒ div_w16_aux w' (ror_w32 divs) (ror_w16 molt) (or_w16 molt q) t c' + | false ⇒ div_w16_aux divd (ror_w32 divs) (ror_w16 molt) q t c' ]]. + +ndefinition div_w16 ≝ +λw:word32.λb:word16.match eq_w16 b 〈〈x0,x0〉:〈x0,x0〉〉 with +(* + la combinazione n/0 e' illegale, segnala solo overflow senza dare risultato +*) + [ true ⇒ triple … 〈〈xF,xF〉:〈xF,xF〉〉 (w32l w) true + | false ⇒ match eq_w32 w 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x0〉〉〉 with +(* 0 diviso qualsiasi cosa diverso da 0 da' q=0 r=0 o=false *) + [ true ⇒ triple … 〈〈x0,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,x0〉〉 false +(* 1) e' una divisione sensata che produrra' overflow/risultato *) +(* 2) parametri: dividendo, divisore, moltiplicatore, quoziente, contatore *) +(* 3) ad ogni ciclo il divisore e il moltiplicatore vengono scalati di 1 a dx *) +(* 4) il moltiplicatore e' la quantita' aggiunta al quoziente se il divisore *) +(* puo' essere sottratto al dividendo *) + | false ⇒ div_w16_aux w (rol_w32_n 〈〈〈x0,x0〉:〈x0,x0〉〉.b〉 ? (bit_to_recbit t0F)) 〈〈x8,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,x0〉〉 ? (ex_to_recex xF) ]]. + +(* operatore x in [inf,sup] *) +ndefinition inrange_w32 ≝ +λx,inf,sup:word32.(le_w32 inf sup) ⊗ (ge_w32 x inf) ⊗ (le_w32 x sup). + +(* iteratore sulle word *) +ndefinition forall_w32 ≝ + λP. + forall_w16 (λbh. + forall_w16 (λbl. + P (mk_word32 bh bl ))). diff --git a/helm/software/matita/contribs/ng_assembly/num/word32_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/word32_lemmas.ma new file mode 100755 index 000000000..d7f6cc558 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/num/word32_lemmas.ma @@ -0,0 +1,327 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* ********************************************************************** *) + +include "num/word32.ma". +include "num/word16_lemmas.ma". + +(* ***** *) +(* DWORD *) +(* ***** *) + +nlemma word32_destruct_1 : +∀x1,x2,y1,y2. + mk_word32 x1 y1 = mk_word32 x2 y2 → x1 = x2. + #x1; #x2; #y1; #y2; #H; + nchange with (match mk_word32 x2 y2 with [ mk_word32 a _ ⇒ x1 = a ]); + nrewrite < H; + nnormalize; + napply refl_eq. +nqed. + +nlemma word32_destruct_2 : +∀x1,x2,y1,y2. + mk_word32 x1 y1 = mk_word32 x2 y2 → y1 = y2. + #x1; #x2; #y1; #y2; #H; + nchange with (match mk_word32 x2 y2 with [ mk_word32 _ b ⇒ y1 = b ]); + nrewrite < H; + nnormalize; + napply refl_eq. +nqed. + +nlemma symmetric_eqw32 : symmetricT word32 bool eq_w32. + #dw1; #dw2; + nelim dw1; + nelim dw2; + #w1; #w2; #w3; #w4; + nchange with (((eq_w16 w3 w1)⊗(eq_w16 w4 w2)) = ((eq_w16 w1 w3)⊗(eq_w16 w2 w4))); + nrewrite > (symmetric_eqw16 w1 w3); + nrewrite > (symmetric_eqw16 w2 w4); + napply refl_eq. +nqed. + +nlemma symmetric_andw32 : symmetricT word32 word32 and_w32. + #dw1; #dw2; + nelim dw1; + nelim dw2; + #w1; #w2; #w3; #w4; + nchange with ((mk_word32 (and_w16 w3 w1) (and_w16 w4 w2)) = (mk_word32 (and_w16 w1 w3) (and_w16 w2 w4))); + nrewrite > (symmetric_andw16 w1 w3); + nrewrite > (symmetric_andw16 w2 w4); + napply refl_eq. +nqed. + +nlemma associative_andw32 : ∀dw1,dw2,dw3.(and_w32 (and_w32 dw1 dw2) dw3) = (and_w32 dw1 (and_w32 dw2 dw3)). + #dw1; #dw2; #dw3; + nelim dw1; + #w1; #w2; + nelim dw2; + #w3; #w4; + nelim dw3; + #w5; #w6; + nchange with (mk_word32 (and_w16 (and_w16 w1 w3) w5) (and_w16 (and_w16 w2 w4) w6) = + mk_word32 (and_w16 w1 (and_w16 w3 w5)) (and_w16 w2 (and_w16 w4 w6))); + nrewrite < (associative_andw16 w1 w3 w5); + nrewrite < (associative_andw16 w2 w4 w6); + napply refl_eq. +nqed. + +nlemma symmetric_orw32 : symmetricT word32 word32 or_w32. + #dw1; #dw2; + nelim dw1; + nelim dw2; + #w1; #w2; #w3; #w4; + nchange with ((mk_word32 (or_w16 w3 w1) (or_w16 w4 w2)) = (mk_word32 (or_w16 w1 w3) (or_w16 w2 w4))); + nrewrite > (symmetric_orw16 w1 w3); + nrewrite > (symmetric_orw16 w2 w4); + napply refl_eq. +nqed. + +nlemma associative_orw32 : ∀dw1,dw2,dw3.(or_w32 (or_w32 dw1 dw2) dw3) = (or_w32 dw1 (or_w32 dw2 dw3)). + #dw1; #dw2; #dw3; + nelim dw1; + #w1; #w2; + nelim dw2; + #w3; #w4; + nelim dw3; + #w5; #w6; + nchange with (mk_word32 (or_w16 (or_w16 w1 w3) w5) (or_w16 (or_w16 w2 w4) w6) = + mk_word32 (or_w16 w1 (or_w16 w3 w5)) (or_w16 w2 (or_w16 w4 w6))); + nrewrite < (associative_orw16 w1 w3 w5); + nrewrite < (associative_orw16 w2 w4 w6); + napply refl_eq. +nqed. + +nlemma symmetric_xorw32 : symmetricT word32 word32 xor_w32. + #dw1; #dw2; + nelim dw1; + nelim dw2; + #w1; #w2; #w3; #w4; + nchange with ((mk_word32 (xor_w16 w3 w1) (xor_w16 w4 w2)) = (mk_word32 (xor_w16 w1 w3) (xor_w16 w2 w4))); + nrewrite > (symmetric_xorw16 w1 w3); + nrewrite > (symmetric_xorw16 w2 w4); + napply refl_eq. +nqed. + +nlemma associative_xorw32 : ∀dw1,dw2,dw3.(xor_w32 (xor_w32 dw1 dw2) dw3) = (xor_w32 dw1 (xor_w32 dw2 dw3)). + #dw1; #dw2; #dw3; + nelim dw1; + #w1; #w2; + nelim dw2; + #w3; #w4; + nelim dw3; + #w5; #w6; + nchange with (mk_word32 (xor_w16 (xor_w16 w1 w3) w5) (xor_w16 (xor_w16 w2 w4) w6) = + mk_word32 (xor_w16 w1 (xor_w16 w3 w5)) (xor_w16 w2 (xor_w16 w4 w6))); + nrewrite < (associative_xorw16 w1 w3 w5); + nrewrite < (associative_xorw16 w2 w4 w6); + napply refl_eq. +nqed. + +nlemma symmetric_plusw32_dc_dc : ∀dw1,dw2,c.plus_w32_dc_dc dw1 dw2 c = plus_w32_dc_dc dw2 dw1 c. + #dw1; #dw2; #c; + nelim dw1; + #w1; #w2; + nelim dw2; + #w3; #w4; + nchange with ( + match plus_w16_dc_dc w2 w4 c with + [ pair l c ⇒ match plus_w16_dc_dc w1 w3 c with + [ pair h c' ⇒ pair … 〈h.l〉 c' ]] = + match plus_w16_dc_dc w4 w2 c with + [ pair l c ⇒ match plus_w16_dc_dc w3 w1 c with + [ pair h c' ⇒ pair … 〈h.l〉 c' ]]); + nrewrite > (symmetric_plusw16_dc_dc w4 w2 c); + ncases (plus_w16_dc_dc w2 w4 c); + #w5; #c1; + nchange with ( + match plus_w16_dc_dc w1 w3 c1 with + [ pair h c' ⇒ pair … 〈h.w5〉 c' ] = + match plus_w16_dc_dc w3 w1 c1 with + [ pair h c' ⇒ pair … 〈h.w5〉 c' ]); + nrewrite > (symmetric_plusw16_dc_dc w1 w3 c1); + napply refl_eq. +nqed. + +nlemma symmetric_plusw32_dc_d : ∀dw1,dw2,c.plus_w32_dc_d dw1 dw2 c = plus_w32_dc_d dw2 dw1 c. + #dw1; #dw2; #c; + nelim dw1; + #w1; #w2; + nelim dw2; + #w3; #w4; + nchange with ( + match plus_w16_dc_dc w2 w4 c with + [ pair l c ⇒ 〈plus_w16_dc_d w1 w3 c.l〉 ] = + match plus_w16_dc_dc w4 w2 c with + [ pair l c ⇒ 〈plus_w16_dc_d w3 w1 c.l〉 ]); + nrewrite > (symmetric_plusw16_dc_dc w4 w2 c); + ncases (plus_w16_dc_dc w2 w4 c); + #w5; #c1; + nchange with (〈plus_w16_dc_d w1 w3 c1.w5〉 = 〈plus_w16_dc_d w3 w1 c1.w5〉); + nrewrite > (symmetric_plusw16_dc_d w1 w3 c1); + napply refl_eq. +nqed. + +nlemma symmetric_plusw32_dc_c : ∀dw1,dw2,c.plus_w32_dc_c dw1 dw2 c = plus_w32_dc_c dw2 dw1 c. + #dw1; #dw2; #c; + nelim dw1; + #w1; #w2; + nelim dw2; + #w3; #w4; + nchange with ( + plus_w16_dc_c w1 w3 (plus_w16_dc_c w2 w4 c) = + plus_w16_dc_c w3 w1 (plus_w16_dc_c w4 w2 c)); + nrewrite > (symmetric_plusw16_dc_c w4 w2 c); + nrewrite > (symmetric_plusw16_dc_c w3 w1 (plus_w16_dc_c w2 w4 c)); + napply refl_eq. +nqed. + +nlemma symmetric_plusw32_d_dc : ∀dw1,dw2.plus_w32_d_dc dw1 dw2 = plus_w32_d_dc dw2 dw1. + #dw1; #dw2; + nelim dw1; + #w1; #w2; + nelim dw2; + #w3; #w4; + nchange with ( + match plus_w16_d_dc w2 w4 with + [ pair l c ⇒ match plus_w16_dc_dc w1 w3 c with + [ pair h c' ⇒ pair … 〈h.l〉 c' ]] = + match plus_w16_d_dc w4 w2 with + [ pair l c ⇒ match plus_w16_dc_dc w3 w1 c with + [ pair h c' ⇒ pair … 〈h.l〉 c' ]]); + nrewrite > (symmetric_plusw16_d_dc w4 w2); + ncases (plus_w16_d_dc w2 w4); + #w5; #c; + nchange with ( + match plus_w16_dc_dc w1 w3 c with + [ pair h c' ⇒ pair … 〈h.w5〉 c' ] = + match plus_w16_dc_dc w3 w1 c with + [ pair h c' ⇒ pair … 〈h.w5〉 c' ]); + nrewrite > (symmetric_plusw16_dc_dc w1 w3 c); + napply refl_eq. +nqed. + +nlemma symmetric_plusw32_d_d : ∀dw1,dw2.plus_w32_d_d dw1 dw2 = plus_w32_d_d dw2 dw1. + #dw1; #dw2; + nelim dw1; + #w1; #w2; + nelim dw2; + #w3; #w4; + nchange with ( + match plus_w16_d_dc w2 w4 with + [ pair l c ⇒ 〈plus_w16_dc_d w1 w3 c.l〉 ] = + match plus_w16_d_dc w4 w2 with + [ pair l c ⇒ 〈plus_w16_dc_d w3 w1 c.l〉 ]); + nrewrite > (symmetric_plusw16_d_dc w4 w2); + ncases (plus_w16_d_dc w2 w4); + #w5; #c; + nchange with (〈plus_w16_dc_d w1 w3 c.w5〉 = 〈plus_w16_dc_d w3 w1 c.w5〉); + nrewrite > (symmetric_plusw16_dc_d w1 w3 c); + napply refl_eq. +nqed. + +nlemma symmetric_plusw32_d_c : ∀dw1,dw2.plus_w32_d_c dw1 dw2 = plus_w32_d_c dw2 dw1. + #dw1; #dw2; + nelim dw1; + #w1; #w2; + nelim dw2; + #w3; #w4; + nchange with ( + plus_w16_dc_c w1 w3 (plus_w16_d_c w2 w4) = + plus_w16_dc_c w3 w1 (plus_w16_d_c w4 w2)); + nrewrite > (symmetric_plusw16_d_c w4 w2); + nrewrite > (symmetric_plusw16_dc_c w3 w1 (plus_w16_d_c w2 w4)); + napply refl_eq. +nqed. + +nlemma symmetric_mulw16 : symmetricT word16 word32 mul_w16. + #w1; #w2; + nelim w1; + #b1; #b2; + nelim w2; + #b3; #b4; + nchange with (match mul_b8 b2 b4 with + [ mk_word16 t1_h t1_l ⇒ match mul_b8 b1 b4 with + [ mk_word16 t2_h t2_l ⇒ match mul_b8 b3 b2 with + [ mk_word16 t3_h t3_l ⇒ match mul_b8 b1 b3 with + [ mk_word16 t4_h t4_l ⇒ plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:t3_h〉.〈t3_l:〈x0,x0〉〉〉 〈〈〈x0,x0〉:t2_h〉.〈t2_l:〈x0,x0〉〉〉) 〈〈t4_h:t4_l〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈t1_h:t1_l〉〉 + ]]]] = match mul_b8 b4 b2 with + [ mk_word16 t1_h t1_l ⇒ match mul_b8 b3 b2 with + [ mk_word16 t2_h t2_l ⇒ match mul_b8 b1 b4 with + [ mk_word16 t3_h t3_l ⇒ match mul_b8 b3 b1 with + [ mk_word16 t4_h t4_l ⇒ plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:t3_h〉.〈t3_l:〈x0,x0〉〉〉 〈〈〈x0,x0〉:t2_h〉.〈t2_l:〈x0,x0〉〉〉) 〈〈t4_h:t4_l〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈t1_h:t1_l〉〉 + ]]]]); + nrewrite < (symmetric_mulb8 b2 b4); + ncases (mul_b8 b2 b4); + #b5; #b6; + nchange with (match mul_b8 b1 b4 with + [ mk_word16 t2_h t2_l ⇒ match mul_b8 b3 b2 with + [ mk_word16 t3_h t3_l ⇒ match mul_b8 b1 b3 with + [ mk_word16 t4_h t4_l ⇒ plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:t3_h〉.〈t3_l:〈x0,x0〉〉〉 〈〈〈x0,x0〉:t2_h〉.〈t2_l:〈x0,x0〉〉〉) 〈〈t4_h:t4_l〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈b5:b6〉〉 + ]]] = match mul_b8 b3 b2 with + [ mk_word16 t2_h t2_l ⇒ match mul_b8 b1 b4 with + [ mk_word16 t3_h t3_l ⇒ match mul_b8 b3 b1 with + [ mk_word16 t4_h t4_l ⇒ plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:t3_h〉.〈t3_l:〈x0,x0〉〉〉 〈〈〈x0,x0〉:t2_h〉.〈t2_l:〈x0,x0〉〉〉) 〈〈t4_h:t4_l〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈b5:b6〉〉 + ]]]); + ncases (mul_b8 b3 b2); + #b7; #b8; + ncases (mul_b8 b1 b4); + #b9; #b10; + nchange with (match mul_b8 b1 b3 with + [ mk_word16 t4_h t4_l ⇒ plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:b7〉.〈b8:〈x0,x0〉〉〉 〈〈〈x0,x0〉:b9〉.〈b10:〈x0,x0〉〉〉) 〈〈t4_h:t4_l〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈b5:b6〉〉 + ] = match mul_b8 b3 b1 with + [ mk_word16 t4_h t4_l ⇒ plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:b9〉.〈b10:〈x0,x0〉〉〉 〈〈〈x0,x0〉:b7〉.〈b8:〈x0,x0〉〉〉) 〈〈t4_h:t4_l〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈b5:b6〉〉 + ]); + nrewrite < (symmetric_mulb8 b1 b3); + ncases (mul_b8 b1 b3); + #b11; #b12; + nchange with ((plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:b7〉.〈b8:〈x0,x0〉〉〉 〈〈〈x0,x0〉:b9〉.〈b10:〈x0,x0〉〉〉) 〈〈b11:b12〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈b5:b6〉〉) = + (plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:b9〉.〈b10:〈x0,x0〉〉〉 〈〈〈x0,x0〉:b7〉.〈b8:〈x0,x0〉〉〉) 〈〈b11:b12〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈b5:b6〉〉)); + nrewrite > (symmetric_plusw32_d_d 〈〈〈x0,x0〉:b7〉.〈b8:〈x0,x0〉〉〉 〈〈〈x0,x0〉:b9〉.〈b10:〈x0,x0〉〉〉); + napply refl_eq. +nqed. + +nlemma eqw32_to_eq : ∀dw1,dw2:word32.(eq_w32 dw1 dw2 = true) → (dw1 = dw2). + #dw1; #dw2; + nelim dw1; + nelim dw2; + #w1; #w2; #w3; #w4; + nchange in ⊢ (% → ?) with (((eq_w16 w3 w1)⊗(eq_w16 w4 w2)) = true); + #H; + nrewrite < (eqw16_to_eq … (andb_true_true_l … H)); + nrewrite < (eqw16_to_eq … (andb_true_true_r … H)); + napply refl_eq. +nqed. + +nlemma eq_to_eqw32 : ∀dw1,dw2.dw1 = dw2 → eq_w32 dw1 dw2 = true. + #dw1; #dw2; + nelim dw1; + nelim dw2; + #w1; #w2; #w3; #w4; + #H; + nrewrite < (word32_destruct_1 … H); + nrewrite < (word32_destruct_2 … H); + nchange with (((eq_w16 w3 w3)⊗(eq_w16 w4 w4)) = true); + nrewrite > (eq_to_eqw16 w3 w3 (refl_eq …)); + nrewrite > (eq_to_eqw16 w4 w4 (refl_eq …)); + nnormalize; + napply refl_eq. +nqed. -- 2.39.2