From 29cfb9e2961e62c836cb50217905c0594a074e81 Mon Sep 17 00:00:00 2001 From: Cosimo Oliboni Date: Fri, 7 Aug 2009 00:08:25 +0000 Subject: [PATCH] freescale porting, work in progress --- .../ng_assembly/common/ascii_lemmas3.ma | 252 ++++----- .../ng_assembly/common/list_utility_lemmas.ma | 277 +++++++++- .../contribs/ng_assembly/common/nat_lemmas.ma | 52 +- .../ng_assembly/common/option_lemmas.ma | 55 ++ .../ng_assembly/common/prod_lemmas.ma | 481 +++++++++++++++++- .../ng_assembly/common/string_lemmas.ma | 85 ++++ .../contribs/ng_assembly/common/theory.ma | 164 +++++- .../matita/contribs/ng_assembly/depends | 2 +- .../contribs/ng_assembly/num/bitrigesim.ma | 48 +- .../ng_assembly/num/bitrigesim_lemmas.ma | 470 +++++++---------- .../contribs/ng_assembly/num/bool_lemmas.ma | 95 +++- .../contribs/ng_assembly/num/byte8_lemmas.ma | 22 +- .../ng_assembly/num/exadecim_lemmas.ma | 228 +++++---- .../contribs/ng_assembly/num/oct_lemmas.ma | 4 +- .../ng_assembly/num/quatern_lemmas.ma | 4 +- .../contribs/ng_assembly/num/word16_lemmas.ma | 22 +- .../contribs/ng_assembly/num/word32_lemmas.ma | 22 +- 17 files changed, 1631 insertions(+), 652 deletions(-) diff --git a/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas3.ma b/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas3.ma index de510fe40..98dabd50e 100755 --- a/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas3.ma +++ b/helm/software/matita/contribs/ng_assembly/common/ascii_lemmas3.ma @@ -29,442 +29,442 @@ include "num/bool_lemmas.ma". nlemma decidable_ascii1 : ∀x:ascii.decidable (ch_0 = x). #x; nnormalize; nelim x; - ##[ ##1: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##1: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii2 : ∀x:ascii.decidable (ch_1 = x). #x; nnormalize; nelim x; - ##[ ##2: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##2: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii3 : ∀x:ascii.decidable (ch_2 = x). #x; nnormalize; nelim x; - ##[ ##3: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##3: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii4 : ∀x:ascii.decidable (ch_3 = x). #x; nnormalize; nelim x; - ##[ ##4: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##4: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii5 : ∀x:ascii.decidable (ch_4 = x). #x; nnormalize; nelim x; - ##[ ##5: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##5: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii6 : ∀x:ascii.decidable (ch_5 = x). #x; nnormalize; nelim x; - ##[ ##6: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##6: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii7 : ∀x:ascii.decidable (ch_6 = x). #x; nnormalize; nelim x; - ##[ ##7: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##7: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii8 : ∀x:ascii.decidable (ch_7 = x). #x; nnormalize; nelim x; - ##[ ##8: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##8: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii9 : ∀x:ascii.decidable (ch_8 = x). #x; nnormalize; nelim x; - ##[ ##9: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##9: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii10 : ∀x:ascii.decidable (ch_9 = x). #x; nnormalize; nelim x; - ##[ ##10: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##10: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii11 : ∀x:ascii.decidable (ch__ = x). #x; nnormalize; nelim x; - ##[ ##11: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##11: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii12 : ∀x:ascii.decidable (ch_A = x). #x; nnormalize; nelim x; - ##[ ##12: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##12: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii13 : ∀x:ascii.decidable (ch_B = x). #x; nnormalize; nelim x; - ##[ ##13: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##13: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii14 : ∀x:ascii.decidable (ch_C = x). #x; nnormalize; nelim x; - ##[ ##14: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##14: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii15 : ∀x:ascii.decidable (ch_D = x). #x; nnormalize; nelim x; - ##[ ##15: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##15: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii16 : ∀x:ascii.decidable (ch_E = x). #x; nnormalize; nelim x; - ##[ ##16: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##16: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii17 : ∀x:ascii.decidable (ch_F = x). #x; nnormalize; nelim x; - ##[ ##17: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##17: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii18 : ∀x:ascii.decidable (ch_G = x). #x; nnormalize; nelim x; - ##[ ##18: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##18: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii19 : ∀x:ascii.decidable (ch_H = x). #x; nnormalize; nelim x; - ##[ ##19: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##19: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii20 : ∀x:ascii.decidable (ch_I = x). #x; nnormalize; nelim x; - ##[ ##20: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##20: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii21 : ∀x:ascii.decidable (ch_J = x). #x; nnormalize; nelim x; - ##[ ##21: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##21: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii22 : ∀x:ascii.decidable (ch_K = x). #x; nnormalize; nelim x; - ##[ ##22: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##22: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii23 : ∀x:ascii.decidable (ch_L = x). #x; nnormalize; nelim x; - ##[ ##23: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##23: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii24 : ∀x:ascii.decidable (ch_M = x). #x; nnormalize; nelim x; - ##[ ##24: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##24: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii25 : ∀x:ascii.decidable (ch_N = x). #x; nnormalize; nelim x; - ##[ ##25: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##25: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii26 : ∀x:ascii.decidable (ch_O = x). #x; nnormalize; nelim x; - ##[ ##26: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##26: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii27 : ∀x:ascii.decidable (ch_P = x). #x; nnormalize; nelim x; - ##[ ##27: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##27: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii28 : ∀x:ascii.decidable (ch_Q = x). #x; nnormalize; nelim x; - ##[ ##28: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##28: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii29 : ∀x:ascii.decidable (ch_R = x). #x; nnormalize; nelim x; - ##[ ##29: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##29: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii30 : ∀x:ascii.decidable (ch_S = x). #x; nnormalize; nelim x; - ##[ ##30: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##30: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii31 : ∀x:ascii.decidable (ch_T = x). #x; nnormalize; nelim x; - ##[ ##31: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##31: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii32 : ∀x:ascii.decidable (ch_U = x). #x; nnormalize; nelim x; - ##[ ##32: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##32: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii33 : ∀x:ascii.decidable (ch_V = x). #x; nnormalize; nelim x; - ##[ ##33: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##33: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii34 : ∀x:ascii.decidable (ch_W = x). #x; nnormalize; nelim x; - ##[ ##34: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##34: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii35 : ∀x:ascii.decidable (ch_X = x). #x; nnormalize; nelim x; - ##[ ##35: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##35: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii36 : ∀x:ascii.decidable (ch_Y = x). #x; nnormalize; nelim x; - ##[ ##36: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##36: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii37 : ∀x:ascii.decidable (ch_Z = x). #x; nnormalize; nelim x; - ##[ ##37: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##37: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii38 : ∀x:ascii.decidable (ch_a = x). #x; nnormalize; nelim x; - ##[ ##38: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##38: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii39 : ∀x:ascii.decidable (ch_b = x). #x; nnormalize; nelim x; - ##[ ##39: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##39: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii40 : ∀x:ascii.decidable (ch_c = x). #x; nnormalize; nelim x; - ##[ ##40: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##40: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii41 : ∀x:ascii.decidable (ch_d = x). #x; nnormalize; nelim x; - ##[ ##41: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##41: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii42 : ∀x:ascii.decidable (ch_e = x). #x; nnormalize; nelim x; - ##[ ##42: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##42: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii43 : ∀x:ascii.decidable (ch_f = x). #x; nnormalize; nelim x; - ##[ ##43: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##43: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii44 : ∀x:ascii.decidable (ch_g = x). #x; nnormalize; nelim x; - ##[ ##44: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##44: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii45 : ∀x:ascii.decidable (ch_h = x). #x; nnormalize; nelim x; - ##[ ##45: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##45: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii46 : ∀x:ascii.decidable (ch_i = x). #x; nnormalize; nelim x; - ##[ ##46: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##46: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii47 : ∀x:ascii.decidable (ch_j = x). #x; nnormalize; nelim x; - ##[ ##47: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##47: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii48 : ∀x:ascii.decidable (ch_k = x). #x; nnormalize; nelim x; - ##[ ##48: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##48: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii49 : ∀x:ascii.decidable (ch_l = x). #x; nnormalize; nelim x; - ##[ ##49: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##49: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii50 : ∀x:ascii.decidable (ch_m = x). #x; nnormalize; nelim x; - ##[ ##50: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##50: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii51 : ∀x:ascii.decidable (ch_n = x). #x; nnormalize; nelim x; - ##[ ##51: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##51: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii52 : ∀x:ascii.decidable (ch_o = x). #x; nnormalize; nelim x; - ##[ ##52: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##52: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii53 : ∀x:ascii.decidable (ch_p = x). #x; nnormalize; nelim x; - ##[ ##53: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##53: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii54 : ∀x:ascii.decidable (ch_q = x). #x; nnormalize; nelim x; - ##[ ##54: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##54: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii55 : ∀x:ascii.decidable (ch_r = x). #x; nnormalize; nelim x; - ##[ ##55: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##55: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii56 : ∀x:ascii.decidable (ch_s = x). #x; nnormalize; nelim x; - ##[ ##56: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##56: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii57 : ∀x:ascii.decidable (ch_t = x). #x; nnormalize; nelim x; - ##[ ##57: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##57: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii58 : ∀x:ascii.decidable (ch_u = x). #x; nnormalize; nelim x; - ##[ ##58: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##58: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii59 : ∀x:ascii.decidable (ch_v = x). #x; nnormalize; nelim x; - ##[ ##59: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##59: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii60 : ∀x:ascii.decidable (ch_w = x). #x; nnormalize; nelim x; - ##[ ##60: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##60: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii61 : ∀x:ascii.decidable (ch_x = x). #x; nnormalize; nelim x; - ##[ ##61: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##61: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii62 : ∀x:ascii.decidable (ch_y = x). #x; nnormalize; nelim x; - ##[ ##62: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##62: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. nlemma decidable_ascii63 : ∀x:ascii.decidable (ch_z = x). #x; nnormalize; nelim x; - ##[ ##63: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) + ##[ ##63: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H) ##] nqed. diff --git a/helm/software/matita/contribs/ng_assembly/common/list_utility_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/list_utility_lemmas.ma index 9cc7f317d..c9d7b910f 100755 --- a/helm/software/matita/contribs/ng_assembly/common/list_utility_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/common/list_utility_lemmas.ma @@ -141,6 +141,145 @@ nlemma eq_to_bfoldrightlist2 ##] nqed. +nlemma bfoldrightlist2_to_lenlist + : ∀T.∀f:T → T → bool.∀l1,l2:list T.bfold_right_list2 T f l1 l2 = true → len_list T l1 = len_list T l2. + #T; #f; #l1; + nelim l1; + ##[ ##1: #l2; ncases l2; + ##[ ##1: nnormalize; #H; napply refl_eq + ##| ##2: nnormalize; #hh; #tt; #H; napply (bool_destruct … H) + ##] + ##| ##2: #hh; #tt; #H; #l2; ncases l2; + ##[ ##1: nnormalize; #H1; napply (bool_destruct … H1) + ##| ##2: #hh1; #tt1; #H1; nnormalize; + nrewrite > (H tt1 ?); + ##[ ##1: napply refl_eq + ##| ##2: nchange in H1:(%) with ((? ⊗ (bfold_right_list2 T f tt tt1)) = true); + napply (andb_true_true_r … H1) + ##] + ##] + ##] +nqed. + +nlemma decidable_list : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀x,y:list T.decidable (x = y). + #T; #H; #x; nelim x; + ##[ ##1: #y; ncases y; + ##[ ##1: nnormalize; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …)) + ##| ##2: #hh2; #tt2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?); + nnormalize; #H1; napply (list_destruct_nil_cons T … H1) + ##] + ##| ##2: #hh1; #tt1; #H1; #y; ncases y; + ##[ ##1: nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?); + nnormalize; #H2; napply (list_destruct_cons_nil T … H2) + ##| ##2: #hh2; #tt2; nnormalize; napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H …)); + ##[ ##2: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) ?); + nnormalize; #H3; napply (H2 (list_destruct_1 T … H3)) + ##| ##1: #H2; napply (or2_elim (tt1 = tt2) (tt1 ≠ tt2) ? (H1 tt2)); + ##[ ##2: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?); + nnormalize; #H4; napply (H3 (list_destruct_2 T … H4)) + ##| ##1: #H3; napply (or2_intro1 (? = ?) (? ≠ ?) ?); + nrewrite > H2; nrewrite > H3; napply refl_eq + ##] + ##] + ##] + ##] +nqed. + +nlemma nbfoldrightlist2_to_neq + : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:list T1. + (∀x,y.(f x y = false → x ≠ y)) → + (bfold_right_list2 T1 f l1 l2 = false → l1 ≠ l2). + #T; #f; #l1; + nelim l1; + ##[ ##1: #l2; ncases l2; + ##[ ##1: #H; nnormalize; #H1; napply (bool_destruct … H1) + ##| ##2: #hh2; #ll2; #H; #H1; nnormalize; #H2; napply (list_destruct_nil_cons T … H2) + ##] + ##| ##2: #hh1; #ll1; #H; #l2; ncases l2; + ##[ ##1: #H1; #H2; nnormalize; #H3; napply (list_destruct_cons_nil T … H3) + ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize; #H3; + nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = false); + napply (H ll2 H1 ? (list_destruct_2 T … H3)); + napply (or2_elim ??? (andb_false … H2) ); + ##[ ##1: #H4; napply (absurd (hh1 = hh2) …); + ##[ ##1: nrewrite > (list_destruct_1 T … H3); napply refl_eq + ##| ##2: napply (H1 … H4) + ##] + ##| ##2: #H4; napply H4 + ##] + ##] + ##] +nqed. + +nlemma list_destruct + : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀h1,h2:T.∀l1,l2:list T.(h1::l1) ≠ (h2::l2) → h1 ≠ h2 ∨ l1 ≠ l2. + #T; #H; #h1; #h2; #l1; nelim l1; + ##[ ##1: #l2; ncases l2; + ##[ ##1: #H1; napply (or2_intro1 (h1 ≠ h2) ([] ≠ []) …); + nnormalize; #H2; nrewrite > H2 in H1:(%); + nnormalize; #H1; napply (H1 (refl_eq …)) + ##| ##2: #hh2; #ll2; #H1; napply (or2_intro2 (h1 ≠ h2) ([] ≠ (hh2::ll2)) …); + nnormalize; #H2; napply (list_destruct_nil_cons T … H2) + ##] + ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2; + ##[ ##1: #H2; napply (or2_intro2 (h1 ≠ h2) ((hh1::ll1) ≠ []) …); + nnormalize; #H3; napply (list_destruct_cons_nil T … H3) + ##| ##2: #hh2; #ll2; #H2; + napply (or2_elim (h1 = h2) (h1 ≠ h2) ? (H h1 h2) …); + ##[ ##2: #H3; napply (or2_intro1 (h1 ≠ h2) ((hh1::ll1) ≠ (hh2::ll2)) H3) + ##| ##1: #H3; napply (or2_intro2 (h1 ≠ h2) ((hh1::ll1) ≠ (hh2::ll2) …)); + nrewrite > H3 in H2:(%); #H2; + nnormalize; #H4; nrewrite > (list_destruct_1 T … H4) in H2:(%); #H2; + nrewrite > (list_destruct_2 T … H4) in H2:(%); #H2; + napply (H2 (refl_eq …)) + ##] + ##] + ##] +nqed. + +nlemma neq_to_nbfoldrightlist2 + : ∀T:Type.∀f:T → T → bool.∀l1,l2:list T. + (∀x,y:T.decidable (x = y)) → + (∀x,y.(x ≠ y → f x y = false)) → + (l1 ≠ l2 → bfold_right_list2 T f l1 l2 = false). + #T; #f; #l1; + nelim l1; + ##[ ##1: #l2; ncases l2; + ##[ ##1: #H; #H1; nnormalize; #H2; nelim (H2 (refl_eq …)) + ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; #H2; napply refl_eq + ##] + ##| ##2: #hh1; #ll1; #H; #l2; ncases l2; + ##[ ##1: #H1; #H2; nnormalize; #H3; napply refl_eq + ##| ##2: #hh2; #ll2; #H1; #H2; #H3; + nchange with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = false); + napply (or2_elim (hh1 ≠ hh2) (ll1 ≠ ll2) ? (list_destruct T H1 … H3) …); + ##[ ##1: #H4; nrewrite > (H2 hh1 hh2 H4); nnormalize; napply refl_eq + ##| ##2: #H4; nrewrite > (H ll2 H1 H2 H4); + nrewrite > (symmetric_andbool (f hh1 hh2) false); + nnormalize; napply refl_eq + ##] + ##] + ##] +nqed. + +nlemma isbemptylist_to_isemptylist : ∀T,l.isb_empty_list T l = true → is_empty_list T l. + #T; #l; + ncases l; + nnormalize; + ##[ ##1: #H; napply I + ##| ##2: #x; #l; #H; napply (bool_destruct … H) + ##] +nqed. + +nlemma isnotbemptylist_to_isnotemptylist : ∀T,l.isnotb_empty_list T l = true → isnot_empty_list T l. + #T; #l; + ncases l; + nnormalize; + ##[ ##1: #H; napply (bool_destruct … H) + ##| ##2: #x; #l; #H; napply I + ##] +nqed. + (* ************** *) (* NON-EMPTY LIST *) (* ************** *) @@ -272,20 +411,134 @@ nlemma eq_to_bfoldrightnelist2 ##] nqed. -nlemma isbemptylist_to_isemptylist : ∀T,l.isb_empty_list T l = true → is_empty_list T l. - #T; #l; - ncases l; - nnormalize; - ##[ ##1: #H; napply I - ##| ##2: #x; #l; #H; napply (bool_destruct … H) +nlemma bfoldrightnelist2_to_lennelist + : ∀T.∀f:T → T → bool.∀l1,l2:ne_list T.bfold_right_neList2 T f l1 l2 = true → len_neList T l1 = len_neList T l2. + #T; #f; #l1; + nelim l1; + ##[ ##1: #hh1; #l2; ncases l2; + ##[ ##1: nnormalize; #hh2; #H; napply refl_eq + ##| ##2: nnormalize; #hh2; #tt2; #H; napply (bool_destruct … H) + ##] + ##| ##2: #hh1; #tt1; #H; #l2; ncases l2; + ##[ ##1: nnormalize; #hh2; #H1; napply (bool_destruct … H1) + ##| ##2: #hh2; #tt2; #H1; nnormalize; + nrewrite > (H tt2 ?); + ##[ ##1: napply refl_eq + ##| ##2: nchange in H1:(%) with ((? ⊗ (bfold_right_neList2 T f tt1 tt2)) = true); + napply (andb_true_true_r … H1) + ##] + ##] ##] nqed. -nlemma isnotbemptylist_to_isnotemptylist : ∀T,l.isnotb_empty_list T l = true → isnot_empty_list T l. - #T; #l; - ncases l; - nnormalize; - ##[ ##1: #H; napply (bool_destruct … H) - ##| ##2: #x; #l; #H; napply I +nlemma decidable_nelist : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀x,y:ne_list T.decidable (x = y). + #T; #H; #x; nelim x; + ##[ ##1: #hh1; #y; ncases y; + ##[ ##1: #hh2; nnormalize; napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H hh1 hh2)); + ##[ ##1: #H1; nrewrite > H1; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …)) + ##| ##2: #H1; napply (or2_intro2 (? = ?) (? ≠ ?) ?); nnormalize; + #H2; napply (H1 (nelist_destruct_nil_nil T … H2)) + ##] + ##| ##2: #hh2; #tt2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?); + nnormalize; #H1; napply (nelist_destruct_nil_cons T … H1) + ##] + ##| ##2: #hh1; #tt1; #H1; #y; ncases y; + ##[ ##1: #hh1; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?); + nnormalize; #H2; napply (nelist_destruct_cons_nil T … H2) + ##| ##2: #hh2; #tt2; nnormalize; napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H …)); + ##[ ##2: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) ?); + nnormalize; #H3; napply (H2 (nelist_destruct_cons_cons_1 T … H3)) + ##| ##1: #H2; napply (or2_elim (tt1 = tt2) (tt1 ≠ tt2) ? (H1 tt2)); + ##[ ##2: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?); + nnormalize; #H4; napply (H3 (nelist_destruct_cons_cons_2 T … H4)) + ##| ##1: #H3; napply (or2_intro1 (? = ?) (? ≠ ?) ?); + nrewrite > H2; nrewrite > H3; napply refl_eq + ##] + ##] + ##] + ##] +nqed. + +nlemma nbfoldrightnelist2_to_neq + : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1. + (∀x,y.(f x y = false → x ≠ y)) → + (bfold_right_neList2 T1 f l1 l2 = false → l1 ≠ l2). + #T; #f; #l1; + nelim l1; + ##[ ##1: #hh1; #l2; ncases l2; + ##[ ##1: #hh2; #H; nnormalize; #H1; #H2; napply (H hh1 hh2 H1 (nelist_destruct_nil_nil T … H2)) + ##| ##2: #hh2; #ll2; #H; #H1; nnormalize; #H2; napply (nelist_destruct_nil_cons T … H2) + ##] + ##| ##2: #hh1; #ll1; #H; #l2; ncases l2; + ##[ ##1: #hh2; #H1; #H2; nnormalize; #H3; napply (nelist_destruct_cons_nil T … H3) + ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize; #H3; + nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = false); + napply (H ll2 H1 ? (nelist_destruct_cons_cons_2 T … H3)); + napply (or2_elim ??? (andb_false … H2) ); + ##[ ##1: #H4; napply (absurd (hh1 = hh2) …); + ##[ ##1: nrewrite > (nelist_destruct_cons_cons_1 T … H3); napply refl_eq + ##| ##2: napply (H1 … H4) + ##] + ##| ##2: #H4; napply H4 + ##] + ##] + ##] +nqed. + +nlemma nelist_destruct + : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀h1,h2:T.∀l1,l2:ne_list T.(h1§§l1) ≠ (h2§§l2) → h1 ≠ h2 ∨ l1 ≠ l2. + #T; #H; #h1; #h2; #l1; nelim l1; + ##[ ##1: #hh1; #l2; ncases l2; + ##[ ##1: #hh2; #H1; napply (or2_elim (h1 = h2) (h1 ≠ h2) ? (H …) …); + ##[ ##2: #H2; napply (or2_intro1 (h1 ≠ h2) («£hh1» ≠ «£hh2») H2) + ##| ##1: #H2; nrewrite > H2 in H1:(%); #H1; + napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H …) …); + ##[ ##2: #H3; napply (or2_intro2 (h2 ≠ h2) («£hh1» ≠ «£hh2») ?); + nnormalize; #H4; napply (H3 (nelist_destruct_nil_nil T … H4)) + ##| ##1: #H3; nrewrite > H3 in H1:(%); #H1; nelim (H1 (refl_eq …)) + ##] + ##] + ##| ##2: #hh2; #ll2; #H1; napply (or2_intro2 (h1 ≠ h2) («£hh1» ≠ (hh2§§ll2)) …); + nnormalize; #H2; napply (nelist_destruct_nil_cons T … H2) + ##] + ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2; + ##[ ##1: #hh2; #H2; napply (or2_intro2 (h1 ≠ h2) ((hh1§§ll1) ≠ «£hh2») …); + nnormalize; #H3; napply (nelist_destruct_cons_nil T … H3) + ##| ##2: #hh2; #ll2; #H2; + napply (or2_elim (h1 = h2) (h1 ≠ h2) ? (H h1 h2) …); + ##[ ##2: #H3; napply (or2_intro1 (h1 ≠ h2) ((hh1§§ll1) ≠ (hh2§§ll2)) H3) + ##| ##1: #H3; napply (or2_intro2 (h1 ≠ h2) ((hh1§§ll1) ≠ (hh2§§ll2) …)); + nrewrite > H3 in H2:(%); #H2; + nnormalize; #H4; nrewrite > (nelist_destruct_cons_cons_1 T … H4) in H2:(%); #H2; + nrewrite > (nelist_destruct_cons_cons_2 T … H4) in H2:(%); #H2; + napply (H2 (refl_eq …)) + ##] + ##] + ##] +nqed. + +nlemma neq_to_nbfoldrightnelist2 + : ∀T:Type.∀f:T → T → bool.∀l1,l2:ne_list T. + (∀x,y:T.decidable (x = y)) → + (∀x,y.(x ≠ y → f x y = false)) → + (l1 ≠ l2 → bfold_right_neList2 T f l1 l2 = false). + #T; #f; #l1; + nelim l1; + ##[ ##1: #hh1; #l2; ncases l2; + ##[ ##1: #hh2; #H; #H1; nnormalize; #H2; napply (H1 hh1 hh2 ?); + nnormalize; #H3; nrewrite > H3 in H2:(%); #H2; napply (H2 (refl_eq …)) + ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; #H2; napply refl_eq + ##] + ##| ##2: #hh1; #ll1; #H; #l2; ncases l2; + ##[ ##1: #hh2; #H1; #H2; nnormalize; #H3; napply refl_eq + ##| ##2: #hh2; #ll2; #H1; #H2; #H3; + nchange with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = false); + napply (or2_elim (hh1 ≠ hh2) (ll1 ≠ ll2) ? (nelist_destruct T H1 … H3) …); + ##[ ##1: #H4; nrewrite > (H2 hh1 hh2 H4); nnormalize; napply refl_eq + ##| ##2: #H4; nrewrite > (H ll2 H1 H2 H4); + nrewrite > (symmetric_andbool (f hh1 hh2) false); + nnormalize; napply refl_eq + ##] + ##] ##] nqed. diff --git a/helm/software/matita/contribs/ng_assembly/common/nat_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/nat_lemmas.ma index 4bfc4c118..bbce188e5 100644 --- a/helm/software/matita/contribs/ng_assembly/common/nat_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/common/nat_lemmas.ma @@ -88,7 +88,7 @@ nlemma eq_to_eqnat : ∀n1,n2:nat.n1 = n2 → eq_nat n1 n2 = true. napply (H n4 (nat_destruct_S_S … H1)) ##] ##] -nqed. +nqed. nlemma eqnat_to_eq : ∀n1,n2:nat.(eq_nat n1 n2 = true → n1 = n2). #n1; @@ -110,6 +110,56 @@ nlemma eqnat_to_eq : ∀n1,n2:nat.(eq_nat n1 n2 = true → n1 = n2). ##] nqed. +nlemma decidable_nat : ∀x,y:nat.decidable (x = y). + #x; nelim x; nnormalize; + ##[ ##1: #y; ncases y; + ##[ ##1: napply (or2_intro1 (O = O) (O ≠ O) (refl_eq …)) + ##| ##2: #n2; napply (or2_intro2 (O = (S n2)) (O ≠ (S n2)) ?); + nnormalize; #H; napply (nat_destruct_0_S n2 H) + ##] + ##| ##2: #n1; #H; #y; ncases y; + ##[ ##1: napply (or2_intro2 ((S n1) = O) ((S n1) ≠ O) ?); + nnormalize; #H1; napply (nat_destruct_S_0 n1 H1) + ##| ##2: #n2; napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (H n2) …); + ##[ ##1: #H1; napply (or2_intro1 (? = ?) (? ≠ ?) …); + nrewrite > H1; napply refl_eq + ##| ##2: #H1; napply (or2_intro2 (? = ?) (? ≠ ?) …); + nnormalize; #H2; napply (H1 (nat_destruct_S_S … H2)) + ##] + ##] + ##] +nqed. + +nlemma neq_to_neqnat : ∀n1,n2:nat.n1 ≠ n2 → eq_nat n1 n2 = false. + #n1; nelim n1; + ##[ ##1: #n2; ncases n2; + ##[ ##1: nnormalize; #H; nelim (H (refl_eq …)) + ##| ##2: #nn2; #H; nnormalize; napply refl_eq + ##] + ##| ##2: #nn1; #H; #n2; ncases n2; + ##[ ##1: #H1; nnormalize; napply refl_eq + ##| ##2: #nn2; nnormalize; #H1; + napply (H nn2 ?); nnormalize; #H2; + nrewrite > H2 in H1:(%); #H1; + napply (H1 (refl_eq …)) + ##] + ##] +nqed. + +nlemma neqnat_to_neq : ∀n1,n2:nat.(eq_nat n1 n2 = false → n1 ≠ n2). + #n1; nelim n1; + ##[ ##1: #n2; ncases n2; + ##[ ##1: nnormalize; #H; napply (bool_destruct … H) + ##| ##2: #nn2; nnormalize; #H; #H1; nelim (nat_destruct_0_S … H1) + ##] + ##| ##2: #nn1; #H; #n2; ncases n2; + ##[ ##1: nnormalize; #H1; #H2; nelim (nat_destruct_S_0 … H2) + ##| ##2: #nn2; nnormalize; #H1; #H2; napply (H nn2 H1 ?); + napply (nat_destruct_S_S … H2) + ##] + ##] +nqed. + nlemma Sn_p_n_to_S_npn : ∀n1,n2.(S n1) + n2 = S (n1 + n2). #n1; nelim n1; 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 303d11ad3..c8942ae6c 100644 --- a/helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma @@ -99,3 +99,58 @@ nlemma eqoption_to_eq : napply refl_eq ##] nqed. + +nlemma decidable_option : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀x,y:option T.decidable (x = y). + #T; #H; #x; nelim x; + ##[ ##1: #y; ncases y; + ##[ ##1: nnormalize; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …)) + ##| ##2: #yy; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?); + nnormalize; #H1; napply (option_destruct_none_some T … H1) + ##] + ##| ##2: #xx; #y; ncases y; + ##[ ##1: nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?); + nnormalize; #H2; napply (option_destruct_some_none T … H2) + ##| ##2: #yy; nnormalize; napply (or2_elim (xx = yy) (xx ≠ yy) ? (H …)); + ##[ ##2: #H1; napply (or2_intro2 (? = ?) (? ≠ ?) ?); + nnormalize; #H2; napply (H1 (option_destruct_some_some T … H2)) + ##| ##1: #H1; napply (or2_intro1 (? = ?) (? ≠ ?) ?); + nrewrite > H1; 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; nelim op1; + ##[ ##1: #op2; ncases op2; + ##[ ##1: nnormalize; #f; #H; #H1; nelim (H1 (refl_eq …)) + ##| ##2: #yy; #f; #H; nnormalize; #H1; napply refl_eq + ##] + ##| ##2: #xx; #op2; ncases op2; + ##[ ##1: #f; #H; nnormalize; #H1; napply refl_eq + ##| ##2: #yy; #f; #H; nnormalize; #H1; napply (H xx yy …); + nnormalize; #H2; nrewrite > H2 in H1:(%); #H1; + napply (H1 (refl_eq …)) + ##] + ##] +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; nelim op1; + ##[ ##1: #op2; ncases op2; + ##[ ##1: nnormalize; #f; #H; #H1; napply (bool_destruct … H1) + ##| ##2: #yy; #f; #H; nnormalize; #H1; #H2; napply (option_destruct_none_some T … H2) + ##] + ##| ##2: #xx; #op2; ncases op2; + ##[ ##1: nnormalize; #f; #H; #H1; #H2; napply (option_destruct_some_none T … H2) + ##| ##2: #yy; #f; #H; nnormalize; #H1; #H2; napply (H xx yy H1 ?); + napply (option_destruct_some_some T … H2) + ##] + ##] +nqed. diff --git a/helm/software/matita/contribs/ng_assembly/common/prod_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/prod_lemmas.ma index 8ebed668a..15afe0a68 100644 --- a/helm/software/matita/contribs/ng_assembly/common/prod_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/common/prod_lemmas.ma @@ -23,9 +23,9 @@ include "common/prod.ma". include "num/bool_lemmas.ma". -(* ***** *) -(* TUPLE *) -(* ***** *) +(* ********* *) +(* TUPLE x 2 *) +(* ********* *) nlemma pair_destruct_1 : ∀T1,T2.∀x1,x2:T1.∀y1,y2:T2. @@ -70,8 +70,8 @@ nqed. nlemma eq_to_eqpair : ∀T1,T2.∀p1,p2:ProdT T1 T2. ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool. - (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) → - (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) → + (∀x,y:T1.x = y → f1 x y = true) → + (∀x,y:T2.x = y → f2 x y = true) → (p1 = p2 → eq_pair T1 T2 p1 p2 f1 f2 = true). #T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2; nelim p1; @@ -88,8 +88,8 @@ nqed. nlemma eqpair_to_eq : ∀T1,T2.∀p1,p2:ProdT T1 T2. ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool. - (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) → - (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) → + (∀x,y:T1.f1 x y = true → x = y) → + (∀x,y:T2.f2 x y = true → x = y) → (eq_pair T1 T2 p1 p2 f1 f2 = true → p1 = p2). #T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2; nelim p1; @@ -108,6 +108,87 @@ nlemma eqpair_to_eq : napply refl_eq. nqed. +nlemma decidable_pair + : ∀T1,T2. + (∀x,y:T1.decidable (x = y)) → + (∀x,y:T2.decidable (x = y)) → + ∀x,y:ProdT T1 T2.decidable (x = y). + #T1; #T2; #H; #H1; + #x; nelim x; #xx1; #xx2; + #y; nelim y; #yy1; #yy2; + nnormalize; + napply (or2_elim (xx1 = yy1) (xx1 ≠ yy1) ? (H xx1 yy1) ?); + ##[ ##1: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) ?); + nnormalize; #H3; napply (H2 (pair_destruct_1 T1 T2 … H3)) + ##| ##2: #H2; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?); + ##[ ##1: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?); + nnormalize; #H4; napply (H3 (pair_destruct_2 T1 T2 … H4)) + ##| ##2: #H3; napply (or2_intro1 (? = ?) (? ≠ ?) ?); + nrewrite > H2; nrewrite > H3; napply refl_eq + ##] + ##] +nqed. + +nlemma neqpair_to_neq : + ∀T1,T2.∀p1,p2:ProdT T1 T2. + ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool. + (∀x,y:T1.f1 x y = false → x ≠ y) → + (∀x,y:T2.f2 x y = false → x ≠ y) → + (eq_pair T1 T2 p1 p2 f1 f2 = false → p1 ≠ p2). + #T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2; + nelim p1; + #x1; #y1; + nelim p2; + #x2; #y2; + nchange with ((((f1 x1 x2) ⊗ (f2 y1 y2)) = false) → ?); #H; + nnormalize; #H3; + napply (or2_elim ((f1 x1 x2) = false) ((f2 y1 y2) = false) ? (andb_false2 … H) ?); + ##[ ##1: #H4; napply (H2 y1 y2 H4); napply (pair_destruct_2 T1 T2 … H3) + ##| ##2: #H4; napply (H1 x1 x2 H4); napply (pair_destruct_1 T1 T2 … H3) + ##] +nqed. + +nlemma pair_destruct + : ∀T1,T2. + (∀x,y:T1.decidable (x = y)) → + (∀x,y:T2.decidable (x = y)) → + ∀x1,x2:T1.∀y1,y2:T2.(pair T1 T2 x1 y1) ≠ (pair T1 T2 x2 y2) → x1 ≠ x2 ∨ y1 ≠ y2. + #T1; #T2; #H1; #H2; #x1; #x2; #y1; #y2; + nnormalize; #H; + napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?); + ##[ ##1: #H3; napply (or2_intro1 … H3) + ##| ##2: #H3; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?); + ##[ ##1: #H4; napply (or2_intro2 … H4) + ##| ##2: #H4; nrewrite > H3 in H:(%); + nrewrite > H4; #H; nelim (H (refl_eq …)) + ##] + ##] +nqed. + +nlemma neq_to_neqpair : + ∀T1,T2.∀p1,p2:ProdT T1 T2. + ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool. + (∀x,y:T1.decidable (x = y)) → + (∀x,y:T2.decidable (x = y)) → + (∀x,y:T1.x ≠ y → f1 x y = false) → + (∀x,y:T2.x ≠ y → f2 x y = false) → + (p1 ≠ p2 → eq_pair T1 T2 p1 p2 f1 f2 = false). + #T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2; #H3; #H4; + nelim p1; + #x1; #y1; + nelim p2; + #x2; #y2; #H; + nchange with (((f1 x1 x2) ⊗ (f2 y1 y2)) = false); + napply (or2_elim (x1 ≠ x2) (y1 ≠ y2) ? (pair_destruct T1 T2 H1 H2 … H) ?); + ##[ ##1: #H5; nrewrite > (H4 … H5); nrewrite > (andb_false2_2 (f1 x1 x2)); napply refl_eq + ##| ##2: #H5; nrewrite > (H3 … H5); nnormalize; napply refl_eq + ##] +nqed. + +(* ********* *) +(* TUPLE x 3 *) +(* ********* *) + nlemma triple_destruct_1 : ∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3. triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → x1 = x2. @@ -213,6 +294,106 @@ nlemma eqtriple_to_eq : napply refl_eq. nqed. +nlemma decidable_triple + : ∀T1,T2,T3. + (∀x,y:T1.decidable (x = y)) → + (∀x,y:T2.decidable (x = y)) → + (∀x,y:T3.decidable (x = y)) → + ∀x,y:Prod3T T1 T2 T3.decidable (x = y). + #T1; #T2; #T3; #H; #H1; #H2; + #x; nelim x; #xx1; #xx2; #xx3; + #y; nelim y; #yy1; #yy2; #yy3; + nnormalize; + napply (or2_elim (xx1 = yy1) (xx1 ≠ yy1) ? (H xx1 yy1) ?); + ##[ ##1: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?); + nnormalize; #H4; napply (H3 (triple_destruct_1 T1 T2 T3 … H4)) + ##| ##2: #H3; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?); + ##[ ##1: #H4; napply (or2_intro2 (? = ?) (? ≠ ?) ?); + nnormalize; #H5; napply (H4 (triple_destruct_2 T1 T2 T3 … H5)) + ##| ##2: #H4; napply (or2_elim (xx3 = yy3) (xx3 ≠ yy3) ? (H2 xx3 yy3) ?); + ##[ ##1: #H5; napply (or2_intro2 (? = ?) (? ≠ ?) ?); + nnormalize; #H6; napply (H5 (triple_destruct_3 T1 T2 T3 … H6)) + ##| ##2: #H5; napply (or2_intro1 (? = ?) (? ≠ ?) ?); + nrewrite > H3; + nrewrite > H4; + nrewrite > H5; + napply refl_eq + ##] + ##] + ##] +nqed. + +nlemma neqtriple_to_neq : + ∀T1,T2,T3.∀p1,p2:Prod3T T1 T2 T3. + ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool. + (∀x,y:T1.f1 x y = false → x ≠ y) → + (∀x,y:T2.f2 x y = false → x ≠ y) → + (∀x,y:T3.f3 x y = false → x ≠ y) → + (eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = false → p1 ≠ p2). + #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3; + nelim p1; + #x1; #y1; #z1; + nelim p2; + #x2; #y2; #z2; + nchange with ((((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2)) = false) → ?); #H; + nnormalize; #H4; + napply (or3_elim ((f1 x1 x2) = false) ((f2 y1 y2) = false) ((f3 z1 z2) = false) ? (andb_false3 … H) ?); + ##[ ##1: #H5; napply (H2 y1 y2 H5); napply (triple_destruct_2 T1 T2 T3 … H4) + ##| ##2: #H5; napply (H3 z1 z2 H5); napply (triple_destruct_3 T1 T2 T3 … H4) + ##| ##3: #H5; napply (H1 x1 x2 H5); napply (triple_destruct_1 T1 T2 T3 … H4) + ##] +nqed. + +nlemma triple_destruct + : ∀T1,T2,T3. + (∀x,y:T1.decidable (x = y)) → + (∀x,y:T2.decidable (x = y)) → + (∀x,y:T3.decidable (x = y)) → + ∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.(triple T1 T2 T3 x1 y1 z1) ≠ (triple T1 T2 T3 x2 y2 z2) → + Or3 (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2). + #T1; #T2; #T3; #H1; #H2; #H3; #x1; #x2; #y1; #y2; #z1; #z2; + nnormalize; #H; + napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?); + ##[ ##1: #H4; napply (or3_intro1 … H4) + ##| ##2: #H4; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?); + ##[ ##1: #H5; napply (or3_intro2 … H5) + ##| ##2: #H5; napply (or2_elim (z1 = z2) (z1 ≠ z2) ? (H3 z1 z2) ?); + ##[ ##1: #H6; napply (or3_intro3 … H6) + ##| ##2: #H6; nrewrite > H4 in H:(%); + nrewrite > H5; + nrewrite > H6; #H; nelim (H (refl_eq …)) + ##] + ##] + ##] +nqed. + +nlemma neq_to_neqtriple : + ∀T1,T2,T3.∀p1,p2:Prod3T T1 T2 T3. + ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool. + (∀x,y:T1.decidable (x = y)) → + (∀x,y:T2.decidable (x = y)) → + (∀x,y:T3.decidable (x = y)) → + (∀x,y:T1.x ≠ y → f1 x y = false) → + (∀x,y:T2.x ≠ y → f2 x y = false) → + (∀x,y:T3.x ≠ y → f3 x y = false) → + (p1 ≠ p2 → eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = false). + #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3; #H4; #H5; #H6; + nelim p1; + #x1; #y1; #z1; + nelim p2; + #x2; #y2; #z2; #H; + nchange with (((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2)) = false); + napply (or3_elim (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) ? (triple_destruct T1 T2 T3 H1 H2 H3 … H) ?); + ##[ ##1: #H7; nrewrite > (H5 … H7); nrewrite > (andb_false3_2 (f1 x1 x2) (f3 z1 z2)); napply refl_eq + ##| ##2: #H7; nrewrite > (H6 … H7); nrewrite > (andb_false3_3 (f1 x1 x2) (f2 y1 y2)); napply refl_eq + ##| ##3: #H7; nrewrite > (H4 … H7); nrewrite > (andb_false3_1 (f2 y1 y2) (f3 z1 z2)); napply refl_eq + ##] +nqed. + +(* ********* *) +(* TUPLE x 4 *) +(* ********* *) + nlemma quadruple_destruct_1 : ∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4. quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → x1 = x2. @@ -288,10 +469,10 @@ nqed. nlemma eq_to_eqquadruple : ∀T1,T2,T3,T4.∀p1,p2:Prod4T T1 T2 T3 T4. ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool. - (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) → - (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) → - (∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) → - (∀v1,v2:T4.v1 = v2 → f4 v1 v2 = true) → + (∀x,y:T1.x = y → f1 x y = true) → + (∀x,y:T2.x = y → f2 x y = true) → + (∀x,y:T3.x = y → f3 x y = true) → + (∀x,y:T4.x = y → f4 x y = true) → (p1 = p2 → eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = true). #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4; nelim p1; @@ -312,10 +493,10 @@ nqed. nlemma eqquadruple_to_eq : ∀T1,T2,T3,T4.∀p1,p2:Prod4T T1 T2 T3 T4. ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool. - (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) → - (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) → - (∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) → - (∀v1,v2:T4.f4 v1 v2 = true → v1 = v2) → + (∀x,y:T1.f1 x y = true → x = y) → + (∀x,y:T2.f2 x y = true → x = y) → + (∀x,y:T3.f3 x y = true → x = y) → + (∀x,y:T4.f4 x y = true → x = y) → (eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = true → p1 = p2). #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4; nelim p1; @@ -343,6 +524,124 @@ nlemma eqquadruple_to_eq : napply refl_eq. nqed. +nlemma decidable_quadruple + : ∀T1,T2,T3,T4. + (∀x,y:T1.decidable (x = y)) → + (∀x,y:T2.decidable (x = y)) → + (∀x,y:T3.decidable (x = y)) → + (∀x,y:T4.decidable (x = y)) → + ∀x,y:Prod4T T1 T2 T3 T4.decidable (x = y). + #T1; #T2; #T3; #T4; #H; #H1; #H2; #H3; + #x; nelim x; #xx1; #xx2; #xx3; #xx4; + #y; nelim y; #yy1; #yy2; #yy3; #yy4; + nnormalize; + napply (or2_elim (xx1 = yy1) (xx1 ≠ yy1) ? (H xx1 yy1) ?); + ##[ ##1: #H4; napply (or2_intro2 (? = ?) (? ≠ ?) ?); + nnormalize; #H5; napply (H4 (quadruple_destruct_1 T1 T2 T3 T4 … H5)) + ##| ##2: #H4; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?); + ##[ ##1: #H5; napply (or2_intro2 (? = ?) (? ≠ ?) ?); + nnormalize; #H6; napply (H5 (quadruple_destruct_2 T1 T2 T3 T4 … H6)) + ##| ##2: #H5; napply (or2_elim (xx3 = yy3) (xx3 ≠ yy3) ? (H2 xx3 yy3) ?); + ##[ ##1: #H6; napply (or2_intro2 (? = ?) (? ≠ ?) ?); + nnormalize; #H7; napply (H6 (quadruple_destruct_3 T1 T2 T3 T4 … H7)) + ##| ##2: #H6; napply (or2_elim (xx4 = yy4) (xx4 ≠ yy4) ? (H3 xx4 yy4) ?); + ##[ ##1: #H7; napply (or2_intro2 (? = ?) (? ≠ ?) ?); + nnormalize; #H8; napply (H7 (quadruple_destruct_4 T1 T2 T3 T4 … H8)) + ##| ##2: #H7; napply (or2_intro1 (? = ?) (? ≠ ?) ?); + nrewrite > H4; + nrewrite > H5; + nrewrite > H6; + nrewrite > H7; + napply refl_eq + ##] + ##] + ##] + ##] +nqed. + +nlemma neqquadruple_to_neq : + ∀T1,T2,T3,T4.∀p1,p2:Prod4T T1 T2 T3 T4. + ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool. + (∀x,y:T1.f1 x y = false → x ≠ y) → + (∀x,y:T2.f2 x y = false → x ≠ y) → + (∀x,y:T3.f3 x y = false → x ≠ y) → + (∀x,y:T4.f4 x y = false → x ≠ y) → + (eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = false → p1 ≠ p2). + #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4; + nelim p1; + #x1; #y1; #z1; #v1; + nelim p2; + #x2; #y2; #z2; #v2; + nchange with ((((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 v1 v2)) = false) → ?); #H; + nnormalize; #H5; + napply (or4_elim ((f1 x1 x2) = false) ((f2 y1 y2) = false) ((f3 z1 z2) = false) ((f4 v1 v2) = false) ? (andb_false4 … H) ?); + ##[ ##1: #H6; napply (H2 y1 y2 H6); napply (quadruple_destruct_2 T1 T2 T3 T4 … H5) + ##| ##2: #H6; napply (H3 z1 z2 H6); napply (quadruple_destruct_3 T1 T2 T3 T4 … H5) + ##| ##3: #H6; napply (H4 v1 v2 H6); napply (quadruple_destruct_4 T1 T2 T3 T4 … H5) + ##| ##4: #H6; napply (H1 x1 x2 H6); napply (quadruple_destruct_1 T1 T2 T3 T4 … H5) + ##] +nqed. + +nlemma quadruple_destruct + : ∀T1,T2,T3,T4. + (∀x,y:T1.decidable (x = y)) → + (∀x,y:T2.decidable (x = y)) → + (∀x,y:T3.decidable (x = y)) → + (∀x,y:T4.decidable (x = y)) → + ∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4. + (quadruple T1 T2 T3 T4 x1 y1 z1 v1) ≠ (quadruple T1 T2 T3 T4 x2 y2 z2 v2) → + Or4 (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) (v1 ≠ v2). + #T1; #T2; #T3; #T4; #H1; #H2; #H3; #H4; + #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; + nnormalize; #H; + napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?); + ##[ ##1: #H5; napply (or4_intro1 … H5) + ##| ##2: #H5; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?); + ##[ ##1: #H6; napply (or4_intro2 … H6) + ##| ##2: #H6; napply (or2_elim (z1 = z2) (z1 ≠ z2) ? (H3 z1 z2) ?); + ##[ ##1: #H7; napply (or4_intro3 … H7) + ##| ##2: #H7; napply (or2_elim (v1 = v2) (v1 ≠ v2) ? (H4 v1 v2) ?); + ##[ ##1: #H8; napply (or4_intro4 … H8) + ##| ##2: #H8; nrewrite > H5 in H:(%); + nrewrite > H6; + nrewrite > H7; + nrewrite > H8; #H; nelim (H (refl_eq …)) + ##] + ##] + ##] + ##] +nqed. + +nlemma neq_to_neqquadruple : + ∀T1,T2,T3,T4.∀p1,p2:Prod4T T1 T2 T3 T4. + ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool. + (∀x,y:T1.decidable (x = y)) → + (∀x,y:T2.decidable (x = y)) → + (∀x,y:T3.decidable (x = y)) → + (∀x,y:T4.decidable (x = y)) → + (∀x,y:T1.x ≠ y → f1 x y = false) → + (∀x,y:T2.x ≠ y → f2 x y = false) → + (∀x,y:T3.x ≠ y → f3 x y = false) → + (∀x,y:T4.x ≠ y → f4 x y = false) → + (p1 ≠ p2 → eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = false). + #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4; #H5; #H6; #H7; #H8; + nelim p1; + #x1; #y1; #z1; #v1; + nelim p2; + #x2; #y2; #z2; #v2; #H; + nchange with (((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 v1 v2)) = false); + napply (or4_elim (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) (v1 ≠ v2) ? (quadruple_destruct T1 T2 T3 T4 H1 H2 H3 H4 … H) ?); + ##[ ##1: #H9; nrewrite > (H6 … H9); nrewrite > (andb_false4_2 (f1 x1 x2) (f3 z1 z2) (f4 v1 v2)); napply refl_eq + ##| ##2: #H9; nrewrite > (H7 … H9); nrewrite > (andb_false4_3 (f1 x1 x2) (f2 y1 y2) (f4 v1 v2)); napply refl_eq + ##| ##3: #H9; nrewrite > (H8 … H9); nrewrite > (andb_false4_4 (f1 x1 x2) (f2 y1 y2) (f3 z1 z2)); napply refl_eq + ##| ##4: #H9; nrewrite > (H5 … H9); nrewrite > (andb_false4_1 (f2 y1 y2) (f3 z1 z2) (f4 v1 v2)); napply refl_eq + ##] +nqed. + +(* ********* *) +(* TUPLE x 5 *) +(* ********* *) + nlemma quintuple_destruct_1 : ∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5. quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → x1 = x2. @@ -434,11 +733,11 @@ nqed. nlemma eq_to_eqquintuple : ∀T1,T2,T3,T4,T5.∀p1,p2:Prod5T T1 T2 T3 T4 T5. ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool. - (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) → - (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) → - (∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) → - (∀v1,v2:T4.v1 = v2 → f4 v1 v2 = true) → - (∀w1,w2:T5.w1 = w2 → f5 w1 w2 = true) → + (∀x,y:T1.x = y → f1 x y = true) → + (∀x,y:T2.x = y → f2 x y = true) → + (∀x,y:T3.x = y → f3 x y = true) → + (∀x,y:T4.x = y → f4 x y = true) → + (∀x,y:T5.x = y → f5 x y = true) → (p1 = p2 → eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = true). #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5; nelim p1; @@ -461,11 +760,11 @@ nqed. nlemma eqquintuple_to_eq : ∀T1,T2,T3,T4,T5.∀p1,p2:Prod5T T1 T2 T3 T4 T5. ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool. - (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) → - (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) → - (∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) → - (∀v1,v2:T4.f4 v1 v2 = true → v1 = v2) → - (∀w1,w2:T5.f5 w1 w2 = true → w1 = w2) → + (∀x,y:T1.f1 x y = true → x = y) → + (∀x,y:T2.f2 x y = true → x = y) → + (∀x,y:T3.f3 x y = true → x = y) → + (∀x,y:T4.f4 x y = true → x = y) → + (∀x,y:T5.f5 x y = true → x = y) → (eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = true → p1 = p2). #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5; nelim p1; @@ -497,3 +796,135 @@ nlemma eqquintuple_to_eq : nrewrite > (H5 w1 w2 H9); napply refl_eq. nqed. + +nlemma decidable_quintuple + : ∀T1,T2,T3,T4,T5. + (∀x,y:T1.decidable (x = y)) → + (∀x,y:T2.decidable (x = y)) → + (∀x,y:T3.decidable (x = y)) → + (∀x,y:T4.decidable (x = y)) → + (∀x,y:T5.decidable (x = y)) → + ∀x,y:Prod5T T1 T2 T3 T4 T5.decidable (x = y). + #T1; #T2; #T3; #T4; #T5; #H; #H1; #H2; #H3; #H4; + #x; nelim x; #xx1; #xx2; #xx3; #xx4; #xx5; + #y; nelim y; #yy1; #yy2; #yy3; #yy4; #yy5; + nnormalize; + napply (or2_elim (xx1 = yy1) (xx1 ≠ yy1) ? (H xx1 yy1) ?); + ##[ ##1: #H5; napply (or2_intro2 (? = ?) (? ≠ ?) ?); + nnormalize; #H6; napply (H5 (quintuple_destruct_1 T1 T2 T3 T4 T5 … H6)) + ##| ##2: #H5; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?); + ##[ ##1: #H6; napply (or2_intro2 (? = ?) (? ≠ ?) ?); + nnormalize; #H7; napply (H6 (quintuple_destruct_2 T1 T2 T3 T4 T5 … H7)) + ##| ##2: #H6; napply (or2_elim (xx3 = yy3) (xx3 ≠ yy3) ? (H2 xx3 yy3) ?); + ##[ ##1: #H7; napply (or2_intro2 (? = ?) (? ≠ ?) ?); + nnormalize; #H8; napply (H7 (quintuple_destruct_3 T1 T2 T3 T4 T5 … H8)) + ##| ##2: #H7; napply (or2_elim (xx4 = yy4) (xx4 ≠ yy4) ? (H3 xx4 yy4) ?); + ##[ ##1: #H8; napply (or2_intro2 (? = ?) (? ≠ ?) ?); + nnormalize; #H9; napply (H8 (quintuple_destruct_4 T1 T2 T3 T4 T5 … H9)) + ##| ##2: #H8; napply (or2_elim (xx5 = yy5) (xx5 ≠ yy5) ? (H4 xx5 yy5) ?); + ##[ ##1: #H9; napply (or2_intro2 (? = ?) (? ≠ ?) ?); + nnormalize; #H10; napply (H9 (quintuple_destruct_5 T1 T2 T3 T4 T5 … H10)) + ##| ##2: #H9; napply (or2_intro1 (? = ?) (? ≠ ?) ?); + nrewrite > H5; + nrewrite > H6; + nrewrite > H7; + nrewrite > H8; + nrewrite > H9; + napply refl_eq + ##] + ##] + ##] + ##] + ##] +nqed. + +nlemma neqquintuple_to_neq : + ∀T1,T2,T3,T4,T5.∀p1,p2:Prod5T T1 T2 T3 T4 T5. + ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool. + (∀x,y:T1.f1 x y = false → x ≠ y) → + (∀x,y:T2.f2 x y = false → x ≠ y) → + (∀x,y:T3.f3 x y = false → x ≠ y) → + (∀x,y:T4.f4 x y = false → x ≠ y) → + (∀x,y:T5.f5 x y = false → x ≠ y) → + (eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = false → p1 ≠ p2). + #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5; + nelim p1; + #x1; #y1; #z1; #v1; #w1; + nelim p2; + #x2; #y2; #z2; #v2; #w2; + nchange with ((((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 v1 v2) ⊗ (f5 w1 w2)) = false) → ?); #H; + nnormalize; #H6; + napply (or5_elim ((f1 x1 x2) = false) ((f2 y1 y2) = false) ((f3 z1 z2) = false) ((f4 v1 v2) = false) ((f5 w1 w2) = false) ? (andb_false5 … H) ?); + ##[ ##1: #H7; napply (H2 y1 y2 H7); napply (quintuple_destruct_2 T1 T2 T3 T4 T5 … H6) + ##| ##2: #H7; napply (H3 z1 z2 H7); napply (quintuple_destruct_3 T1 T2 T3 T4 T5 … H6) + ##| ##3: #H7; napply (H4 v1 v2 H7); napply (quintuple_destruct_4 T1 T2 T3 T4 T5 … H6) + ##| ##4: #H7; napply (H5 w1 w2 H7); napply (quintuple_destruct_5 T1 T2 T3 T4 T5 … H6) + ##| ##5: #H7; napply (H1 x1 x2 H7); napply (quintuple_destruct_1 T1 T2 T3 T4 T5 … H6) + ##] +nqed. + +nlemma quintuple_destruct + : ∀T1,T2,T3,T4,T5. + (∀x,y:T1.decidable (x = y)) → + (∀x,y:T2.decidable (x = y)) → + (∀x,y:T3.decidable (x = y)) → + (∀x,y:T4.decidable (x = y)) → + (∀x,y:T5.decidable (x = y)) → + ∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5. + (quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1) ≠ (quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2) → + Or5 (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) (v1 ≠ v2) (w1 ≠ w2). + #T1; #T2; #T3; #T4; #T5; #H1; #H2; #H3; #H4; #H5; + #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2; + nnormalize; #H; + napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?); + ##[ ##1: #H6; napply (or5_intro1 … H6) + ##| ##2: #H6; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?); + ##[ ##1: #H7; napply (or5_intro2 … H7) + ##| ##2: #H7; napply (or2_elim (z1 = z2) (z1 ≠ z2) ? (H3 z1 z2) ?); + ##[ ##1: #H8; napply (or5_intro3 … H8) + ##| ##2: #H8; napply (or2_elim (v1 = v2) (v1 ≠ v2) ? (H4 v1 v2) ?); + ##[ ##1: #H9; napply (or5_intro4 … H9) + ##| ##2: #H9; napply (or2_elim (w1 = w2) (w1 ≠ w2) ? (H5 w1 w2) ?); + ##[ ##1: #H10; napply (or5_intro5 … H10) + ##| ##2: #H10; nrewrite > H6 in H:(%); + nrewrite > H7; + nrewrite > H8; + nrewrite > H9; + nrewrite > H10; #H; nelim (H (refl_eq …)) + ##] + ##] + ##] + ##] + ##] +nqed. + +nlemma neq_to_neqquintuple : + ∀T1,T2,T3,T4,T5.∀p1,p2:Prod5T T1 T2 T3 T4 T5. + ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool. + (∀x,y:T1.decidable (x = y)) → + (∀x,y:T2.decidable (x = y)) → + (∀x,y:T3.decidable (x = y)) → + (∀x,y:T4.decidable (x = y)) → + (∀x,y:T5.decidable (x = y)) → + (∀x,y:T1.x ≠ y → f1 x y = false) → + (∀x,y:T2.x ≠ y → f2 x y = false) → + (∀x,y:T3.x ≠ y → f3 x y = false) → + (∀x,y:T4.x ≠ y → f4 x y = false) → + (∀x,y:T5.x ≠ y → f5 x y = false) → + (p1 ≠ p2 → eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = false). + #T1; #T2; #T3; #T4; #T5; #p1; #p2; + #f1; #f2; #f3; #f4; #f5; + #H1; #H2; #H3; #H4; #H5; #H6; #H7; #H8; #H9; #H10; + nelim p1; + #x1; #y1; #z1; #v1; #w1; + nelim p2; + #x2; #y2; #z2; #v2; #w2; #H; + nchange with (((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 v1 v2) ⊗ (f5 w1 w2)) = false); + napply (or5_elim (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) (v1 ≠ v2) (w1 ≠ w2) ? (quintuple_destruct T1 T2 T3 T4 T5 H1 H2 H3 H4 H5 … H) ?); + ##[ ##1: #H11; nrewrite > (H7 … H11); nrewrite > (andb_false5_2 (f1 x1 x2) (f3 z1 z2) (f4 v1 v2) (f5 w1 w2)); napply refl_eq + ##| ##2: #H11; nrewrite > (H8 … H11); nrewrite > (andb_false5_3 (f1 x1 x2) (f2 y1 y2) (f4 v1 v2) (f5 w1 w2)); napply refl_eq + ##| ##3: #H11; nrewrite > (H9 … H11); nrewrite > (andb_false5_4 (f1 x1 x2) (f2 y1 y2) (f3 z1 z2) (f5 w1 w2)); napply refl_eq + ##| ##4: #H11; nrewrite > (H10 … H11); nrewrite > (andb_false5_5 (f1 x1 x2) (f2 y1 y2) (f3 z1 z2) (f4 v1 v2)); napply refl_eq + ##| ##5: #H11; nrewrite > (H6 … H11); nrewrite > (andb_false5_1 (f2 y1 y2) (f3 z1 z2) (f4 v1 v2) (f5 w1 w2)); napply refl_eq + ##] +nqed. diff --git a/helm/software/matita/contribs/ng_assembly/common/string_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/string_lemmas.ma index 7429ab70b..170581a67 100755 --- a/helm/software/matita/contribs/ng_assembly/common/string_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/common/string_lemmas.ma @@ -22,6 +22,9 @@ include "common/string.ma". include "common/ascii_lemmas2.ma". +include "common/ascii_lemmas3.ma". +include "common/ascii_lemmas4.ma". +include "common/ascii_lemmas5.ma". include "common/list_utility_lemmas.ma". (* ************************ *) @@ -43,6 +46,25 @@ nlemma eq_to_eqstr : ∀s,s'.s = s' → eq_str s s' = true. napply (eq_to_bfoldrightlist2 ascii eq_ascii s1 s2 eq_to_eqascii). nqed. +nlemma decidable_str : ∀x,y:list ascii.decidable (x = y). + napply (decidable_list ascii …); + napply decidable_ascii. +nqed. + +nlemma neqstr_to_neq : ∀s,s'.eq_str s s' = false → s ≠ s'. + #s1; #s2; + napply (nbfoldrightlist2_to_neq ascii eq_ascii s1 s2 …); + napply neqascii_to_neq. +nqed. + +nlemma neq_to_neqstr : ∀s,s'.s ≠ s' → eq_str s s' = false. + #s1; #s2; + napply (neq_to_nbfoldrightlist2 ascii eq_ascii s1 s2 …); + ##[ ##1: napply decidable_ascii + ##| ##2: napply neq_to_neqascii + ##] +nqed. + (* ************ *) (* STRINGA + ID *) (* ************ *) @@ -99,3 +121,66 @@ nlemma eq_to_eqstrid : ∀s,s'.s = s' → eq_strId s s' = true. nnormalize; napply refl_eq. nqed. + +nlemma decidable_strid_aux1 : ∀s1,n1,s2,n2.s1 ≠ s2 → (mk_strId s1 n1) ≠ (mk_strId s2 n2). + #s1; #n1; #s2; #n2; + nnormalize; #H; #H1; + napply (H (strid_destruct_1 … H1)). +nqed. + +nlemma decidable_strid_aux2 : ∀s1,n1,s2,n2.n1 ≠ n2 → (mk_strId s1 n1) ≠ (mk_strId s2 n2). + #s1; #n1; #s2; #n2; + nnormalize; #H; #H1; + napply (H (strid_destruct_2 … H1)). +nqed. + +nlemma decidable_strid : ∀x,y:strId.decidable (x = y). + #x; nelim x; #s1; #n1; + #y; nelim y; #s2; #n2; + nnormalize; + napply (or2_elim (s1 = s2) (s1 ≠ s2) ? (decidable_str s1 s2) …); + ##[ ##2: #H; napply (or2_intro2 … (decidable_strid_aux1 … H)) + ##| ##1: #H; napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_nat n1 n2) …); + ##[ ##2: #H1; napply (or2_intro2 … (decidable_strid_aux2 … H1)) + ##| ##1: #H1; nrewrite > H; nrewrite > H1; + napply (or2_intro1 … (refl_eq ? (mk_strId s2 n2))) + ##] + ##] +nqed. + +nlemma neqstrid_to_neq : ∀sid1,sid2:strId.(eq_strId sid1 sid2 = false) → (sid1 ≠ sid2). + #sid1; nelim sid1; #s1; #n1; + #sid2; nelim sid2; #s2; #n2; + nchange with ((((eq_str s1 s2) ⊗ (eq_nat n1 n2)) = false) → ?); + #H; + napply (or2_elim ((eq_str s1 s2) = false) ((eq_nat n1 n2) = false) ? (andb_false … H) …); + ##[ ##1: #H1; napply (decidable_strid_aux1 … (neqstr_to_neq … H1)) + ##| ##2: #H1; napply (decidable_strid_aux2 … (neqnat_to_neq … H1)) + ##] +nqed. + +nlemma strid_destruct : ∀s1,s2,n1,n2.(mk_strId s1 n1) ≠ (mk_strId s2 n2) → s1 ≠ s2 ∨ n1 ≠ n2. + #s1; #s2; #n1; #n2; + nnormalize; #H; + napply (or2_elim (s1 = s2) (s1 ≠ s2) ? (decidable_str s1 s2) …); + ##[ ##2: #H1; napply (or2_intro1 … H1) + ##| ##1: #H1; napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_nat n1 n2) …); + ##[ ##2: #H2; napply (or2_intro2 … H2) + ##| ##1: #H2; nrewrite > H1 in H:(%); + nrewrite > H2; + #H; nelim (H (refl_eq …)) + ##] + ##] +nqed. + +nlemma neq_to_neqstrid : ∀sid1,sid2.sid1 ≠ sid2 → eq_strId sid1 sid2 = false. + #sid1; nelim sid1; #s1; #n1; + #sid2; nelim sid2; #s2; #n2; + #H; nchange with (((eq_str s1 s2) ⊗ (eq_nat n1 n2)) = false); + napply (or2_elim (s1 ≠ s2) (n1 ≠ n2) ? (strid_destruct … H) …); + ##[ ##1: #H1; nrewrite > (neq_to_neqstr … H1); nnormalize; napply refl_eq + ##| ##2: #H1; nrewrite > (neq_to_neqnat … H1); + nrewrite > (symmetric_andbool (eq_str s1 s2) false); + nnormalize; napply refl_eq + ##] +nqed. diff --git a/helm/software/matita/contribs/ng_assembly/common/theory.ma b/helm/software/matita/contribs/ng_assembly/common/theory.ma index bb1358926..c4bd19f16 100644 --- a/helm/software/matita/contribs/ng_assembly/common/theory.ma +++ b/helm/software/matita/contribs/ng_assembly/common/theory.ma @@ -57,37 +57,171 @@ nlemma prop_to_nnprop : ∀P.P → ¬¬P. napply (H1 H). nqed. -ninductive And (A,B:Prop) : Prop ≝ - conj : A → B → (And A B). +ninductive And2 (A,B:Prop) : Prop ≝ + conj2 : A → B → (And2 A B). -interpretation "logical and" 'and x y = (And x y). +interpretation "logical and" 'and x y = (And2 x y). -nlemma proj1: ∀A,B:Prop.A ∧ B → A. +nlemma proj2_1: ∀A,B:Prop.A ∧ B → A. #A; #B; #H; - (* \ldots al posto di ??? *) - napply (And_ind A B … H); + napply (And2_ind A B … H); #H1; #H2; napply H1. nqed. -nlemma proj2: ∀A,B:Prop.A ∧ B → B. +nlemma proj2_2: ∀A,B:Prop.A ∧ B → B. #A; #B; #H; - napply (And_ind A B … H); + napply (And2_ind A B … H); #H1; #H2; napply H2. nqed. -ninductive Or (A,B:Prop) : Prop ≝ - or_introl : A → (Or A B) -| or_intror : B → (Or A B). +ninductive And3 (A,B,C:Prop) : Prop ≝ + conj3 : A → B → C → (And3 A B C). -interpretation "logical or" 'or x y = (Or x y). +nlemma proj3_1: ∀A,B,C:Prop.And3 A B C → A. + #A; #B; #C; #H; + napply (And3_ind A B C … H); + #H1; #H2; #H3; + napply H1. +nqed. + +nlemma proj3_2: ∀A,B,C:Prop.And3 A B C → B. + #A; #B; #C; #H; + napply (And3_ind A B C … H); + #H1; #H2; #H3; + napply H2. +nqed. + +nlemma proj3_3: ∀A,B,C:Prop.And3 A B C → C. + #A; #B; #C; #H; + napply (And3_ind A B C … H); + #H1; #H2; #H3; + napply H3. +nqed. + +ninductive And4 (A,B,C,D:Prop) : Prop ≝ + conj4 : A → B → C → D → (And4 A B C D). + +nlemma proj4_1: ∀A,B,C,D:Prop.And4 A B C D → A. + #A; #B; #C; #D; #H; + napply (And4_ind A B C D … H); + #H1; #H2; #H3; #H4; + napply H1. +nqed. + +nlemma proj4_2: ∀A,B,C,D:Prop.And4 A B C D → B. + #A; #B; #C; #D; #H; + napply (And4_ind A B C D … H); + #H1; #H2; #H3; #H4; + napply H2. +nqed. + +nlemma proj4_3: ∀A,B,C,D:Prop.And4 A B C D → C. + #A; #B; #C; #D; #H; + napply (And4_ind A B C D … H); + #H1; #H2; #H3; #H4; + napply H3. +nqed. + +nlemma proj4_4: ∀A,B,C,D:Prop.And4 A B C D → D. + #A; #B; #C; #D; #H; + napply (And4_ind A B C D … H); + #H1; #H2; #H3; #H4; + napply H4. +nqed. + +ninductive And5 (A,B,C,D,E:Prop) : Prop ≝ + conj5 : A → B → C → D → E → (And5 A B C D E). + +nlemma proj5_1: ∀A,B,C,D,E:Prop.And5 A B C D E → A. + #A; #B; #C; #D; #E; #H; + napply (And5_ind A B C D E … H); + #H1; #H2; #H3; #H4; #H5; + napply H1. +nqed. + +nlemma proj5_2: ∀A,B,C,D,E:Prop.And5 A B C D E → B. + #A; #B; #C; #D; #E; #H; + napply (And5_ind A B C D E … H); + #H1; #H2; #H3; #H4; #H5; + napply H2. +nqed. + +nlemma proj5_3: ∀A,B,C,D,E:Prop.And5 A B C D E → C. + #A; #B; #C; #D; #E; #H; + napply (And5_ind A B C D E … H); + #H1; #H2; #H3; #H4; #H5; + napply H3. +nqed. + +nlemma proj5_4: ∀A,B,C,D,E:Prop.And5 A B C D E → D. + #A; #B; #C; #D; #E; #H; + napply (And5_ind A B C D E … H); + #H1; #H2; #H3; #H4; #H5; + napply H4. +nqed. + +nlemma proj5_5: ∀A,B,C,D,E:Prop.And5 A B C D E → E. + #A; #B; #C; #D; #E; #H; + napply (And5_ind A B C D E … H); + #H1; #H2; #H3; #H4; #H5; + napply H5. +nqed. + +ninductive Or2 (A,B:Prop) : Prop ≝ + or2_intro1 : A → (Or2 A B) +| or2_intro2 : B → (Or2 A B). + +interpretation "logical or" 'or x y = (Or2 x y). ndefinition decidable : Prop → Prop ≝ λA:Prop.A ∨ ¬A. -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 ?); +nlemma or2_elim + : ∀P1,P2,Q:Prop.Or2 P1 P2 → ∀f1:P1 → Q.∀f2:P2 → Q.Q. + #P1; #P2; #Q; #H; #f1; #f2; + napply (Or2_ind P1 P2 ? f1 f2 ?); + napply H. +nqed. + +ninductive Or3 (A,B,C:Prop) : Prop ≝ + or3_intro1 : A → (Or3 A B C) +| or3_intro2 : B → (Or3 A B C) +| or3_intro3 : C → (Or3 A B C). + +nlemma or3_elim + : ∀P1,P2,P3,Q:Prop.Or3 P1 P2 P3 → ∀f1:P1 → Q.∀f2:P2 → Q.∀f3:P3 → Q.Q. + #P1; #P2; #P3; #Q; #H; #f1; #f2; #f3; + napply (Or3_ind P1 P2 P3 ? f1 f2 f3 ?); + napply H. +nqed. + +ninductive Or4 (A,B,C,D:Prop) : Prop ≝ + or4_intro1 : A → (Or4 A B C D) +| or4_intro2 : B → (Or4 A B C D) +| or4_intro3 : C → (Or4 A B C D) +| or4_intro4 : D → (Or4 A B C D). + +nlemma or4_elim + : ∀P1,P2,P3,P4,Q:Prop.Or4 P1 P2 P3 P4 → ∀f1:P1 → Q.∀f2:P2 → Q. + ∀f3:P3 → Q.∀f4:P4 → Q.Q. + #P1; #P2; #P3; #P4; #Q; #H; #f1; #f2; #f3; #f4; + napply (Or4_ind P1 P2 P3 P4 ? f1 f2 f3 f4 ?); + napply H. +nqed. + +ninductive Or5 (A,B,C,D,E:Prop) : Prop ≝ + or5_intro1 : A → (Or5 A B C D E) +| or5_intro2 : B → (Or5 A B C D E) +| or5_intro3 : C → (Or5 A B C D E) +| or5_intro4 : D → (Or5 A B C D E) +| or5_intro5 : E → (Or5 A B C D E). + +nlemma or5_elim + : ∀P1,P2,P3,P4,P5,Q:Prop.Or5 P1 P2 P3 P4 P5 → ∀f1:P1 → Q.∀f2:P2 → Q. + ∀f3:P3 → Q.∀f4:P4 → Q.∀f5:P5 → Q.Q. + #P1; #P2; #P3; #P4; #P5; #Q; #H; #f1; #f2; #f3; #f4; #f5; + napply (Or5_ind P1 P2 P3 P4 P5 ? f1 f2 f3 f4 f5 ?); napply H. nqed. diff --git a/helm/software/matita/contribs/ng_assembly/depends b/helm/software/matita/contribs/ng_assembly/depends index 4c4e9187b..745c07a01 100644 --- a/helm/software/matita/contribs/ng_assembly/depends +++ b/helm/software/matita/contribs/ng_assembly/depends @@ -11,7 +11,7 @@ common/nat_to_num.ma common/nat.ma num/word32.ma common/nat.ma num/bool.ma freescale/opcode_base_lemmas.ma freescale/opcode_base.ma num/bool_lemmas.ma freescale_tests/medium_tests_tools.ma freescale/multivm.ma -common/string_lemmas.ma common/ascii_lemmas2.ma common/list_utility_lemmas.ma common/string.ma +common/string_lemmas.ma common/ascii_lemmas2.ma common/ascii_lemmas3.ma common/ascii_lemmas4.ma common/ascii_lemmas5.ma common/list_utility_lemmas.ma common/string.ma compiler/ast_type_lemmas.ma common/list_utility_lemmas.ma compiler/ast_type.ma num/quatern.ma num/bool.ma freescale/table_HC05_tests.ma freescale/opcode.ma freescale/table_HC05.ma diff --git a/helm/software/matita/contribs/ng_assembly/num/bitrigesim.ma b/helm/software/matita/contribs/ng_assembly/num/bitrigesim.ma index 63eae8657..18dcce4b7 100755 --- a/helm/software/matita/contribs/ng_assembly/num/bitrigesim.ma +++ b/helm/software/matita/contribs/ng_assembly/num/bitrigesim.ma @@ -64,38 +64,22 @@ ninductive bitrigesim : Type ≝ 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 ] + [ 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 *) diff --git a/helm/software/matita/contribs/ng_assembly/num/bitrigesim_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/bitrigesim_lemmas.ma index be8b1665f..812f31a9d 100755 --- a/helm/software/matita/contribs/ng_assembly/num/bitrigesim_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/num/bitrigesim_lemmas.ma @@ -414,75 +414,43 @@ 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 ] + [ 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 + ##[ ##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. @@ -653,40 +621,23 @@ nlemma eqbit_to_eq32 : ∀t2.eq_bit t1F t2 = true → t1F = t2. 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 + #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. @@ -819,301 +770,268 @@ nlemma eq_to_eqbit32 : ∀t2.t1F = t2 → eq_bit t1F t2 = true. 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 + #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. nlemma decidable_bit1 : ∀x:bitrigesim.decidable (t00 = x). #x; nnormalize; nelim x; - ##[ ##1: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) + ##[ ##1: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) ##] nqed. nlemma decidable_bit2 : ∀x:bitrigesim.decidable (t01 = x). #x; nnormalize; nelim x; - ##[ ##2: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) + ##[ ##2: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) ##] nqed. nlemma decidable_bit3 : ∀x:bitrigesim.decidable (t02 = x). #x; nnormalize; nelim x; - ##[ ##3: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) + ##[ ##3: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) ##] nqed. nlemma decidable_bit4 : ∀x:bitrigesim.decidable (t03 = x). #x; nnormalize; nelim x; - ##[ ##4: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) + ##[ ##4: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) ##] nqed. nlemma decidable_bit5 : ∀x:bitrigesim.decidable (t04 = x). #x; nnormalize; nelim x; - ##[ ##5: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) + ##[ ##5: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) ##] nqed. nlemma decidable_bit6 : ∀x:bitrigesim.decidable (t05 = x). #x; nnormalize; nelim x; - ##[ ##6: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) + ##[ ##6: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) ##] nqed. nlemma decidable_bit7 : ∀x:bitrigesim.decidable (t06 = x). #x; nnormalize; nelim x; - ##[ ##7: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) + ##[ ##7: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) ##] nqed. nlemma decidable_bit8 : ∀x:bitrigesim.decidable (t07 = x). #x; nnormalize; nelim x; - ##[ ##8: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) + ##[ ##8: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) ##] nqed. nlemma decidable_bit9 : ∀x:bitrigesim.decidable (t08 = x). #x; nnormalize; nelim x; - ##[ ##9: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) + ##[ ##9: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) ##] nqed. nlemma decidable_bit10 : ∀x:bitrigesim.decidable (t09 = x). #x; nnormalize; nelim x; - ##[ ##10: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) + ##[ ##10: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) ##] nqed. nlemma decidable_bit11 : ∀x:bitrigesim.decidable (t0A = x). #x; nnormalize; nelim x; - ##[ ##11: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) + ##[ ##11: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) ##] nqed. nlemma decidable_bit12 : ∀x:bitrigesim.decidable (t0B = x). #x; nnormalize; nelim x; - ##[ ##12: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) + ##[ ##12: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) ##] nqed. nlemma decidable_bit13 : ∀x:bitrigesim.decidable (t0C = x). #x; nnormalize; nelim x; - ##[ ##13: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) + ##[ ##13: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) ##] nqed. nlemma decidable_bit14 : ∀x:bitrigesim.decidable (t0D = x). #x; nnormalize; nelim x; - ##[ ##14: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) + ##[ ##14: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) ##] nqed. nlemma decidable_bit15 : ∀x:bitrigesim.decidable (t0E = x). #x; nnormalize; nelim x; - ##[ ##15: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) + ##[ ##15: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) ##] nqed. nlemma decidable_bit16 : ∀x:bitrigesim.decidable (t0F = x). #x; nnormalize; nelim x; - ##[ ##16: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) + ##[ ##16: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) ##] nqed. nlemma decidable_bit17 : ∀x:bitrigesim.decidable (t10 = x). #x; nnormalize; nelim x; - ##[ ##17: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) + ##[ ##17: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) ##] nqed. nlemma decidable_bit18 : ∀x:bitrigesim.decidable (t11 = x). #x; nnormalize; nelim x; - ##[ ##18: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) + ##[ ##18: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) ##] nqed. nlemma decidable_bit19 : ∀x:bitrigesim.decidable (t12 = x). #x; nnormalize; nelim x; - ##[ ##19: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) + ##[ ##19: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) ##] nqed. nlemma decidable_bit20 : ∀x:bitrigesim.decidable (t13 = x). #x; nnormalize; nelim x; - ##[ ##20: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) + ##[ ##20: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) ##] nqed. nlemma decidable_bit21 : ∀x:bitrigesim.decidable (t14 = x). #x; nnormalize; nelim x; - ##[ ##21: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) + ##[ ##21: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) ##] nqed. nlemma decidable_bit22 : ∀x:bitrigesim.decidable (t15 = x). #x; nnormalize; nelim x; - ##[ ##22: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) + ##[ ##22: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) ##] nqed. nlemma decidable_bit23 : ∀x:bitrigesim.decidable (t16 = x). #x; nnormalize; nelim x; - ##[ ##23: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) + ##[ ##23: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) ##] nqed. nlemma decidable_bit24 : ∀x:bitrigesim.decidable (t17 = x). #x; nnormalize; nelim x; - ##[ ##24: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) + ##[ ##24: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) ##] nqed. nlemma decidable_bit25 : ∀x:bitrigesim.decidable (t18 = x). #x; nnormalize; nelim x; - ##[ ##25: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) + ##[ ##25: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) ##] nqed. nlemma decidable_bit26 : ∀x:bitrigesim.decidable (t19 = x). #x; nnormalize; nelim x; - ##[ ##26: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) + ##[ ##26: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) ##] nqed. nlemma decidable_bit27 : ∀x:bitrigesim.decidable (t1A = x). #x; nnormalize; nelim x; - ##[ ##27: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) + ##[ ##27: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) ##] nqed. nlemma decidable_bit28 : ∀x:bitrigesim.decidable (t1B = x). #x; nnormalize; nelim x; - ##[ ##28: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) + ##[ ##28: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) ##] nqed. nlemma decidable_bit29 : ∀x:bitrigesim.decidable (t1C = x). #x; nnormalize; nelim x; - ##[ ##29: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) + ##[ ##29: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) ##] nqed. nlemma decidable_bit30 : ∀x:bitrigesim.decidable (t1D = x). #x; nnormalize; nelim x; - ##[ ##30: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) + ##[ ##30: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) ##] nqed. nlemma decidable_bit31 : ∀x:bitrigesim.decidable (t1E = x). #x; nnormalize; nelim x; - ##[ ##31: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) + ##[ ##31: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) ##] nqed. nlemma decidable_bit32 : ∀x:bitrigesim.decidable (t1F = x). #x; nnormalize; nelim x; - ##[ ##32: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) + ##[ ##32: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H) ##] nqed. nlemma decidable_bit : ∀x,y:bitrigesim.decidable (x = y). #x; nnormalize; nelim x; - ##[ ##1: napply decidable_bit1 - ##| ##2: napply decidable_bit2 - ##| ##3: napply decidable_bit3 - ##| ##4: napply decidable_bit4 - ##| ##5: napply decidable_bit5 - ##| ##6: napply decidable_bit6 - ##| ##7: napply decidable_bit7 - ##| ##8: napply decidable_bit8 - ##| ##9: napply decidable_bit9 - ##| ##10: napply decidable_bit10 - ##| ##11: napply decidable_bit11 - ##| ##12: napply decidable_bit12 - ##| ##13: napply decidable_bit13 - ##| ##14: napply decidable_bit14 - ##| ##15: napply decidable_bit15 - ##| ##16: napply decidable_bit16 - ##| ##17: napply decidable_bit17 - ##| ##18: napply decidable_bit18 - ##| ##19: napply decidable_bit19 - ##| ##20: napply decidable_bit20 - ##| ##21: napply decidable_bit21 - ##| ##22: napply decidable_bit22 - ##| ##23: napply decidable_bit23 - ##| ##24: napply decidable_bit24 - ##| ##25: napply decidable_bit25 - ##| ##26: napply decidable_bit26 - ##| ##27: napply decidable_bit27 - ##| ##28: napply decidable_bit28 - ##| ##29: napply decidable_bit29 - ##| ##30: napply decidable_bit30 - ##| ##31: napply decidable_bit31 - ##| ##32: napply decidable_bit32 + ##[ ##1: napply decidable_bit1 ##| ##2: napply decidable_bit2 + ##| ##3: napply decidable_bit3 ##| ##4: napply decidable_bit4 + ##| ##5: napply decidable_bit5 ##| ##6: napply decidable_bit6 + ##| ##7: napply decidable_bit7 ##| ##8: napply decidable_bit8 + ##| ##9: napply decidable_bit9 ##| ##10: napply decidable_bit10 + ##| ##11: napply decidable_bit11 ##| ##12: napply decidable_bit12 + ##| ##13: napply decidable_bit13 ##| ##14: napply decidable_bit14 + ##| ##15: napply decidable_bit15 ##| ##16: napply decidable_bit16 + ##| ##17: napply decidable_bit17 ##| ##18: napply decidable_bit18 + ##| ##19: napply decidable_bit19 ##| ##20: napply decidable_bit20 + ##| ##21: napply decidable_bit21 ##| ##22: napply decidable_bit22 + ##| ##23: napply decidable_bit23 ##| ##24: napply decidable_bit24 + ##| ##25: napply decidable_bit25 ##| ##26: napply decidable_bit26 + ##| ##27: napply decidable_bit27 ##| ##28: napply decidable_bit28 + ##| ##29: napply decidable_bit29 ##| ##30: napply decidable_bit30 + ##| ##31: napply decidable_bit31 ##| ##32: napply decidable_bit32 ##] nqed. @@ -1343,38 +1261,22 @@ nqed. nlemma neqbit_to_neq : ∀t1,t2.eq_bit t1 t2 = false → t1 ≠ t2. #t1; nelim t1; - ##[ ##1: napply neqbit_to_neq1 - ##| ##2: napply neqbit_to_neq2 - ##| ##3: napply neqbit_to_neq3 - ##| ##4: napply neqbit_to_neq4 - ##| ##5: napply neqbit_to_neq5 - ##| ##6: napply neqbit_to_neq6 - ##| ##7: napply neqbit_to_neq7 - ##| ##8: napply neqbit_to_neq8 - ##| ##9: napply neqbit_to_neq9 - ##| ##10: napply neqbit_to_neq10 - ##| ##11: napply neqbit_to_neq11 - ##| ##12: napply neqbit_to_neq12 - ##| ##13: napply neqbit_to_neq13 - ##| ##14: napply neqbit_to_neq14 - ##| ##15: napply neqbit_to_neq15 - ##| ##16: napply neqbit_to_neq16 - ##| ##17: napply neqbit_to_neq17 - ##| ##18: napply neqbit_to_neq18 - ##| ##19: napply neqbit_to_neq19 - ##| ##20: napply neqbit_to_neq20 - ##| ##21: napply neqbit_to_neq21 - ##| ##22: napply neqbit_to_neq22 - ##| ##23: napply neqbit_to_neq23 - ##| ##24: napply neqbit_to_neq24 - ##| ##25: napply neqbit_to_neq25 - ##| ##26: napply neqbit_to_neq26 - ##| ##27: napply neqbit_to_neq27 - ##| ##28: napply neqbit_to_neq28 - ##| ##29: napply neqbit_to_neq29 - ##| ##30: napply neqbit_to_neq30 - ##| ##31: napply neqbit_to_neq31 - ##| ##32: napply neqbit_to_neq32 + ##[ ##1: napply neqbit_to_neq1 ##| ##2: napply neqbit_to_neq2 + ##| ##3: napply neqbit_to_neq3 ##| ##4: napply neqbit_to_neq4 + ##| ##5: napply neqbit_to_neq5 ##| ##6: napply neqbit_to_neq6 + ##| ##7: napply neqbit_to_neq7 ##| ##8: napply neqbit_to_neq8 + ##| ##9: napply neqbit_to_neq9 ##| ##10: napply neqbit_to_neq10 + ##| ##11: napply neqbit_to_neq11 ##| ##12: napply neqbit_to_neq12 + ##| ##13: napply neqbit_to_neq13 ##| ##14: napply neqbit_to_neq14 + ##| ##15: napply neqbit_to_neq15 ##| ##16: napply neqbit_to_neq16 + ##| ##17: napply neqbit_to_neq17 ##| ##18: napply neqbit_to_neq18 + ##| ##19: napply neqbit_to_neq19 ##| ##20: napply neqbit_to_neq20 + ##| ##21: napply neqbit_to_neq21 ##| ##22: napply neqbit_to_neq22 + ##| ##23: napply neqbit_to_neq23 ##| ##24: napply neqbit_to_neq24 + ##| ##25: napply neqbit_to_neq25 ##| ##26: napply neqbit_to_neq26 + ##| ##27: napply neqbit_to_neq27 ##| ##28: napply neqbit_to_neq28 + ##| ##29: napply neqbit_to_neq29 ##| ##30: napply neqbit_to_neq30 + ##| ##31: napply neqbit_to_neq31 ##| ##32: napply neqbit_to_neq32 ##] nqed. @@ -1508,37 +1410,21 @@ nqed. nlemma neq_to_neqbit : ∀t1,t2.t1 ≠ t2 → eq_bit t1 t2 = false. #t1; nelim t1; - ##[ ##1: napply neq_to_neqbit1 - ##| ##2: napply neq_to_neqbit2 - ##| ##3: napply neq_to_neqbit3 - ##| ##4: napply neq_to_neqbit4 - ##| ##5: napply neq_to_neqbit5 - ##| ##6: napply neq_to_neqbit6 - ##| ##7: napply neq_to_neqbit7 - ##| ##8: napply neq_to_neqbit8 - ##| ##9: napply neq_to_neqbit9 - ##| ##10: napply neq_to_neqbit10 - ##| ##11: napply neq_to_neqbit11 - ##| ##12: napply neq_to_neqbit12 - ##| ##13: napply neq_to_neqbit13 - ##| ##14: napply neq_to_neqbit14 - ##| ##15: napply neq_to_neqbit15 - ##| ##16: napply neq_to_neqbit16 - ##| ##17: napply neq_to_neqbit17 - ##| ##18: napply neq_to_neqbit18 - ##| ##19: napply neq_to_neqbit19 - ##| ##20: napply neq_to_neqbit20 - ##| ##21: napply neq_to_neqbit21 - ##| ##22: napply neq_to_neqbit22 - ##| ##23: napply neq_to_neqbit23 - ##| ##24: napply neq_to_neqbit24 - ##| ##25: napply neq_to_neqbit25 - ##| ##26: napply neq_to_neqbit26 - ##| ##27: napply neq_to_neqbit27 - ##| ##28: napply neq_to_neqbit28 - ##| ##29: napply neq_to_neqbit29 - ##| ##30: napply neq_to_neqbit30 - ##| ##31: napply neq_to_neqbit31 - ##| ##32: napply neq_to_neqbit32 + ##[ ##1: napply neq_to_neqbit1 ##| ##2: napply neq_to_neqbit2 + ##| ##3: napply neq_to_neqbit3 ##| ##4: napply neq_to_neqbit4 + ##| ##5: napply neq_to_neqbit5 ##| ##6: napply neq_to_neqbit6 + ##| ##7: napply neq_to_neqbit7 ##| ##8: napply neq_to_neqbit8 + ##| ##9: napply neq_to_neqbit9 ##| ##10: napply neq_to_neqbit10 + ##| ##11: napply neq_to_neqbit11 ##| ##12: napply neq_to_neqbit12 + ##| ##13: napply neq_to_neqbit13 ##| ##14: napply neq_to_neqbit14 + ##| ##15: napply neq_to_neqbit15 ##| ##16: napply neq_to_neqbit16 + ##| ##17: napply neq_to_neqbit17 ##| ##18: napply neq_to_neqbit18 + ##| ##19: napply neq_to_neqbit19 ##| ##20: napply neq_to_neqbit20 + ##| ##21: napply neq_to_neqbit21 ##| ##22: napply neq_to_neqbit22 + ##| ##23: napply neq_to_neqbit23 ##| ##24: napply neq_to_neqbit24 + ##| ##25: napply neq_to_neqbit25 ##| ##26: napply neq_to_neqbit26 + ##| ##27: napply neq_to_neqbit27 ##| ##28: napply neq_to_neqbit28 + ##| ##29: napply neq_to_neqbit29 ##| ##30: napply neq_to_neqbit30 + ##| ##31: napply neq_to_neqbit31 ##| ##32: napply neq_to_neqbit32 ##] 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 07d9c7001..9190adda8 100755 --- a/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma @@ -137,8 +137,8 @@ nlemma decidable_bool : ∀x,y:bool.decidable (x = y). nnormalize; nelim x; nelim y; - ##[ ##1,4: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bool_destruct … H) + ##[ ##1,4: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bool_destruct … H) ##] nqed. @@ -182,17 +182,102 @@ nlemma andb_true_true_r: ∀b1,b2.(b1 ⊗ b2) = true → b2 = true. ##] nqed. -nlemma andb_false : ∀b1,b2.(b1 ⊗ b2) = false → (b1 = false) ∨ (b2 = false). +nlemma andb_false2 + : ∀b1,b2.(b1 ⊗ b2) = false → + (b1 = false) ∨ (b2 = false). #b1; #b2; ncases b1; ncases b2; nnormalize; ##[ ##1: #H; napply (bool_destruct … H) - ##| ##2,4: #H; napply (or_intror … H) - ##| ##3: #H; napply (or_introl … H) + ##| ##2,4: #H; napply (or2_intro2 … H) + ##| ##3: #H; napply (or2_intro1 … H) ##] nqed. +nlemma andb_false3 + : ∀b1,b2,b3.(b1 ⊗ b2 ⊗ b3) = false → + Or3 (b1 = false) (b2 = false) (b3 = false). + #b1; #b2; #b3; + ncases b1; + ncases b2; + ncases b3; + nnormalize; + ##[ ##1: #H; napply (bool_destruct … H) + ##| ##5,6,7,8: #H; napply (or3_intro1 … H) + ##| ##2,4: #H; napply (or3_intro3 … H) + ##| ##3: #H; napply (or3_intro2 … H) + ##] +nqed. + +nlemma andb_false4 + : ∀b1,b2,b3,b4.(b1 ⊗ b2 ⊗ b3 ⊗ b4) = false → + Or4 (b1 = false) (b2 = false) (b3 = false) (b4 = false). + #b1; #b2; #b3; #b4; + ncases b1; + ncases b2; + ncases b3; + ncases b4; + nnormalize; + ##[ ##1: #H; napply (bool_destruct … H) + ##| ##9,10,11,12,13,14,15,16: #H; napply (or4_intro1 … H) + ##| ##5,6,7,8: #H; napply (or4_intro2 … H) + ##| ##3,4: #H; napply (or4_intro3 … H) + ##| ##2: #H; napply (or4_intro4 … H) + ##] +nqed. + +nlemma andb_false5 + : ∀b1,b2,b3,b4,b5.(b1 ⊗ b2 ⊗ b3 ⊗ b4 ⊗ b5) = false → + Or5 (b1 = false) (b2 = false) (b3 = false) (b4 = false) (b5 = false). + #b1; #b2; #b3; #b4; #b5; + ncases b1; + ncases b2; + ncases b3; + ncases b4; + ncases b5; + nnormalize; + ##[ ##1: #H; napply (bool_destruct … H) + ##| ##17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #H; napply (or5_intro1 … H) + ##| ##9,10,11,12,13,14,15,16: #H; napply (or5_intro2 … H) + ##| ##5,6,7,8: #H; napply (or5_intro3 … H) + ##| ##3,4: #H; napply (or5_intro4 … H) + ##| ##2: #H; napply (or5_intro5 … H) + ##] +nqed. + +nlemma andb_false2_1 : ∀b.(false ⊗ b) = false. + #b; nnormalize; napply refl_eq. nqed. +nlemma andb_false2_2 : ∀b.(b ⊗ false) = false. + #b; nelim b; nnormalize; napply refl_eq. nqed. + +nlemma andb_false3_1 : ∀b1,b2.(false ⊗ b1 ⊗ b2) = false. + #b1; #b2; nnormalize; napply refl_eq. nqed. +nlemma andb_false3_2 : ∀b1,b2.(b1 ⊗ false ⊗ b2) = false. + #b1; #b2; nelim b1; nnormalize; napply refl_eq. nqed. +nlemma andb_false3_3 : ∀b1,b2.(b1 ⊗ b2 ⊗ false) = false. + #b1; #b2; nelim b1; nelim b2; nnormalize; napply refl_eq. nqed. + +nlemma andb_false4_1 : ∀b1,b2,b3.(false ⊗ b1 ⊗ b2 ⊗ b3) = false. + #b1; #b2; #b3; nnormalize; napply refl_eq. nqed. +nlemma andb_false4_2 : ∀b1,b2,b3.(b1 ⊗ false ⊗ b2 ⊗ b3) = false. + #b1; #b2; #b3; nelim b1; nnormalize; napply refl_eq. nqed. +nlemma andb_false4_3 : ∀b1,b2,b3.(b1 ⊗ b2 ⊗ false ⊗ b3) = false. + #b1; #b2; #b3; nelim b1; nelim b2; nnormalize; napply refl_eq. nqed. +nlemma andb_false4_4 : ∀b1,b2,b3.(b1 ⊗ b2 ⊗ b3 ⊗ false) = false. + #b1; #b2; #b3; nelim b1; nelim b2; nelim b3; nnormalize; napply refl_eq. nqed. + +nlemma andb_false5_1 : ∀b1,b2,b3,b4.(false ⊗ b1 ⊗ b2 ⊗ b3 ⊗ b4) = false. + #b1; #b2; #b3; #b4; nnormalize; napply refl_eq. nqed. +nlemma andb_false5_2 : ∀b1,b2,b3,b4.(b1 ⊗ false ⊗ b2 ⊗ b3 ⊗ b4) = false. + #b1; #b2; #b3; #b4; nelim b1; nnormalize; napply refl_eq. nqed. +nlemma andb_false5_3 : ∀b1,b2,b3,b4.(b1 ⊗ b2 ⊗ false ⊗ b3 ⊗ b4) = false. + #b1; #b2; #b3; #b4; nelim b1; nelim b2; nnormalize; napply refl_eq. nqed. +nlemma andb_false5_4 : ∀b1,b2,b3,b4.(b1 ⊗ b2 ⊗ b3 ⊗ false ⊗ b4) = false. + #b1; #b2; #b3; #b4; nelim b1; nelim b2; nelim b3; nnormalize; napply refl_eq. nqed. +nlemma andb_false5_5 : ∀b1,b2,b3,b4.(b1 ⊗ b2 ⊗ b3 ⊗ b4 ⊗ false) = false. + #b1; #b2; #b3; #b4; nelim b1; nelim b2; nelim b3; nelim b4; nnormalize; napply refl_eq. nqed. + nlemma orb_false_false_l : ∀b1,b2:bool.(b1 ⊕ b2) = false → b1 = false. #b1; #b2; ncases b1; diff --git a/helm/software/matita/contribs/ng_assembly/num/byte8_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/byte8_lemmas.ma index c71eed49b..3165dd255 100755 --- a/helm/software/matita/contribs/ng_assembly/num/byte8_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/num/byte8_lemmas.ma @@ -303,12 +303,12 @@ nlemma decidable_b8 : ∀x,y:byte8.decidable (x = y). #x; nelim x; #e1; #e2; #y; nelim y; #e3; #e4; nnormalize; - napply (or_elim (e1 = e3) (e1 ≠ e3) ? (decidable_ex e1 e3) …); - ##[ ##2: #H; napply (or_intror … (decidable_b8_aux1 e1 e2 e3 e4 H)) - ##| ##1: #H; napply (or_elim (e2 = e4) (e2 ≠ e4) ? (decidable_ex e2 e4) …); - ##[ ##2: #H1; napply (or_intror … (decidable_b8_aux2 e1 e2 e3 e4 H1)) + napply (or2_elim (e1 = e3) (e1 ≠ e3) ? (decidable_ex e1 e3) …); + ##[ ##2: #H; napply (or2_intro2 … (decidable_b8_aux1 e1 e2 e3 e4 H)) + ##| ##1: #H; napply (or2_elim (e2 = e4) (e2 ≠ e4) ? (decidable_ex e2 e4) …); + ##[ ##2: #H1; napply (or2_intro2 … (decidable_b8_aux2 e1 e2 e3 e4 H1)) ##| ##1: #H1; nrewrite > H; nrewrite > H1; - napply (or_introl … (refl_eq ? 〈e3,e4〉)) + napply (or2_intro1 … (refl_eq ? 〈e3,e4〉)) ##] ##] nqed. @@ -320,7 +320,7 @@ nlemma neqb8_to_neq : ∀b1,b2:byte8.(eq_b8 b1 b2 = false) → (b1 ≠ b2). #e1; #e2; #e3; #e4; nchange with ((((eq_ex e3 e1) ⊗ (eq_ex e4 e2)) = false) → ?); #H; - napply (or_elim ((eq_ex e3 e1) = false) ((eq_ex e4 e2) = false) ? (andb_false … H) …); + napply (or2_elim ((eq_ex e3 e1) = false) ((eq_ex e4 e2) = false) ? (andb_false … H) …); ##[ ##1: #H1; napply (decidable_b8_aux1 … (neqex_to_neq … H1)) ##| ##2: #H1; napply (decidable_b8_aux2 … (neqex_to_neq … H1)) ##] @@ -329,10 +329,10 @@ nqed. nlemma byte8_destruct : ∀e1,e2,e3,e4.〈e1,e2〉 ≠ 〈e3,e4〉 → e1 ≠ e3 ∨ e2 ≠ e4. #e1; #e2; #e3; #e4; nnormalize; #H; - napply (or_elim (e1 = e3) (e1 ≠ e3) ? (decidable_ex e1 e3) …); - ##[ ##2: #H1; napply (or_introl … H1) - ##| ##1: #H1; napply (or_elim (e2 = e4) (e2 ≠ e4) ? (decidable_ex e2 e4) …); - ##[ ##2: #H2; napply (or_intror … H2) + napply (or2_elim (e1 = e3) (e1 ≠ e3) ? (decidable_ex e1 e3) …); + ##[ ##2: #H1; napply (or2_intro1 … H1) + ##| ##1: #H1; napply (or2_elim (e2 = e4) (e2 ≠ e4) ? (decidable_ex e2 e4) …); + ##[ ##2: #H2; napply (or2_intro2 … H2) ##| ##1: #H2; nrewrite > H1 in H:(%); nrewrite > H2; #H; nelim (H (refl_eq …)) @@ -345,7 +345,7 @@ nlemma neq_to_neqb8 : ∀b1,b2.b1 ≠ b2 → eq_b8 b1 b2 = false. nelim b1; #e1; #e2; nelim b2; #e3; #e4; #H; nchange with (((eq_ex e1 e3) ⊗ (eq_ex e2 e4)) = false); - napply (or_elim (e1 ≠ e3) (e2 ≠ e4) ? (byte8_destruct … H) …); + napply (or2_elim (e1 ≠ e3) (e2 ≠ e4) ? (byte8_destruct … H) …); ##[ ##1: #H1; nrewrite > (neq_to_neqex … H1); nnormalize; napply refl_eq ##| ##2: #H1; nrewrite > (neq_to_neqex … H1); nrewrite > (symmetric_andbool (eq_ex e1 e3) false); 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 47847434e..cbb03f412 100755 --- a/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma @@ -174,42 +174,26 @@ nqed. ndefinition exadecim_destruct_aux ≝ Πe1,e2.ΠP:Prop.ΠH:e1 = e2. match e1 with - [ x0 ⇒ match e2 with [ x0 ⇒ P → P | _ ⇒ P ] - | x1 ⇒ match e2 with [ x1 ⇒ P → P | _ ⇒ P ] - | x2 ⇒ match e2 with [ x2 ⇒ P → P | _ ⇒ P ] - | x3 ⇒ match e2 with [ x3 ⇒ P → P | _ ⇒ P ] - | x4 ⇒ match e2 with [ x4 ⇒ P → P | _ ⇒ P ] - | x5 ⇒ match e2 with [ x5 ⇒ P → P | _ ⇒ P ] - | x6 ⇒ match e2 with [ x6 ⇒ P → P | _ ⇒ P ] - | x7 ⇒ match e2 with [ x7 ⇒ P → P | _ ⇒ P ] - | x8 ⇒ match e2 with [ x8 ⇒ P → P | _ ⇒ P ] - | x9 ⇒ match e2 with [ x9 ⇒ P → P | _ ⇒ P ] - | xA ⇒ match e2 with [ xA ⇒ P → P | _ ⇒ P ] - | xB ⇒ match e2 with [ xB ⇒ P → P | _ ⇒ P ] - | xC ⇒ match e2 with [ xC ⇒ P → P | _ ⇒ P ] - | xD ⇒ match e2 with [ xD ⇒ P → P | _ ⇒ P ] - | xE ⇒ match e2 with [ xE ⇒ P → P | _ ⇒ P ] - | xF ⇒ match e2 with [ xF ⇒ P → P | _ ⇒ P ] + [ x0 ⇒ match e2 with [ x0 ⇒ P → P | _ ⇒ P ] | x1 ⇒ match e2 with [ x1 ⇒ P → P | _ ⇒ P ] + | x2 ⇒ match e2 with [ x2 ⇒ P → P | _ ⇒ P ] | x3 ⇒ match e2 with [ x3 ⇒ P → P | _ ⇒ P ] + | x4 ⇒ match e2 with [ x4 ⇒ P → P | _ ⇒ P ] | x5 ⇒ match e2 with [ x5 ⇒ P → P | _ ⇒ P ] + | x6 ⇒ match e2 with [ x6 ⇒ P → P | _ ⇒ P ] | x7 ⇒ match e2 with [ x7 ⇒ P → P | _ ⇒ P ] + | x8 ⇒ match e2 with [ x8 ⇒ P → P | _ ⇒ P ] | x9 ⇒ match e2 with [ x9 ⇒ P → P | _ ⇒ P ] + | xA ⇒ match e2 with [ xA ⇒ P → P | _ ⇒ P ] | xB ⇒ match e2 with [ xB ⇒ P → P | _ ⇒ P ] + | xC ⇒ match e2 with [ xC ⇒ P → P | _ ⇒ P ] | xD ⇒ match e2 with [ xD ⇒ P → P | _ ⇒ P ] + | xE ⇒ match e2 with [ xE ⇒ P → P | _ ⇒ P ] | xF ⇒ match e2 with [ xF ⇒ P → P | _ ⇒ P ] ]. ndefinition exadecim_destruct : exadecim_destruct_aux. #e1; ncases e1; - ##[ ##1: napply exadecim_destruct1 - ##| ##2: napply exadecim_destruct2 - ##| ##3: napply exadecim_destruct3 - ##| ##4: napply exadecim_destruct4 - ##| ##5: napply exadecim_destruct5 - ##| ##6: napply exadecim_destruct6 - ##| ##7: napply exadecim_destruct7 - ##| ##8: napply exadecim_destruct8 - ##| ##9: napply exadecim_destruct9 - ##| ##10: napply exadecim_destruct10 - ##| ##11: napply exadecim_destruct11 - ##| ##12: napply exadecim_destruct12 - ##| ##13: napply exadecim_destruct13 - ##| ##14: napply exadecim_destruct14 - ##| ##15: napply exadecim_destruct15 - ##| ##16: napply exadecim_destruct16 + ##[ ##1: napply exadecim_destruct1 ##| ##2: napply exadecim_destruct2 + ##| ##3: napply exadecim_destruct3 ##| ##4: napply exadecim_destruct4 + ##| ##5: napply exadecim_destruct5 ##| ##6: napply exadecim_destruct6 + ##| ##7: napply exadecim_destruct7 ##| ##8: napply exadecim_destruct8 + ##| ##9: napply exadecim_destruct9 ##| ##10: napply exadecim_destruct10 + ##| ##11: napply exadecim_destruct11 ##| ##12: napply exadecim_destruct12 + ##| ##13: napply exadecim_destruct13 ##| ##14: napply exadecim_destruct14 + ##| ##15: napply exadecim_destruct15 ##| ##16: napply exadecim_destruct16 ##] nqed. @@ -229,25 +213,33 @@ nlemma symmetric_andex : symmetricT exadecim exadecim and_ex. napply refl_eq. nqed. +nlemma associative_andex1 : ∀e2,e3.(and_ex (and_ex x0 e2) e3) = (and_ex x0 (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_andex2 : ∀e2,e3.(and_ex (and_ex x1 e2) e3) = (and_ex x1 (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_andex3 : ∀e2,e3.(and_ex (and_ex x2 e2) e3) = (and_ex x2 (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_andex4 : ∀e2,e3.(and_ex (and_ex x3 e2) e3) = (and_ex x3 (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_andex5 : ∀e2,e3.(and_ex (and_ex x4 e2) e3) = (and_ex x4 (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_andex6 : ∀e2,e3.(and_ex (and_ex x5 e2) e3) = (and_ex x5 (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_andex7 : ∀e2,e3.(and_ex (and_ex x6 e2) e3) = (and_ex x6 (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_andex8 : ∀e2,e3.(and_ex (and_ex x7 e2) e3) = (and_ex x7 (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_andex9 : ∀e2,e3.(and_ex (and_ex x8 e2) e3) = (and_ex x8 (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_andex10 : ∀e2,e3.(and_ex (and_ex x9 e2) e3) = (and_ex x9 (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_andex11 : ∀e2,e3.(and_ex (and_ex xA e2) e3) = (and_ex xA (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_andex12 : ∀e2,e3.(and_ex (and_ex xB e2) e3) = (and_ex xB (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_andex13 : ∀e2,e3.(and_ex (and_ex xC e2) e3) = (and_ex xC (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_andex14 : ∀e2,e3.(and_ex (and_ex xD e2) e3) = (and_ex xD (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_andex15 : ∀e2,e3.(and_ex (and_ex xE e2) e3) = (and_ex xE (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_andex16 : ∀e2,e3.(and_ex (and_ex xF e2) e3) = (and_ex xF (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. + nlemma associative_andex : ∀e1,e2,e3.(and_ex (and_ex e1 e2) e3) = (and_ex e1 (and_ex e2 e3)). - #e1; #e2; #e3; - nelim e1; - ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq + #e1; nelim e1; + ##[ ##1: napply associative_andex1 ##| ##2: napply associative_andex2 + ##| ##3: napply associative_andex3 ##| ##4: napply associative_andex4 + ##| ##5: napply associative_andex5 ##| ##6: napply associative_andex6 + ##| ##7: napply associative_andex7 ##| ##8: napply associative_andex8 + ##| ##9: napply associative_andex9 ##| ##10: napply associative_andex10 + ##| ##11: napply associative_andex11 ##| ##12: napply associative_andex12 + ##| ##13: napply associative_andex13 ##| ##14: napply associative_andex14 + ##| ##15: napply associative_andex15 ##| ##16: napply associative_andex16 ##] nqed. @@ -259,25 +251,33 @@ nlemma symmetric_orex : symmetricT exadecim exadecim or_ex. napply refl_eq. nqed. +nlemma associative_orex1 : ∀e2,e3.(or_ex (or_ex x0 e2) e3) = (or_ex x0 (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_orex2 : ∀e2,e3.(or_ex (or_ex x1 e2) e3) = (or_ex x1 (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_orex3 : ∀e2,e3.(or_ex (or_ex x2 e2) e3) = (or_ex x2 (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_orex4 : ∀e2,e3.(or_ex (or_ex x3 e2) e3) = (or_ex x3 (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_orex5 : ∀e2,e3.(or_ex (or_ex x4 e2) e3) = (or_ex x4 (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_orex6 : ∀e2,e3.(or_ex (or_ex x5 e2) e3) = (or_ex x5 (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_orex7 : ∀e2,e3.(or_ex (or_ex x6 e2) e3) = (or_ex x6 (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_orex8 : ∀e2,e3.(or_ex (or_ex x7 e2) e3) = (or_ex x7 (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_orex9 : ∀e2,e3.(or_ex (or_ex x8 e2) e3) = (or_ex x8 (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_orex10 : ∀e2,e3.(or_ex (or_ex x9 e2) e3) = (or_ex x9 (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_orex11 : ∀e2,e3.(or_ex (or_ex xA e2) e3) = (or_ex xA (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_orex12 : ∀e2,e3.(or_ex (or_ex xB e2) e3) = (or_ex xB (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_orex13 : ∀e2,e3.(or_ex (or_ex xC e2) e3) = (or_ex xC (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_orex14 : ∀e2,e3.(or_ex (or_ex xD e2) e3) = (or_ex xD (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_orex15 : ∀e2,e3.(or_ex (or_ex xE e2) e3) = (or_ex xE (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_orex16 : ∀e2,e3.(or_ex (or_ex xF e2) e3) = (or_ex xF (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. + nlemma associative_orex : ∀e1,e2,e3.(or_ex (or_ex e1 e2) e3) = (or_ex e1 (or_ex e2 e3)). - #e1; #e2; #e3; - nelim e1; - ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq + #e1; nelim e1; + ##[ ##1: napply associative_orex1 ##| ##2: napply associative_orex2 + ##| ##3: napply associative_orex3 ##| ##4: napply associative_orex4 + ##| ##5: napply associative_orex5 ##| ##6: napply associative_orex6 + ##| ##7: napply associative_orex7 ##| ##8: napply associative_orex8 + ##| ##9: napply associative_orex9 ##| ##10: napply associative_orex10 + ##| ##11: napply associative_orex11 ##| ##12: napply associative_orex12 + ##| ##13: napply associative_orex13 ##| ##14: napply associative_orex14 + ##| ##15: napply associative_orex15 ##| ##16: napply associative_orex16 ##] nqed. @@ -289,25 +289,33 @@ nlemma symmetric_xorex : symmetricT exadecim exadecim xor_ex. napply refl_eq. nqed. +nlemma associative_xorex1 : ∀e2,e3.(xor_ex (xor_ex x0 e2) e3) = (xor_ex x0 (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_xorex2 : ∀e2,e3.(xor_ex (xor_ex x1 e2) e3) = (xor_ex x1 (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_xorex3 : ∀e2,e3.(xor_ex (xor_ex x2 e2) e3) = (xor_ex x2 (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_xorex4 : ∀e2,e3.(xor_ex (xor_ex x3 e2) e3) = (xor_ex x3 (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_xorex5 : ∀e2,e3.(xor_ex (xor_ex x4 e2) e3) = (xor_ex x4 (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_xorex6 : ∀e2,e3.(xor_ex (xor_ex x5 e2) e3) = (xor_ex x5 (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_xorex7 : ∀e2,e3.(xor_ex (xor_ex x6 e2) e3) = (xor_ex x6 (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_xorex8 : ∀e2,e3.(xor_ex (xor_ex x7 e2) e3) = (xor_ex x7 (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_xorex9 : ∀e2,e3.(xor_ex (xor_ex x8 e2) e3) = (xor_ex x8 (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_xorex10 : ∀e2,e3.(xor_ex (xor_ex x9 e2) e3) = (xor_ex x9 (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_xorex11 : ∀e2,e3.(xor_ex (xor_ex xA e2) e3) = (xor_ex xA (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_xorex12 : ∀e2,e3.(xor_ex (xor_ex xB e2) e3) = (xor_ex xB (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_xorex13 : ∀e2,e3.(xor_ex (xor_ex xC e2) e3) = (xor_ex xC (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_xorex14 : ∀e2,e3.(xor_ex (xor_ex xD e2) e3) = (xor_ex xD (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_xorex15 : ∀e2,e3.(xor_ex (xor_ex xE e2) e3) = (xor_ex xE (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_xorex16 : ∀e2,e3.(xor_ex (xor_ex xF e2) e3) = (xor_ex xF (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. + nlemma associative_xorex : ∀e1,e2,e3.(xor_ex (xor_ex e1 e2) e3) = (xor_ex e1 (xor_ex e2 e3)). - #e1; #e2; #e3; - nelim e1; - ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq + #e1; nelim e1; + ##[ ##1: napply associative_xorex1 ##| ##2: napply associative_xorex2 + ##| ##3: napply associative_xorex3 ##| ##4: napply associative_xorex4 + ##| ##5: napply associative_xorex5 ##| ##6: napply associative_xorex6 + ##| ##7: napply associative_xorex7 ##| ##8: napply associative_xorex8 + ##| ##9: napply associative_xorex9 ##| ##10: napply associative_xorex10 + ##| ##11: napply associative_xorex11 ##| ##12: napply associative_xorex12 + ##| ##13: napply associative_xorex13 ##| ##14: napply associative_xorex14 + ##| ##15: napply associative_xorex15 ##| ##16: napply associative_xorex16 ##] nqed. @@ -412,25 +420,33 @@ nlemma symmetric_plusex_d_d : ∀e1,e2.plus_ex_d_d e1 e2 = plus_ex_d_d e2 e1. napply refl_eq. nqed. +nlemma associative_plusex_d_d1 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d x0 e2) e3) = (plus_ex_d_d x0 (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_plusex_d_d2 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d x1 e2) e3) = (plus_ex_d_d x1 (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_plusex_d_d3 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d x2 e2) e3) = (plus_ex_d_d x2 (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_plusex_d_d4 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d x3 e2) e3) = (plus_ex_d_d x3 (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_plusex_d_d5 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d x4 e2) e3) = (plus_ex_d_d x4 (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_plusex_d_d6 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d x5 e2) e3) = (plus_ex_d_d x5 (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_plusex_d_d7 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d x6 e2) e3) = (plus_ex_d_d x6 (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_plusex_d_d8 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d x7 e2) e3) = (plus_ex_d_d x7 (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_plusex_d_d9 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d x8 e2) e3) = (plus_ex_d_d x8 (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_plusex_d_d10 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d x9 e2) e3) = (plus_ex_d_d x9 (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_plusex_d_d11 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d xA e2) e3) = (plus_ex_d_d xA (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_plusex_d_d12 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d xB e2) e3) = (plus_ex_d_d xB (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_plusex_d_d13 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d xC e2) e3) = (plus_ex_d_d xC (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_plusex_d_d14 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d xD e2) e3) = (plus_ex_d_d xD (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_plusex_d_d15 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d xE e2) e3) = (plus_ex_d_d xE (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. +nlemma associative_plusex_d_d16 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d xF e2) e3) = (plus_ex_d_d xF (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed. + nlemma associative_plusex_d_d : ∀e1,e2,e3.(plus_ex_d_d (plus_ex_d_d e1 e2) e3) = (plus_ex_d_d e1 (plus_ex_d_d e2 e3)). - #e1; #e2; #e3; - nelim e1; - ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq - ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq + #e1; nelim e1; + ##[ ##1: napply associative_plusex_d_d1 ##| ##2: napply associative_plusex_d_d2 + ##| ##3: napply associative_plusex_d_d3 ##| ##4: napply associative_plusex_d_d4 + ##| ##5: napply associative_plusex_d_d5 ##| ##6: napply associative_plusex_d_d6 + ##| ##7: napply associative_plusex_d_d7 ##| ##8: napply associative_plusex_d_d8 + ##| ##9: napply associative_plusex_d_d9 ##| ##10: napply associative_plusex_d_d10 + ##| ##11: napply associative_plusex_d_d11 ##| ##12: napply associative_plusex_d_d12 + ##| ##13: napply associative_plusex_d_d13 ##| ##14: napply associative_plusex_d_d14 + ##| ##15: napply associative_plusex_d_d15 ##| ##16: napply associative_plusex_d_d16 ##] nqed. @@ -467,8 +483,8 @@ nlemma decidable_ex : ∀x,y:exadecim.decidable (x = y). nnormalize; nelim x; nelim y; - ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (exadecim_destruct … H) + ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (exadecim_destruct … H) ##] 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 dc7e96f89..2d754d799 100755 --- a/helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma @@ -127,8 +127,8 @@ nlemma decidable_oct : ∀x,y:oct.decidable (x = y). nnormalize; nelim x; nelim y; - ##[ ##1,10,19,28,37,46,55,64: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (oct_destruct … H) + ##[ ##1,10,19,28,37,46,55,64: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (oct_destruct … H) ##] 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 d32aa0f3e..00e559ed4 100755 --- a/helm/software/matita/contribs/ng_assembly/num/quatern_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/num/quatern_lemmas.ma @@ -99,8 +99,8 @@ nlemma decidable_qu : ∀x,y:quatern.decidable (x = y). nnormalize; nelim x; nelim y; - ##[ ##1,6,11,16: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq - ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (quatern_destruct … H) + ##[ ##1,6,11,16: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq + ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (quatern_destruct … H) ##] 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 index a9c59de32..06030fffb 100755 --- a/helm/software/matita/contribs/ng_assembly/num/word16_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/num/word16_lemmas.ma @@ -342,12 +342,12 @@ nlemma decidable_w16 : ∀x,y:word16.decidable (x = y). #x; nelim x; #b1; #b2; #y; nelim y; #b3; #b4; nnormalize; - napply (or_elim (b1 = b3) (b1 ≠ b3) ? (decidable_b8 b1 b3) …); - ##[ ##2: #H; napply (or_intror … (decidable_w16_aux1 b1 b2 b3 b4 H)) - ##| ##1: #H; napply (or_elim (b2 = b4) (b2 ≠ b4) ? (decidable_b8 b2 b4) …); - ##[ ##2: #H1; napply (or_intror … (decidable_w16_aux2 b1 b2 b3 b4 H1)) + napply (or2_elim (b1 = b3) (b1 ≠ b3) ? (decidable_b8 b1 b3) …); + ##[ ##2: #H; napply (or2_intro2 … (decidable_w16_aux1 b1 b2 b3 b4 H)) + ##| ##1: #H; napply (or2_elim (b2 = b4) (b2 ≠ b4) ? (decidable_b8 b2 b4) …); + ##[ ##2: #H1; napply (or2_intro2 … (decidable_w16_aux2 b1 b2 b3 b4 H1)) ##| ##1: #H1; nrewrite > H; nrewrite > H1; - napply (or_introl … (refl_eq ? 〈b3:b4〉)) + napply (or2_intro1 … (refl_eq ? 〈b3:b4〉)) ##] ##] nqed. @@ -359,7 +359,7 @@ nlemma neqw16_to_neq : ∀w1,w2:word16.(eq_w16 w1 w2 = false) → (w1 ≠ w2). #b1; #b2; #b3; #b4; nchange with ((((eq_b8 b3 b1) ⊗ (eq_b8 b4 b2)) = false) → ?); #H; - napply (or_elim ((eq_b8 b3 b1) = false) ((eq_b8 b4 b2) = false) ? (andb_false … H) …); + napply (or2_elim ((eq_b8 b3 b1) = false) ((eq_b8 b4 b2) = false) ? (andb_false … H) …); ##[ ##1: #H1; napply (decidable_w16_aux1 … (neqb8_to_neq … H1)) ##| ##2: #H1; napply (decidable_w16_aux2 … (neqb8_to_neq … H1)) ##] @@ -368,10 +368,10 @@ nqed. nlemma word16_destruct : ∀b1,b2,b3,b4.〈b1:b2〉 ≠ 〈b3:b4〉 → b1 ≠ b3 ∨ b2 ≠ b4. #b1; #b2; #b3; #b4; nnormalize; #H; - napply (or_elim (b1 = b3) (b1 ≠ b3) ? (decidable_b8 b1 b3) …); - ##[ ##2: #H1; napply (or_introl … H1) - ##| ##1: #H1; napply (or_elim (b2 = b4) (b2 ≠ b4) ? (decidable_b8 b2 b4) …); - ##[ ##2: #H2; napply (or_intror … H2) + napply (or2_elim (b1 = b3) (b1 ≠ b3) ? (decidable_b8 b1 b3) …); + ##[ ##2: #H1; napply (or2_intro1 … H1) + ##| ##1: #H1; napply (or2_elim (b2 = b4) (b2 ≠ b4) ? (decidable_b8 b2 b4) …); + ##[ ##2: #H2; napply (or2_intro2 … H2) ##| ##1: #H2; nrewrite > H1 in H:(%); nrewrite > H2; #H; nelim (H (refl_eq …)) @@ -384,7 +384,7 @@ nlemma neq_to_neqw16 : ∀w1,w2.w1 ≠ w2 → eq_w16 w1 w2 = false. nelim w1; #b1; #b2; nelim w2; #b3; #b4; #H; nchange with (((eq_b8 b1 b3) ⊗ (eq_b8 b2 b4)) = false); - napply (or_elim (b1 ≠ b3) (b2 ≠ b4) ? (word16_destruct … H) …); + napply (or2_elim (b1 ≠ b3) (b2 ≠ b4) ? (word16_destruct … H) …); ##[ ##1: #H1; nrewrite > (neq_to_neqb8 … H1); nnormalize; napply refl_eq ##| ##2: #H1; nrewrite > (neq_to_neqb8 … H1); nrewrite > (symmetric_andbool (eq_b8 b1 b3) false); diff --git a/helm/software/matita/contribs/ng_assembly/num/word32_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/word32_lemmas.ma index 2bb6c0b24..7f1c9ddc8 100755 --- a/helm/software/matita/contribs/ng_assembly/num/word32_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/num/word32_lemmas.ma @@ -342,12 +342,12 @@ nlemma decidable_w32 : ∀x,y:word32.decidable (x = y). #x; nelim x; #w1; #w2; #y; nelim y; #w3; #w4; nnormalize; - napply (or_elim (w1 = w3) (w1 ≠ w3) ? (decidable_w16 w1 w3) …); - ##[ ##2: #H; napply (or_intror … (decidable_w32_aux1 w1 w2 w3 w4 H)) - ##| ##1: #H; napply (or_elim (w2 = w4) (w2 ≠ w4) ? (decidable_w16 w2 w4) …); - ##[ ##2: #H1; napply (or_intror … (decidable_w32_aux2 w1 w2 w3 w4 H1)) + napply (or2_elim (w1 = w3) (w1 ≠ w3) ? (decidable_w16 w1 w3) …); + ##[ ##2: #H; napply (or2_intro2 … (decidable_w32_aux1 w1 w2 w3 w4 H)) + ##| ##1: #H; napply (or2_elim (w2 = w4) (w2 ≠ w4) ? (decidable_w16 w2 w4) …); + ##[ ##2: #H1; napply (or2_intro2 … (decidable_w32_aux2 w1 w2 w3 w4 H1)) ##| ##1: #H1; nrewrite > H; nrewrite > H1; - napply (or_introl … (refl_eq ? 〈w3.w4〉)) + napply (or2_intro1 … (refl_eq ? 〈w3.w4〉)) ##] ##] nqed. @@ -359,7 +359,7 @@ nlemma neqw32_to_neq : ∀dw1,dw2:word32.(eq_w32 dw1 dw2 = false) → (dw1 ≠ d #w1; #w2; #w3; #w4; nchange with ((((eq_w16 w3 w1) ⊗ (eq_w16 w4 w2)) = false) → ?); #H; - napply (or_elim ((eq_w16 w3 w1) = false) ((eq_w16 w4 w2) = false) ? (andb_false … H) …); + napply (or2_elim ((eq_w16 w3 w1) = false) ((eq_w16 w4 w2) = false) ? (andb_false … H) …); ##[ ##1: #H1; napply (decidable_w32_aux1 … (neqw16_to_neq … H1)) ##| ##2: #H1; napply (decidable_w32_aux2 … (neqw16_to_neq … H1)) ##] @@ -368,10 +368,10 @@ nqed. nlemma word32_destruct : ∀w1,w2,w3,w4.〈w1.w2〉 ≠ 〈w3.w4〉 → w1 ≠ w3 ∨ w2 ≠ w4. #w1; #w2; #w3; #w4; nnormalize; #H; - napply (or_elim (w1 = w3) (w1 ≠ w3) ? (decidable_w16 w1 w3) …); - ##[ ##2: #H1; napply (or_introl … H1) - ##| ##1: #H1; napply (or_elim (w2 = w4) (w2 ≠ w4) ? (decidable_w16 w2 w4) …); - ##[ ##2: #H2; napply (or_intror … H2) + napply (or2_elim (w1 = w3) (w1 ≠ w3) ? (decidable_w16 w1 w3) …); + ##[ ##2: #H1; napply (or2_intro1 … H1) + ##| ##1: #H1; napply (or2_elim (w2 = w4) (w2 ≠ w4) ? (decidable_w16 w2 w4) …); + ##[ ##2: #H2; napply (or2_intro2 … H2) ##| ##1: #H2; nrewrite > H1 in H:(%); nrewrite > H2; #H; nelim (H (refl_eq …)) @@ -384,7 +384,7 @@ nlemma neq_to_neqw32 : ∀dw1,dw2.dw1 ≠ dw2 → eq_w32 dw1 dw2 = false. nelim dw1; #w1; #w2; nelim dw2; #w3; #w4; #H; nchange with (((eq_w16 w1 w3) ⊗ (eq_w16 w2 w4)) = false); - napply (or_elim (w1 ≠ w3) (w2 ≠ w4) ? (word32_destruct … H) …); + napply (or2_elim (w1 ≠ w3) (w2 ≠ w4) ? (word32_destruct … H) …); ##[ ##1: #H1; nrewrite > (neq_to_neqw16 … H1); nnormalize; napply refl_eq ##| ##2: #H1; nrewrite > (neq_to_neqw16 … H1); nrewrite > (symmetric_andbool (eq_w16 w1 w3) false); -- 2.39.2