From 34e2c8f59dd7924e15a7746644182d12ad09fed3 Mon Sep 17 00:00:00 2001
From: Cosimo Oliboni <??>
Date: Fri, 4 Sep 2009 00:52:21 +0000
Subject: [PATCH]  freescale porting, work in progress

---
 .../ng_assembly/common/list_utility.ma        |  2 --
 .../contribs/ng_assembly/common/theory.ma     | 32 +++++++++++++++++++
 .../ng_assembly/compiler/environment.ma       |  8 ++---
 .../contribs/ng_assembly/universe/universe.ma | 32 +++----------------
 4 files changed, 39 insertions(+), 35 deletions(-)

diff --git a/helm/software/matita/contribs/ng_assembly/common/list_utility.ma b/helm/software/matita/contribs/ng_assembly/common/list_utility.ma
index ce118e74c..1c062a912 100755
--- a/helm/software/matita/contribs/ng_assembly/common/list_utility.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/list_utility.ma
@@ -321,8 +321,6 @@ ndefinition abs_neList_aux1 : ∀T:Type.∀h:T.∀n.((len_neList T («£h»)) >
 ndefinition abs_neList_aux2 : ∀T:Type.∀h:T.∀t:ne_list T.∀n.((len_neList T (h§§t)) > (S n) = true) → ((len_neList T t) > n) = true.
  #T; #h; #t; #n; nnormalize; #H; napply H. nqed.
 
-naxiom daemon : False.
-
 nlet rec abs_neList (T:Type) (l:ne_list T) on l ≝
  match l
   return λl.Πn.(((len_neList T l) > n) = true) → T
diff --git a/helm/software/matita/contribs/ng_assembly/common/theory.ma b/helm/software/matita/contribs/ng_assembly/common/theory.ma
index 093c85e13..2ce5c7036 100644
--- a/helm/software/matita/contribs/ng_assembly/common/theory.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/theory.ma
@@ -525,3 +525,35 @@ ndefinition symmetricT: ∀A,T:Type.∀R:relationT A T.Prop ≝
 
 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 }.
+
+nlemma symmetric_peqv: ∀A:Prop. symmetric A (peqv A).
+ #A;
+ nnormalize;
+ #x; #y; #H;
+ napply (peqv_ind A x (λ_.?) ? y H);
+ napply prefl_eqv.
+nqed.
+
+nlemma peqv_ind_r: ∀A:Prop.∀x:A.∀P:A → Prop.P x → ∀y:A.y ≡ x → P y.
+ #A; #x; #P; #H; #y; #H1;
+ napply (peqv_ind A x (λ_.?) H y (symmetric_peqv … H1)).
+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 73a2c8aa4..6a5e204f3 100755
--- a/helm/software/matita/contribs/ng_assembly/compiler/environment.ma
+++ b/helm/software/matita/contribs/ng_assembly/compiler/environment.ma
@@ -58,6 +58,8 @@ ndefinition defined_envList ≝
 (* 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.
+
 ndefinition cut_first_envList_aux : Πd.env_list (S d) → env_list d ≝
 λd.λl:env_list (S d).
   match l
@@ -65,8 +67,4 @@ ndefinition cut_first_envList_aux : Πd.env_list (S d) → env_list d ≝
   with
    [ env_nil h ⇒ λp:defined_envList O (env_nil h).False_rect_Type0 ? p
    | env_cons n h t ⇒ λp:defined_envList (S n) (env_cons n h t).t
-   ] ?.
- napply (inv_envList ? l …);
- (* se apro l, a ritroso modifica il suo parametro destro d e non dimostro piu' nulla *)
- (* io pensavo di ottenere per env_nil l'assurdo S d = O ... *)
- ncases l;
+   ] (defined_envList_S d l).
diff --git a/helm/software/matita/contribs/ng_assembly/universe/universe.ma b/helm/software/matita/contribs/ng_assembly/universe/universe.ma
index a673c999b..061cccd3e 100755
--- a/helm/software/matita/contribs/ng_assembly/universe/universe.ma
+++ b/helm/software/matita/contribs/ng_assembly/universe/universe.ma
@@ -103,34 +103,8 @@ nlemma neqSUN_to_neq : ∀l.∀x,y:S_UN l.eq_SUN l x y = false → x ≠ y.
  ##]
 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 *)
+(* serve l'assioma di equivalenza sulle dimostrazioni *)
 nlemma eqSUN_to_eq : ∀l.∀x,y:S_UN l.eq_SUN l x y = true → x = y.
  #l; #x; nelim x;
  #u1; #dim1;
@@ -138,7 +112,9 @@ nlemma eqSUN_to_eq : ∀l.∀x,y:S_UN l.eq_SUN l x y = true → x = 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));
+ nrewrite > (eqnat_to_eq u1 u2 H) in dim1:(%) ⊢ %;
+ #dim1;
+ napply (peqv_ind ? dim1 (λ_.?) ? dim2 (peqv_ax ? dim1 dim2));
  napply refl_eq.
 nqed.
 
-- 
2.39.2