(* *)
(* ********************************************************************** *)
-include "common/string_lemmas.ma".
+include "common/list_utility_lemmas.ma".
nlet rec nmember_list (T:Type) (elem:T) (f:T → T → bool) (l:list T) on l ≝
match l with
].
+(* costruttore di un sottouniverso:
+ S_EL cioe' uno qualsiasi degli elementi del sottouniverso
+ S_KO cioe' il caso impossibile
+*)
+ninductive S_UN (l:list UN) : Type ≝
+ S_EL : Πx:UN.((member_list UN x eq_UN l) = true) → (∀y.eq_UN x y = true → x = y) → S_UN l
+| S_KO : False → S_UN l.
+
+ndefinition getelem : ∀l.∀e:S_UN l.UN.
+ #l; #s; nelim s;
+ ##[ ##1: #u; #dim1; #dim2; napply u
+ ##| ##2: #F; nelim F
+ ##]
+nqed.
+
+ndefinition eq_SUN ≝ λl.λx,y:S_UN l.eq_UN (getelem ? x) (getelem ? y).
+
+ndefinition getdim1 : ∀l.∀e:S_UN l.member_list UN (getelem ? e) eq_UN l = true.
+ #l; #s; nelim s;
+ ##[ ##2: #F; nelim F
+ ##| ##1: #u; #dim1; #dim2; napply dim1
+ ##]
+nqed.
+
+ndefinition getdim2 : ∀l.∀e:S_UN l.(∀y.eq_UN (getelem ? e) y = true → (getelem ? e) = y).
+ #l; #s; nelim s;
+ ##[ ##2: #F; nelim F
+ ##| ##1: #u; #dim1; #dim2; napply dim2
+ ##]
+nqed.
+
+nlemma SUN_destruct_1
+ : ∀l.∀e1,e2.∀dim11,dim21.∀dim12,dim22.S_EL l e1 dim11 dim12 = S_EL l e2 dim21 dim22 → e1 = e2.
+ #l; #e1; #e2; #dim11; #dim21; #dim12; #dim22; #H;
+ nchange with (match S_EL l e2 dim21 dim22 with [ S_EL a _ _ ⇒ e1 = a | S_KO _ ⇒ False ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
ndefinition UN_destruct : ∀x,y.∀P:Prop.x = y → match eq_UN x y with [ true ⇒ P → P | false ⇒ P ].
#x; #y; #P; #H;
nrewrite > H;
napply (λx.x).
nqed.
+ndefinition SUN_destruct : ∀l.∀x,y:S_UN l.∀P:Prop.x = y → match eq_SUN l x y with [ true ⇒ P → P | false ⇒ P ].
+ #l; #x; nelim x;
+ ##[ ##2: #F; nelim F
+ ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
+ ##[ ##2: #F; nelim F
+ ##| ##1: #u2; #dim21; #dim22; #P;
+ nchange with (? → (match eq_UN u1 u2 with [ true ⇒ P → P | false ⇒ P ]));
+ #H; napply (UN_destruct u1 u2);
+ napply (SUN_destruct_1 l … H)
+ ##]
+ ##]
+nqed.
+
nlemma eq_to_eqUN : ∀e1,e2.e1 = e2 → eq_UN e1 e2 = true.
#e1; #e2; #H;
nrewrite > H;
napply refl_eq.
nqed.
-nlemma pippo : ∀A,B:Prop.(A → B) → ((¬B) → (¬A)).
- #A; #B; #H; nnormalize;
- #H1; #H2;
- napply (H1 (H H2)).
-nqed.
-
-nlemma pluto1 : ∀x.x = false → x ≠ true.
- #x; nelim x;
- ##[ ##1: #H; napply (bool_destruct … H)
- ##| ##2: #H; nnormalize; #H1; napply (bool_destruct … H1)
- ##]
-nqed.
-
-nlemma pluto2 : ∀x.x = true → x ≠ false.
- #x; nelim x;
- ##[ ##1: #H; nnormalize; #H1; napply (bool_destruct … H1)
- ##| ##2: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma pluto3 : ∀x.x ≠ false → x = true.
- #x; nelim x;
- ##[ ##1: #H; napply refl_eq
- ##| ##2: nnormalize; #H; nelim (H (refl_eq …))
- ##]
-nqed.
-
-nlemma pluto4 : ∀x.x ≠ true → x = false.
- #x; nelim x;
- ##[ ##1: nnormalize; #H; nelim (H (refl_eq …))
- ##| ##2: #H; napply refl_eq
+nlemma eq_to_eqSUN : ∀l.∀x,y:S_UN l.x = y → eq_SUN l x y = true.
+ #l; #x; nelim x;
+ ##[ ##2: #F; nelim F
+ ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
+ ##[ ##2: #F; nelim F
+ ##| ##1: #u2; #dim21; #dim22;
+ nchange with (? → eq_UN u1 u2 = true);
+ #H; napply (eq_to_eqUN u1 u2);
+ napply (SUN_destruct_1 l … H)
+ ##]
##]
nqed.
nlemma neqUN_to_neq : ∀e1,e2.eq_UN e1 e2 = false → e1 ≠ e2.
#e1; #e2; #H;
- napply (pippo (e1 = e2) (eq_UN e1 e2 = true) …);
+ napply (not_to_not (e1 = e2) (eq_UN e1 e2 = true) …);
##[ ##1: napply (eq_to_eqUN e1 e2)
- ##| ##2: napply (pluto1 … H)
+ ##| ##2: napply (eqfalse_to_neqtrue … H)
##]
nqed.
-naxiom eqUN_to_eq : ∀e1,e2.eq_UN e1 e2 = true → e1 = e2.
-
-nlemma neq_to_neqUN : ∀e1,e2.e1 ≠ e2 → eq_UN e1 e2 = false.
- #e1; #e2; #H;
- napply (pluto4 (eq_UN e1 e2));
- napply (pippo (eq_UN e1 e2 = true) (e1 = e2) ? H);
- napply (eqUN_to_eq e1 e2).
-nqed.
-
-nlemma decidable_UN : ∀x,y:UN.decidable (x = y).
- #x; #y; nnormalize;
- napply (or2_elim (eq_UN x y = true) (eq_UN x y = false) ?);
- ##[ ##1: ncases (eq_UN x y);
- ##[ ##1: napply (or2_intro1 (true = true) (true = false) (refl_eq …))
- ##| ##2: napply (or2_intro2 (false = true) (false = false) (refl_eq …))
+nlemma neqSUN_to_neq : ∀l.∀x,y:S_UN l.eq_SUN l x y = false → x ≠ y.
+ #l; #x; nelim x;
+ ##[ ##2: #F; nelim F
+ ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
+ ##[ ##2: #F; nelim F
+ ##| ##1: #u2; #dim21; #dim22;
+ nchange with ((eq_UN u1 u2 = false) → ?);
+ #H; nnormalize; #H1;
+ napply (neqUN_to_neq u1 u2 H);
+ napply (SUN_destruct_1 l … H1)
##]
- ##| ##2: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqUN_to_eq … H))
- ##| ##3: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqUN_to_neq … H))
##]
nqed.
- nrewrite > (eq_to_eqUN e1 e2 ?);
+naxiom SUN_construct
+ : ∀l.∀u.
+ ∀dim11,dim21:(member_list UN u eq_UN l = true).
+ ∀dim12,dim22:(∀y0.(eq_UN u y0 = true) → (u = y0)).
+ ((S_EL l u dim11 dim12) = (S_EL l u dim21 dim22)).
-nlemma eqUN_to_eq : ∀e1,e2.eq_UN e1 e2 = true → e1 = e2.
- #e1; #e2; #H;
-
-
-nlemma pippo : ∀P.(¬¬¬P) → (¬P).
- #P; nnormalize; #H; #H1;
- napply H; #H2;
- napply (H2 H1).
+nlemma eqgetelem_to_eq : ∀l.∀x,y:S_UN l.(getelem ? x) = (getelem ? y) → x = y.
+ #l; #x; nelim x;
+ ##[ ##2: #F; nelim F
+ ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
+ ##[ ##2: #F; nelim F
+ ##| ##1: #u2; #dim21; #dim22;
+ nchange with (u1 = u2 → ?); #H;
+ nrewrite > H in dim11:(%) dim12:(%) ⊢ %; #dim11; #dim12;
+ napply (SUN_construct l u2 dim11 dim21 dim12 dim22);
+ ##]
+ ##]
nqed.
-nlemma pippo2 : ∀P.(¬¬P) → P.
- #P; nnormalize; #H;
- napply (or2_elim (¬P) (¬¬¬¬P) ?);
- ##[ ##1: napply (or2_intro2 ?? (prop_to_nnprop ? H))
- ##| ##2: #H1; nelim (H H1)
- ##| ##3: #H1; napply False_ind;
- napply (H (pippo …));
- nnormalize; #H2;
- napply False_ind;
- napply (pippo ? H1);
- #H2;
- napply H;
- napply False_ind;
- napply H1; #H2;
-
- ##[ ##2: #H1;napply (prop_to_nnprop ? H);
- ##| ##1: nnormalize; #H1;
- napply False_ind;
- napply H; #H1;
- napply H;
- napply (or2_elim (¬¬P) (¬¬¬P) ?);
- ##[ ##1: napply (or2_intro1 ?? H);
-
- napply (absurd (¬¬¬P) P ??);
- ##[ ##2: napply (prop_to_nnprop ? H);
- ##| ##1:
- napply (pippo P);
- nnormalize;
- nnormalize in H:(%);
- #H1;
- #H1;
- napply (absurd ? False H ?);
- nnormalize;
- #H2;
- nnormalize; #H;
- napply False_ind;
- napply H; #H1;
- napply (absurd ? False (prop_to_nnprop (¬P) ?));
- ##[ ##1: nnormalize; #H2; napply (H2 H)
- ##| ##2:
- nnormalize; #H2;
- nnormalize in K:(%);
- # .
+nlemma neq_to_neqgetelem : ∀l.∀x,y:S_UN l.x ≠ y → (getelem ? x) ≠ (getelem ? y).
+ #l; #x; nelim x;
+ ##[ ##2: #F; nelim F
+ ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
+ ##[ ##2: #F; nelim F
+ ##| ##1: #u2; #dim21; #dim22; #H;
+ napply (not_to_not ((getelem l ?) = (getelem l ?))
+ ((S_EL l u1 dim11 dim12) = (S_EL l u2 dim21 dim22)) ?);
+ ##[ ##1: napply H
+ ##| ##2: napply (eqgetelem_to_eq l …)
+ ##]
+ ##]
+ ##]
nqed.
-nlemma eqUN_to_eq : ∀e1,e2.eq_UN e1 e2 = true → e1 = e2.
- #e1; #e2;
- napply (or2_elim (eq_UN e1 e2 = false) (e1 ≠ e2) ?);
- ##[ ##3:
- nelim e1;
- nnormalize;
- nchange with (match e2 with [ ? ⇒ true | _ ⇒ false ]);
- nelim e2;
- #H;
- napply (or2_elim (e1 = e2) (e1 ≠ e2) …);
- ##[ ##2:
-
- ##[ ##1: ncases (eq_UN e1 e2);
- ##[ ##1: napply (or2_intro1 (true = true) (true = false) (refl_eq …))
- ##| ##2: napply (or2_intro2 (false = true) (false = false) (refl_eq …))
+nlemma eqSUN_to_eq : ∀l.∀x,y:S_UN l.eq_SUN l x y = true → x = y.
+ #l; #x; nelim x;
+ ##[ ##2: #F; nelim F
+ ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
+ ##[ ##2: #F; nelim F
+ ##| ##1: #u2; #dim21; #dim22;
+ nchange with ((eq_UN u1 u2 = true) → ?); #H;
+ nrewrite > (eqgetelem_to_eq l (S_EL l u1 dim11 dim12) (S_EL l u2 dim21 dim22) (dim12 u2 H));
+ napply refl_eq
##]
- ##| ##3:
-
-
- nnormalize;
- nrewrite > H;
- nelim e2;
- nnormalize;
- napply refl_eq.
+ ##]
nqed.
-ndefinition decidable_UN1 ≝ λx.∀y:UN.decidable (x = y).
- #x;
- nnormalize;
- nelim x;
- ##[ ##1: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (UN_destruct … H)
+nlemma neq_to_neqSUN : ∀l.∀x,y:S_UN l.x ≠ y → eq_SUN l x y = false.
+ #l; #x; nelim x;
+ ##[ ##2: #F; nelim F
+ ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
+ ##[ ##2: #F; nelim F
+ ##| ##1: #u2; #dim21; #dim22; #H;
+ napply neqtrue_to_eqfalse;
+ napply (not_to_not ?? (eqSUN_to_eq l ??) ?) ;
+ napply H
+ ##]
##]
nqed.
-naxiom decidable_UN : ∀x,y:UN.decidable (x = y).
-
-nlemma neq_to_neqUN : ∀e1,e2.e1 ≠ e2 → eq_UN e1 e2 = false.
- #e1; #e2; #H;
-
-nlemma eqUN_to_eq : ∀e1,e2.eq_UN e1 e2 = true → e1 = e2.
- #e1; #e2; #H; napply (or2_elim ??? (decidable_UN e1 e2));
- ##[ ##2: #H1;
-
-nlemma pippo : ∀e1,e2:UN.decidable (e1 = e2).
- #e1; #e2; nnormalize;
- nelim e1;
- napply (or2_intro1 (? = ?) (? ≠ ?) …);
- nchange with (match e2 with [ ? ⇒ refl_eq UN ? | _ ⇒ ? ]);
- napply (destruct_UN ? e2 (? = e2) ?);
-
-nlemma pippo : ∀e1,e2.eq_UN e1 e2 = true → e1 = e2.
- #e1; nelim e1; #e2;
-
-
-(* costruttore di un sottouniverso:
- S_EL cioe' uno qualsiasi degli elementi del sottouniverso
- S_KO cioe' il caso impossibile
-*)
-ninductive S_UN (l:list UN) : Type ≝
- S_EL : Πx:UN.((member_list UN x eq_UN l) = true) →
- (∀y.x = y → (eq_UN x y = true)) →
- (∀y.(eq_UN x y = true) → x = y) →
- (∀y.decidable (x = y)) →
- (∀y.x ≠ y → (eq_UN x y = false)) →
- (∀y.(eq_UN x y = false) → x ≠ y) →
- S_UN l
-| S_KO : False → S_UN l.
-
-ndefinition SUN_create : Πl.Πe.(member_list UN e eq_UN l = true) → S_UN l.
- #l; #e; #dim; napply (S_EL l e dim …);
- ##[ ##1: #y; #H; nrewrite > H; nelim y; nnormalize; napply refl_eq
- ##| ##2: #y;
-
-(* sottoinsieme degli esadecimali *)
-ndefinition EX_UN ≝ [ ux0; ux1; ux2; ux3; ux4; ux5; ux6; ux7; ux8; ux9; uxA; uxB; uxC; uxD; uxE; uxF ].
-
-(* getter del testimone di esistenza *)
-ndefinition getelem : ∀l.∀e:S_UN l.UN.
- #l; #s; nelim s;
- ##[ ##1: #u; #H; napply u
- ##| ##2: #H; nelim H
+nlemma decidable_SUN : ∀l.∀x,y:S_UN l.decidable (x = y).
+ #l; #x; nelim x;
+ ##[ ##2: #F; nelim F
+ ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
+ ##[ ##2: #F; nelim F
+ ##| ##1: #u2; #dim21; #dim22; nnormalize;
+ napply (or2_elim … (decidable_bexpr (eq_SUN l (S_EL l u1 dim11 dim12) (S_EL l u2 dim21 dim22))));
+ ##[ ##1: #H; napply (or2_intro1 (? = ?) (? ≠ ?) (eqSUN_to_eq l … H))
+ ##| ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) (neqSUN_to_neq l … H))
##]
nqed.
-(* getter della dimostrazione di appartenenza *)
-ndefinition getdim : ∀l.∀e:S_UN l.member_list UN ? eq_UN l = true.
- ##[ ##2: nelim e;
- ##[ ##1: #u; #H; napply u
- ##| ##2: #H; nelim H
- ##]
- ##| ##1: #l; #s; nelim s;
- ##[ ##1: #u; #m; napply m
- ##| ##2: #H; nelim H
- ##]
+nlemma symmetric_eqSUN : ∀l.symmetricT (S_UN l) bool (eq_SUN l).
+ #l; #x; nelim x;
+ ##[ ##2: #F; nelim F
+ ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
+ ##[ ##2: #F; nelim F
+ ##| ##1: #u2; #dim21; #dim22;
+ napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_SUN l (S_EL l u1 dim11 dim12) (S_EL l u2 dim21 dim22)));
+ ##[ ##1: #H; nrewrite > H; napply refl_eq
+ ##| ##2: #H; nrewrite > (neq_to_neqSUN l … H);
+ napply (symmetric_eq ? (eq_SUN l ??) false);
+ napply (neq_to_neqSUN l … (symmetric_neq … H))
##]
nqed.
-(* costruttore universale di una funzione ad un solo argomento: esadecimali → esadecimali *)
+(*
+ndefinition EX_UN ≝ [ ux0; ux1; ux2; ux3; ux4; ux5; ux6; ux7; ux8; ux9; uxA; uxB; uxC; uxD; uxE; uxF ].
+
ndefinition f1_EX_UN
: ∀e:S_UN EX_UN.
∀f1,f2,f3,f4,f5,f6,f7,f8,f9,f10,f11,f12,f13,f14,f15,f16:S_UN EX_UN.
##]
nqed.
-(* esempio: successore esadecimale *)
ndefinition succ_EX_UN ≝
λe:S_UN EX_UN.f1_EX_UN
(S_EL EX_UN ux1 (refl_eq …)) (S_EL EX_UN ux2 (refl_eq …))
(S_EL EX_UN uxB (refl_eq …)) (S_EL EX_UN uxC (refl_eq …))
(S_EL EX_UN uxD (refl_eq …)) (S_EL EX_UN uxE (refl_eq …))
(S_EL EX_UN uxF (refl_eq …)) (S_EL EX_UN ux0 (refl_eq …)).
-
-(* lemmi *)
-nlemma same_UN_1 : ∀l.∀e1,e2.∀dim1,dim2.S_EL l e1 dim1 = S_EL l e2 dim2 → e1 = e2.
- #l; #e1; #e2; #dim1; #dim2; #H;
- nchange with (match S_EL l e2 dim2 with [ S_EL a _ ⇒ e1 = a | S_KO _ ⇒ False ]);
- nrewrite < H;
- nnormalize;
- napply refl_eq.
-nqed.
-
-
-
-ndefinition destruct_SUN
- : ∀l.∀e1,e2:S_UN l.∀P:Prop.
- e1 = e2 → match eq_UN (getelem ? e1) (getelem ? e2) with [ true ⇒ P → P | false ⇒ P ].
- #l; #e1; nelim e1;
- ##[ ##2: #H; nelim H
- ##| ##1: #u1; #dim1; #e2; ncases e2;
- ##[ ##2: #H; nelim H
- ##| ##1: #u2; #dim2; #P; #H;
- nchange with (match eq_UN u1 u2 with [ true ⇒ P → P | false ⇒ P ]);
- napply (destruct_UN u1 u2 P (same_UN_1 l … H))
- ##]
- ##]
-nqed.
-
-
-
-nlemma eq_to_eqSUN
- : ∀l.∀e1,e2:S_UN l.(getelem ? e1) = (getelem ? e2) → eq_UN (getelem ? e1) (getelem ? e2) = true.
- #l; #e1; nelim e1;
- ##[ ##2: #H; nelim H
- ##| ##1: #u1; #dim1; #e2; ncases e2;
- ##[ ##2: #H; nelim H;
- ##| ##1: #u2; #dim2; nchange with ((u1 = u2) → (eq_UN u1 u2 = true));
- napply (eq_to_eqUN u1 u2);
- ##]
- ##]
-nqed.
-
-nlet rec scan (T:Type) (e:T) (f:T → T → bool) (l:list T) (n:nat) on l ≝
- match l with
- [ nil ⇒ None ?
- | cons h t ⇒ match f e h with
- [ true ⇒ Some ? n
- | false ⇒ scan T e f t (S n)
- ]
- ].
-
-nlemma pippo : ∀l.∀x,y:S_UN l.x = y → scan ? (getelem ? x) eq_UN l O = scan ? (getelem ? y) eq_UN l O.
- #l; nelim l;
- ##[ ##1: #x; #y; #H; nnormalize; napply refl_eq
- ##| ##2: #hh; #tt; #H; #x; nelim x;
- ##[ ##2: #F; nelim F
- ##| ##1: #u1; #dim1; #y; nelim y;
- ##[ ##2: #F; nelim F
- ##| ##1: #u2; #dim2; #H1;
- nchange with ((scan ? u1 ???) = (scan ? u2 ???));
- nrewrite > (same_UN_1 (hh::tt) … H1);
- nchange with
- nletin K ≝ (same_UN_1 (hh::tt) … H1);
- nchange in K:(%) with (u1 = u2);
- nnormalize in K:(%);
- nrewrite > (same_UN_1 (hh::tt) … H1) in dim1:(%) dim2:(%) ⊢ %;
- nchange with (match eq_UN
-
- nchange with (scan ? u1 eq_UN ? O = scan ? u2 eq_UN ? O);
-
- #x; nelim x;
- ##[ ##2: #H; nelim H
- ##| ##1: #u1; #dim1; #y; nelim y;
- ##[ ##2: #H; nelim H
- ##| ##1: #u2; #dim2; #H; nchange with (scan ? u1 eq_UN l O = scan ? u2 eq_UN l O);
- nrewrite > (same_UN_1 l … H);
- nelim l in x:(%) dim1:(%) y:(%) dim2:(%) H:(%) ⊢ %;
- ##[ ##1: #x; #dim1; #y; #dim2; #H; nnormalize; napply refl_eq
- ##| ##2: #uu1; #ll; #H; #y;
- nnormalize;
-
-nlemma decidable_UN : ∀x,y:UN.decidable (x = y).
- #x; nnormalize; #y;
- napply (Or2_ind);
-
-
- napply (destruct_UN ? y (Or2 ??) ?);
-
-nlemma neq_to_neqUN
- : ∀l.∀e1,e2:S_UN l.(getelem ? e1) ≠ (getelem ? e2) → eq_UN (getelem ? e1) (getelem ? e2) = false.
- #l; #e1; nelim e1;
- ##[ ##2: #H; nelim H
- ##| ##1: #u1; #dim1; #e2; ncases e2;
- ##[ ##2: #H; nelim H;
- ##| ##1: #u2; #dim2; nchange with ((u1 ≠ u2) → (eq_UN u1 u2 = false));
- #H; nrewrite > H;
- nelim u2; nnormalize; napply refl_eq
- ##]
- ##]
-nqed.
-
- nelim u1 in dim1:(%) H:(%) ⊢ %; #dim1; #H;
- ##[ ##1: nelim u2 in dim2:(%) H:(%) ⊢ %; #dim2; #H;
- napply (destruct_UN l (S_EL l uq0 dim1) ?? H);
-
- ##[ ##1: nelim u2; ##[ ##1:
-
-
-ndefinition decidable_UN : ∀l.∀e1,e2:S_UN l.decidable (e1 = e2).
- #l; #e1; ncases e1;
- ##[ ##2: #H; nelim H
- ##| ##1: #u1; #dim1; #e2; ncases e2;
- ##[ ##2: #H; nelim H
- ##| ##1: #u2; #dim2; nnormalize;
- napply (or2_intro2 (? = ?) (? ≠ ?) ?);
- nnormalize;
- #H;
- nchange with (match S_EL l u1 dim1
- return λx.eq_UN x u2 → Prop
- with
- [ S_EL x _ ⇒ λp:(False
- | S_KO H ⇒ True
- ] (refl_eq ? (eq_UN u1 u2);
- nletin K ≝ (same_UN_1 l … H);
- nelim u1 in dim1:(%) H:(%) K:(%);
- #dim1; #H; #K;
- napply (destruct_UN l … H);
-
-
-
-
-
-
-
-
-
-
+*)
napply H.
nqed.
+nlemma symmetric_or2 : ∀P1,P2.Or2 P1 P2 → Or2 P2 P1.
+ #P1; #P2; #H;
+ napply (or2_elim P1 P2 ? H);
+ ##[ ##1: #H1; napply (or2_intro2 P2 P1 H1)
+ ##| ##2: #H1; napply (or2_intro1 P2 P1 H1)
+ ##]
+nqed.
+
ninductive Or3 (A,B,C:Prop) : Prop ≝
or3_intro1 : A → (Or3 A B C)
| or3_intro2 : B → (Or3 A B C)
napply H.
nqed.
+nlemma symmetric_or3_12 : ∀P1,P2,P3:Prop.Or3 P1 P2 P3 → Or3 P2 P1 P3.
+ #P1; #P2; #P3; #H;
+ napply (or3_elim P1 P2 P3 ? H);
+ ##[ ##1: #H1; napply (or3_intro2 P2 P1 P3 H1)
+ ##| ##2: #H1; napply (or3_intro1 P2 P1 P3 H1)
+ ##| ##3: #H1; napply (or3_intro3 P2 P1 P3 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or3_13 : ∀P1,P2,P3:Prop.Or3 P1 P2 P3 → Or3 P3 P2 P1.
+ #P1; #P2; #P3; #H;
+ napply (or3_elim P1 P2 P3 ? H);
+ ##[ ##1: #H1; napply (or3_intro3 P3 P2 P1 H1)
+ ##| ##2: #H1; napply (or3_intro2 P3 P2 P1 H1)
+ ##| ##3: #H1; napply (or3_intro1 P3 P2 P1 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or3_23 : ∀P1,P2,P3:Prop.Or3 P1 P2 P3 → Or3 P1 P3 P2.
+ #P1; #P2; #P3; #H;
+ napply (or3_elim P1 P2 P3 ? H);
+ ##[ ##1: #H1; napply (or3_intro1 P1 P3 P2 H1)
+ ##| ##2: #H1; napply (or3_intro3 P1 P3 P2 H1)
+ ##| ##3: #H1; napply (or3_intro2 P1 P3 P2 H1)
+ ##]
+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)
napply H.
nqed.
+nlemma symmetric_or4_12 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P2 P1 P3 P4.
+ #P1; #P2; #P3; #P4; #H;
+ napply (or4_elim P1 P2 P3 P4 ? H);
+ ##[ ##1: #H1; napply (or4_intro2 P2 P1 P3 P4 H1)
+ ##| ##2: #H1; napply (or4_intro1 P2 P1 P3 P4 H1)
+ ##| ##3: #H1; napply (or4_intro3 P2 P1 P3 P4 H1)
+ ##| ##4: #H1; napply (or4_intro4 P2 P1 P3 P4 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or4_13 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P3 P2 P1 P4.
+ #P1; #P2; #P3; #P4; #H;
+ napply (or4_elim P1 P2 P3 P4 ? H);
+ ##[ ##1: #H1; napply (or4_intro3 P3 P2 P1 P4 H1)
+ ##| ##2: #H1; napply (or4_intro2 P3 P2 P1 P4 H1)
+ ##| ##3: #H1; napply (or4_intro1 P3 P2 P1 P4 H1)
+ ##| ##4: #H1; napply (or4_intro4 P3 P2 P1 P4 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or4_14 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P4 P2 P3 P1.
+ #P1; #P2; #P3; #P4; #H;
+ napply (or4_elim P1 P2 P3 P4 ? H);
+ ##[ ##1: #H1; napply (or4_intro4 P4 P2 P3 P1 H1)
+ ##| ##2: #H1; napply (or4_intro2 P4 P2 P3 P1 H1)
+ ##| ##3: #H1; napply (or4_intro3 P4 P2 P3 P1 H1)
+ ##| ##4: #H1; napply (or4_intro1 P4 P2 P3 P1 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or4_23 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P1 P3 P2 P4.
+ #P1; #P2; #P3; #P4; #H;
+ napply (or4_elim P1 P2 P3 P4 ? H);
+ ##[ ##1: #H1; napply (or4_intro1 P1 P3 P2 P4 H1)
+ ##| ##2: #H1; napply (or4_intro3 P1 P3 P2 P4 H1)
+ ##| ##3: #H1; napply (or4_intro2 P1 P3 P2 P4 H1)
+ ##| ##4: #H1; napply (or4_intro4 P1 P3 P2 P4 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or4_24 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P1 P4 P3 P2.
+ #P1; #P2; #P3; #P4; #H;
+ napply (or4_elim P1 P2 P3 P4 ? H);
+ ##[ ##1: #H1; napply (or4_intro1 P1 P4 P3 P2 H1)
+ ##| ##2: #H1; napply (or4_intro4 P1 P4 P3 P2 H1)
+ ##| ##3: #H1; napply (or4_intro3 P1 P4 P3 P2 H1)
+ ##| ##4: #H1; napply (or4_intro2 P1 P4 P3 P2 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or4_34 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P1 P2 P4 P3.
+ #P1; #P2; #P3; #P4; #H;
+ napply (or4_elim P1 P2 P3 P4 ? H);
+ ##[ ##1: #H1; napply (or4_intro1 P1 P2 P4 P3 H1)
+ ##| ##2: #H1; napply (or4_intro2 P1 P2 P4 P3 H1)
+ ##| ##3: #H1; napply (or4_intro4 P1 P2 P4 P3 H1)
+ ##| ##4: #H1; napply (or4_intro3 P1 P2 P4 P3 H1)
+ ##]
+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)
napply H.
nqed.
+nlemma symmetric_or5_12 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P2 P1 P3 P4 P5.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro2 P2 P1 P3 P4 P5 H1)
+ ##| ##2: #H1; napply (or5_intro1 P2 P1 P3 P4 P5 H1)
+ ##| ##3: #H1; napply (or5_intro3 P2 P1 P3 P4 P5 H1)
+ ##| ##4: #H1; napply (or5_intro4 P2 P1 P3 P4 P5 H1)
+ ##| ##5: #H1; napply (or5_intro5 P2 P1 P3 P4 P5 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_13 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P3 P2 P1 P4 P5.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro3 P3 P2 P1 P4 P5 H1)
+ ##| ##2: #H1; napply (or5_intro2 P3 P2 P1 P4 P5 H1)
+ ##| ##3: #H1; napply (or5_intro1 P3 P2 P1 P4 P5 H1)
+ ##| ##4: #H1; napply (or5_intro4 P3 P2 P1 P4 P5 H1)
+ ##| ##5: #H1; napply (or5_intro5 P3 P2 P1 P4 P5 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_14 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P4 P2 P3 P1 P5.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro4 P4 P2 P3 P1 P5 H1)
+ ##| ##2: #H1; napply (or5_intro2 P4 P2 P3 P1 P5 H1)
+ ##| ##3: #H1; napply (or5_intro3 P4 P2 P3 P1 P5 H1)
+ ##| ##4: #H1; napply (or5_intro1 P4 P2 P3 P1 P5 H1)
+ ##| ##5: #H1; napply (or5_intro5 P4 P2 P3 P1 P5 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_15 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P5 P2 P3 P4 P1.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro5 P5 P2 P3 P4 P1 H1)
+ ##| ##2: #H1; napply (or5_intro2 P5 P2 P3 P4 P1 H1)
+ ##| ##3: #H1; napply (or5_intro3 P5 P2 P3 P4 P1 H1)
+ ##| ##4: #H1; napply (or5_intro4 P5 P2 P3 P4 P1 H1)
+ ##| ##5: #H1; napply (or5_intro1 P5 P2 P3 P4 P1 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_23 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P3 P2 P4 P5.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro1 P1 P3 P2 P4 P5 H1)
+ ##| ##2: #H1; napply (or5_intro3 P1 P3 P2 P4 P5 H1)
+ ##| ##3: #H1; napply (or5_intro2 P1 P3 P2 P4 P5 H1)
+ ##| ##4: #H1; napply (or5_intro4 P1 P3 P2 P4 P5 H1)
+ ##| ##5: #H1; napply (or5_intro5 P1 P3 P2 P4 P5 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_24 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P4 P3 P2 P5.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro1 P1 P4 P3 P2 P5 H1)
+ ##| ##2: #H1; napply (or5_intro4 P1 P4 P3 P2 P5 H1)
+ ##| ##3: #H1; napply (or5_intro3 P1 P4 P3 P2 P5 H1)
+ ##| ##4: #H1; napply (or5_intro2 P1 P4 P3 P2 P5 H1)
+ ##| ##5: #H1; napply (or5_intro5 P1 P4 P3 P2 P5 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_25 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P5 P3 P4 P2.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro1 P1 P5 P3 P4 P2 H1)
+ ##| ##2: #H1; napply (or5_intro5 P1 P5 P3 P4 P2 H1)
+ ##| ##3: #H1; napply (or5_intro3 P1 P5 P3 P4 P2 H1)
+ ##| ##4: #H1; napply (or5_intro4 P1 P5 P3 P4 P2 H1)
+ ##| ##5: #H1; napply (or5_intro2 P1 P5 P3 P4 P2 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_34 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P2 P4 P3 P5.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro1 P1 P2 P4 P3 P5 H1)
+ ##| ##2: #H1; napply (or5_intro2 P1 P2 P4 P3 P5 H1)
+ ##| ##3: #H1; napply (or5_intro4 P1 P2 P4 P3 P5 H1)
+ ##| ##4: #H1; napply (or5_intro3 P1 P2 P4 P3 P5 H1)
+ ##| ##5: #H1; napply (or5_intro5 P1 P2 P4 P3 P5 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_35 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P2 P5 P4 P3.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro1 P1 P2 P5 P4 P3 H1)
+ ##| ##2: #H1; napply (or5_intro2 P1 P2 P5 P4 P3 H1)
+ ##| ##3: #H1; napply (or5_intro5 P1 P2 P5 P4 P3 H1)
+ ##| ##4: #H1; napply (or5_intro4 P1 P2 P5 P4 P3 H1)
+ ##| ##5: #H1; napply (or5_intro3 P1 P2 P5 P4 P3 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_45 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P2 P3 P5 P4.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro1 P1 P2 P3 P5 P4 H1)
+ ##| ##2: #H1; napply (or5_intro2 P1 P2 P3 P5 P4 H1)
+ ##| ##3: #H1; napply (or5_intro3 P1 P2 P3 P5 P4 H1)
+ ##| ##4: #H1; napply (or5_intro5 P1 P2 P3 P5 P4 H1)
+ ##| ##5: #H1; napply (or5_intro4 P1 P2 P3 P5 P4 H1)
+ ##]
+nqed.
+
ninductive ex (A:Type) (Q:A → Prop) : Prop ≝
ex_intro: ∀x:A.Q x → ex A Q.
projects / helm.git / commitdiff