mod change (-x)

[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
old mode 100755 (executable)
new mode 100644 (file)
index 6a5e204..5b14089
--- 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).