(* Progetto FreeScale *)
(* *)
(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Ultima modifica: 05/08/2009 *)
+(* Sviluppo: 2008-2010 *)
(* *)
(* ********************************************************************** *)
##]
nqed.
-(* perche' non si riesce a dimstrare ??? *
-nlemma SUN_construct
- : ∀l.∀u.
- ∀dim1,dim2:(member_natList u l = true).
- ((S_EL l u dim1) = (S_EL l u dim2)).
- #l; #u; #dim1; #dim2;
- nchange with (S_EL l u dim1 = S_EL l u dim1);
- napply refl_eq.
-nqed.
-*)
-naxiom SUN_construct
- : ∀l.∀u.
- ∀dim1,dim2:(member_natList u l = true).
- ((S_EL l u dim1) = (S_EL l u dim2)).
-
-nlemma eqgetelem_to_eq : ∀l.∀x,y:S_UN l.(getelem ? x) = (getelem ? y) → x = y.
- #l; #x; nelim x;
- #u1; #dim1;
- #y; nelim y;
- #u2; #dim2;
- nchange with (u1 = u2 → ?);
- #H;
- nrewrite > H in dim1:(%) ⊢ %;
- #dim1;
- napply (SUN_construct l u2 dim1 dim2).
-nqed.
-
(* eqxx_to_eq universale *)
+(* !!! evidente ma come si fa? *)
+naxiom eqSUN_to_eq_aux : ∀l,x,y.((getelem l x) = (getelem l y)) → x = y.
+
nlemma eqSUN_to_eq : ∀l.∀x,y:S_UN l.eq_SUN l x y = true → x = y.
- #l; #x; nelim x;
- #u1; #dim1;
- #y; nelim y;
- #u2; #dim2;
- nchange with ((eq_nat u1 u2 = true) → ?);
- #H;
- nrewrite > (eqgetelem_to_eq l (S_EL l u1 dim1) (S_EL l u2 dim2) (eqnat_to_eq u1 u2 H));
- napply refl_eq.
+ #l; #x; #y;
+ nchange with ((eq_nat (getelem ? x) (getelem ? y) = true) → x = y);
+ #H; napply (eqSUN_to_eq_aux l x y (eqnat_to_eq … H)).
nqed.
(* neq_to_neqxx universale *)
(* esempio0: universo ottale *)
ndefinition oct0 ≝ O.
-ndefinition oct1 ≝ S O.
-ndefinition oct2 ≝ S (S O).
-ndefinition oct3 ≝ S (S (S O)).
-ndefinition oct4 ≝ S (S (S (S O))).
-ndefinition oct5 ≝ S (S (S (S (S O)))).
-ndefinition oct6 ≝ S (S (S (S (S (S O))))).
-ndefinition oct7 ≝ S (S (S (S (S (S (S O)))))).
+ndefinition oct1 ≝ nat1.
+ndefinition oct2 ≝ nat2.
+ndefinition oct3 ≝ nat3.
+ndefinition oct4 ≝ nat4.
+ndefinition oct5 ≝ nat5.
+ndefinition oct6 ≝ nat6.
+ndefinition oct7 ≝ nat7.
ndefinition oct_UN ≝ « oct0 ; oct1 ; oct2 ; oct3 ; oct4 ; oct5 ; oct6 £ oct7 ».