freescale porting

[helm.git] / helm / software / matita / contribs / ng_assembly / compiler / environment.ma

diff --git a/helm/software/matita/contribs/ng_assembly/compiler/environment.ma b/helm/software/matita/contribs/ng_assembly/compiler/environment.ma
index 73a2c8aa44d990cf42f80cc05e2c9946267cbea8..5b1408931c32144fbe758d1851189681f9a84f3a 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/compiler/environment.ma
+++ b/helm/software/matita/contribs/ng_assembly/compiler/environment.ma
@@ -13,9 +13,10 @@
 (**************************************************************************)
 
 (* ********************************************************************** *)
+(*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(* Sviluppato da:                                                         *)
-(*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
+(*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -39,25 +40,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
-*)
+(* 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));
+ ncases l in ⊢ (? ? % ? → %);
+ ##[ ##1: #dsc; #H; ndestruct (*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).
   match l
@@ -65,8 +62,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).