X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fcompiler%2Fenvironment.ma;h=5b1408931c32144fbe758d1851189681f9a84f3a;hb=e7264f953fcf2cd2bef9057d83add08996d2ce75;hp=6a5e204f332bf4f37b1801df9f313c525eaf2e5e;hpb=34e2c8f59dd7924e15a7746644182d12ad09fed3;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/compiler/environment.ma b/helm/software/matita/contribs/ng_assembly/compiler/environment.ma
index 6a5e204f3..5b1408931 100755
--- 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,26 +40,20 @@ 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));
+ 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).