From c6ec0dc44c2e592c7b1323304052bc1a523e7c22 Mon Sep 17 00:00:00 2001
From: Cosimo Oliboni <??>
Date: Fri, 4 Sep 2009 11:56:25 +0000
Subject: [PATCH]  freescale porting, work in progress

---
 .../contribs/ng_assembly/common/theory.ma     |  7 +++--
 .../ng_assembly/compiler/environment.ma       | 29 ++++++++-----------
 .../contribs/ng_assembly/universe/universe.ma | 10 +++++--
 3 files changed, 24 insertions(+), 22 deletions(-)

diff --git a/helm/software/matita/contribs/ng_assembly/common/theory.ma b/helm/software/matita/contribs/ng_assembly/common/theory.ma
index 2ce5c7036..31cb11c9c 100644
--- 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 6a5e204f3..d62b6fec3 100755
--- 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 061cccd3e..21fd84675 100755
--- 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 *)
-- 
2.39.2