freescale porting, work in progress

diff --git a/helm/software/matita/contribs/ng_assembly/common/theory.ma b/helm/software/matita/contribs/ng_assembly/common/theory.ma
index 2ce5c7036deb6f45b405573846d9f53f48ff418e..31cb11c9ce0ccd06b0f587f8625f1b65a0e1441a 100644 (file)
--- a/helm/software/matita/contribs/ng_assembly/common/theory.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/theory.ma
@@ -527,13 +527,14 @@ ndefinition associative : ∀A:Type.∀R:relationT A A.Prop ≝
 λA.λR.∀x,y,z:A.R (R x y) z = R x (R y z).
 
 (* aggiunta per bypassare i punti in cui le dimostrazioni sono equivalenti *)
-
+(*
 ninductive peqv (A:Prop) (x:A) : A → Prop ≝
  prefl_eqv : peqv A x x.
 
 interpretation "prop equivalence" 'preqv t x y = (peqv t x y).
-
+*)
 (* \equiv *)
+(*
 notation > "hvbox(a break ≡ b)" 
   non associative with precedence 45
 for @{ 'preqv ? $a $b }.
@@ -552,7 +553,7 @@ nlemma peqv_ind_r: ∀A:Prop.∀x:A.∀P:A → Prop.P x → ∀y:A.y ≡ x → P
 nqed.
 
 naxiom peqv_ax : ∀P:Prop.∀Q,R:P.Q ≡ R.
-
+*)
 (* uso P x → P y, H e' P x
    nrewrite > cioe' napply (peqv_ind ? x (λ_.?) H y (dimostrazione di x ≡ y));
    nrewrite < cioe' napply (peqv_ind_r ? x ? H y (dimostrazione y ≡ x)));

diff --git a/helm/software/matita/contribs/ng_assembly/compiler/environment.ma b/helm/software/matita/contribs/ng_assembly/compiler/environment.ma
index 6a5e204f332bf4f37b1801df9f313c525eaf2e5e..d62b6fec366ed110af0a82f1b5ef9c7e205b192b 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/compiler/environment.ma
+++ b/helm/software/matita/contribs/ng_assembly/compiler/environment.ma
@@ -39,26 +39,21 @@ ninductive env_list : nat → Type ≝
   env_nil: list envDsc → env_list O
 | env_cons: ∀n.list envDsc → env_list n → env_list (S n).
 
-(* sto cercando di emulare "inversion e" *)
-nlemma inv_envList :
- ∀n.∀e:env_list n.∀P:Prop.
- (n = (match e with [ env_nil _ ⇒ O | env_cons n' _ _ ⇒ S n' ]) → P) → P.
- #n; #e;
- ncases e;
- nnormalize;
- ##[ ##1: #x; #P; #H;
- ##| ##2: #x; #y; #z; #P; #H;
- ##]
- napply (H (refl_eq …)).
-nqed.
-
 ndefinition defined_envList ≝
 λd.λl:env_list d.match l with [ env_nil _ ⇒ False | env_cons _ _ _ ⇒ True ].
 
-(* bisogna dimostrare "defined_envList (S ...)"
-   impossibile anche cercando di usare l'emulazione di inversion
-*)
-naxiom defined_envList_S : ∀d.∀l:env_list (S d).defined_envList (S d) l.
+(* bisogna bypassare la carenza di inversion *)
+nlemma defined_envList_S : ∀d.∀l:env_list (S d).defined_envList (S d) l.
+ #d; #l;
+ ngeneralize in match (refl_eq ? (S d));
+ (* S d = S d → ? e' in realta' eq nat (S d) (S d) ... *)
+ ncases l in ⊢ (? ? % ? → %);
+ ##[ ##1: #dsc; #H; nelim (nat_destruct_0_S … H)
+ ##| ##2: #n; #dsc; #sub; #H;
+          nnormalize;
+          napply I
+ ##]
+nqed.
 
 ndefinition cut_first_envList_aux : Πd.env_list (S d) → env_list d ≝
 λd.λl:env_list (S d).

diff --git a/helm/software/matita/contribs/ng_assembly/universe/universe.ma b/helm/software/matita/contribs/ng_assembly/universe/universe.ma
index 061cccd3e99983d62b083210e9cc02890bfe54f0..21fd84675aebe79b938ef65f7c07a63a034303d3 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/universe/universe.ma
+++ b/helm/software/matita/contribs/ng_assembly/universe/universe.ma
@@ -105,6 +105,13 @@ nqed.
 
 (* eqxx_to_eq universale *)
 (* serve l'assioma di equivalenza sulle dimostrazioni *)
+
+naxiom eqSUN_to_eq_aux : ∀l,e.∀dim1,dim2:((member_natList e l) = true).S_EL l e dim1 = S_EL l e dim2.
+(* mi dice matita/logic/equality/eq.ind not found che e' vero perche' uso il mio...
+ #l; #e; #dim1; #dim2;
+ nauto library;
+*)
+
 nlemma eqSUN_to_eq : ∀l.∀x,y:S_UN l.eq_SUN l x y = true → x = y.
  #l; #x; nelim x;
  #u1; #dim1;
@@ -114,8 +121,7 @@ nlemma eqSUN_to_eq : ∀l.∀x,y:S_UN l.eq_SUN l x y = true → x = y.
  #H;
  nrewrite > (eqnat_to_eq u1 u2 H) in dim1:(%) ⊢ %;
  #dim1;
- napply (peqv_ind ? dim1 (λ_.?) ? dim2 (peqv_ax ? dim1 dim2));
- napply refl_eq.
+ napply eqSUN_to_eq_aux.
 nqed.
 
 (* neq_to_neqxx universale *)