(**************************************************************************)
(* ********************************************************************** *)
+(* Progetto FreeScale *)
(* *)
-(* Sviluppato da: *)
-(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
(* *)
(* ********************************************************************** *)
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
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).