1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
18 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
20 (* ********************************************************************** *)
22 include "compiler/environment.ma".
23 include "compiler/ast_tree.ma".
25 (* ********************** *)
26 (* GESTIONE AMBIENTE FLAT *)
27 (* ********************** *)
30 inductive var_flatElem : Type ≝
31 VAR_FLAT_ELEM: aux_strId_type → desc_elem → var_flatElem.
33 definition get_name_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM n _ ⇒ n ].
34 definition get_desc_flatVar ≝ λv:var_flatElem.match v with [ VAR_FLAT_ELEM _ d ⇒ d ].
36 definition aux_flatEnv_type ≝ list var_flatElem.
38 definition empty_flatEnv ≝ nil var_flatElem.
40 (* mappa: nome + max + cur *)
41 inductive map_list : nat → Type ≝
43 | map_cons: ∀n.option nat → map_list n → map_list (S n).
45 definition defined_mapList ≝
46 λd.λl:map_list d.match l with [ map_nil ⇒ False | map_cons _ _ _ ⇒ True ].
48 definition cut_first_mapList : Πd.map_list d → ? → map_list (pred d) ≝
49 λd.λl:map_list d.λp:defined_mapList ? l.
52 return λX.λY:map_list X.defined_mapList X Y → map_list (pred X)
54 [ map_nil ⇒ λp:defined_mapList O map_nil.False_rect ? p
55 | map_cons n h t ⇒ λp:defined_mapList (S n) (map_cons n h t).t
58 definition get_first_mapList : Πd.map_list d → ? → option nat ≝
59 λd.λl:map_list d.λp:defined_mapList ? l.
62 return λX.λY:map_list X.defined_mapList X Y → option nat
64 [ map_nil ⇒ λp:defined_mapList O map_nil.False_rect ? p
65 | map_cons n h t ⇒ λp:defined_mapList (S n) (map_cons n h t).h
68 inductive map_elem (d:nat) : Type ≝
69 MAP_ELEM: aux_str_type → nat → map_list (S d) → map_elem d.
71 definition get_name_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM n _ _ ⇒ n ].
72 definition get_max_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM _ m _ ⇒ m ].
73 definition get_cur_mapElem ≝ λd.λm:map_elem d.match m with [ MAP_ELEM _ _ c ⇒ c ].
75 definition aux_map_type ≝ λd.list (map_elem d).
77 definition empty_map ≝ nil (map_elem O).
79 lemma defined_mapList_S_to_true :
80 ∀d.∀l:map_list (S d).defined_mapList (S d) l = True.
84 | intros; simplify; reflexivity
88 lemma defined_mapList_get :
89 ∀d.∀h:map_elem d.defined_mapList (S d) (get_cur_mapElem d h).
91 rewrite > (defined_mapList_S_to_true ? (get_cur_mapElem d h));
96 let rec get_id_map_aux d (map:aux_map_type d) (name:aux_str_type) on map : option nat ≝
99 | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with
100 [ true ⇒ get_first_mapList (S d) (get_cur_mapElem d h) (defined_mapList_get ??)
101 | false ⇒ get_id_map_aux d t name
105 definition get_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
106 match get_id_map_aux d map name with [ None ⇒ O | Some x ⇒ x ].
109 let rec get_max_map_aux d (map:aux_map_type d) (name:aux_str_type) on map ≝
112 | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with
113 [ true ⇒ Some ? (get_max_mapElem d h)
114 | false ⇒ get_max_map_aux d t name
118 definition get_max_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
119 match get_max_map_aux d map name with [ None ⇒ O | Some x ⇒ x ].
122 definition check_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
123 match get_id_map_aux d map name with [ None ⇒ False | Some _ ⇒ True ].
125 definition checkb_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
126 match get_id_map_aux d map name with [ None ⇒ false | Some _ ⇒ true ].
128 lemma checkbidmap_to_checkidmap : ∀d.∀map:aux_map_type d.∀name.checkb_id_map d map name = true → check_id_map d map name.
129 unfold checkb_id_map;
132 elim (get_id_map_aux d map name) 0;
133 [ simplify; intro; destruct H
134 | simplify; intros; apply I
138 definition checknot_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
139 match get_id_map_aux d map name with [ None ⇒ True | Some _ ⇒ False ].
141 definition checknotb_id_map ≝ λd.λmap:aux_map_type d.λname:aux_str_type.
142 match get_id_map_aux d map name with [ None ⇒ true | Some _ ⇒ false ].
144 lemma checknotbidmap_to_checknotidmap : ∀d.∀map:aux_map_type d.∀name.checknotb_id_map d map name = true → checknot_id_map d map name.
145 unfold checknotb_id_map;
146 unfold checknot_id_map;
148 elim (get_id_map_aux d map name) 0;
149 [ simplify; intro; apply I
150 | simplify; intros; destruct H
155 let rec get_desc_flatEnv_aux (fe:aux_flatEnv_type) (name:aux_strId_type) on fe ≝
158 | cons h t ⇒ match eqStrId_str name (get_name_flatVar h) with
159 [ true ⇒ Some ? (get_desc_flatVar h)
160 | false ⇒ get_desc_flatEnv_aux t name
164 definition get_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
165 match get_desc_flatEnv_aux fe str with
166 [ None ⇒ DESC_ELEM true (AST_TYPE_BASE AST_BASE_TYPE_BYTE8) | Some x ⇒ x ].
168 definition check_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
169 match get_desc_flatEnv_aux fe str with [ None ⇒ False | Some _ ⇒ True ].
171 definition checkb_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
172 match get_desc_flatEnv_aux fe str with [ None ⇒ false | Some _ ⇒ true ].
174 lemma checkbdescflatenv_to_checkdescflatenv : ∀fe,str.checkb_desc_flatEnv fe str = true → check_desc_flatEnv fe str.
175 unfold checkb_desc_flatEnv;
176 unfold check_desc_flatEnv;
178 elim (get_desc_flatEnv_aux fe str) 0;
179 [ simplify; intro; destruct H
180 | simplify; intros; apply I
184 definition checknot_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
185 match get_desc_flatEnv_aux fe str with [ None ⇒ True | Some _ ⇒ False ].
187 definition checknotb_desc_flatEnv ≝ λfe:aux_flatEnv_type.λstr:aux_strId_type.
188 match get_desc_flatEnv_aux fe str with [ None ⇒ true | Some _ ⇒ false ].
190 lemma checknotbdescflatenv_to_checknotdescflatenv : ∀fe,str.checknotb_desc_flatEnv fe str = true → checknot_desc_flatEnv fe str.
191 unfold checknotb_desc_flatEnv;
192 unfold checknot_desc_flatEnv;
194 elim (get_desc_flatEnv_aux fe str) 0;
195 [ simplify; intro; apply I
196 | simplify; intros; destruct H
201 definition eq_flatEnv_elem ≝
203 [ VAR_FLAT_ELEM sId1 d1 ⇒ match e2 with
204 [ VAR_FLAT_ELEM sId2 d2 ⇒ (eqStrId_str sId1 sId2)⊗(eqDesc_elem d1 d2) ]].
206 lemma eq_to_eqflatenv : ∀e1,e2.e1 = e2 → eq_flatEnv_elem e1 e2 = true.
211 rewrite > (eq_to_eqstrid a a (refl_eq ??));
212 rewrite > (eq_to_eqdescelem d d (refl_eq ??));
216 lemma eqflatenv_to_eq : ∀e1,e2.eq_flatEnv_elem e1 e2 = true → e1 = e2.
223 rewrite > (eqstrid_to_eq a1 a (andb_true_true ?? H));
224 rewrite > (eqdescelem_to_eq d1 d (andb_true_true_r ?? H));
228 let rec le_flatEnv (fe,fe':aux_flatEnv_type) on fe ≝
231 | cons h tl ⇒ match fe' with
232 [ nil ⇒ false | cons h' tl' ⇒ (eq_flatEnv_elem h h')⊗(le_flatEnv tl tl') ]
235 lemma eq_to_leflatenv : ∀e1,e2.e1 = e2 → le_flatEnv e1 e2 = true.
241 rewrite > (eq_to_eqflatenv a a (refl_eq ??));
247 lemma leflatenv_to_le : ∀fe,fe'.le_flatEnv fe fe' = true → ∃x.fe@x=fe'.
250 [ intros; exists; [ apply fe' | reflexivity ]
251 | intros 4; elim fe';
252 [ simplify in H1:(%); destruct H1
253 | simplify in H2:(%);
254 rewrite < (eqflatenv_to_eq a a1 (andb_true_true ?? H2));
255 cases (H l1 (andb_true_true_r ?? H2));
258 exists; [ apply x | reflexivity ]
263 lemma le_to_leflatenv : ∀fe,x.le_flatEnv fe (fe@x) = true.
269 rewrite > (eq_to_eqflatenv a a (refl_eq ??));
275 lemma leflatenv_to_check : ∀fe,fe',str.
276 (le_flatEnv fe fe' = true) →
277 (check_desc_flatEnv fe str) →
278 (check_desc_flatEnv fe' str).
280 cases (leflatenv_to_le fe fe' H);
283 [ intro; simplify in H2:(%); elim H2;
286 cases (eqStrId_str str (get_name_flatVar a));
287 [ simplify; intro; apply H3
293 lemma leflatenv_to_get : ∀fe,fe',str.
294 (le_flatEnv fe fe' = true) →
295 (check_desc_flatEnv fe str) →
296 (get_desc_flatEnv fe str = get_desc_flatEnv fe' str).
298 cases (leflatenv_to_le fe fe' H);
306 cases (eqStrId_str str (get_name_flatVar a));
311 unfold check_desc_flatEnv;
312 unfold get_desc_flatEnv;
313 cases (get_desc_flatEnv_aux l str);
314 [ simplify; intros; elim H3
315 | simplify; intros; rewrite < (H2 H3); reflexivity
321 (* controllo di coerenza env <-> map *)
322 let rec check_map_env_align_auxEnv (d:nat) (e:aux_env_type d) (str:aux_str_type) (res:nat) on e ≝
325 | env_cons d' h t ⇒ λf.check_map_env_align_auxEnv d' t str (f h)
326 ] (λx.match get_desc_from_lev_env x str with [ None ⇒ S res | Some _ ⇒ O ]).
328 let rec check_map_env_align_auxMap (d:nat) (map:map_list d) (res:nat) on map ≝
330 [ map_nil ⇒ eqb res O
331 | map_cons d' h t ⇒ match eqb res O with
332 [ true ⇒ match h with
333 [ None ⇒ check_map_env_align_auxMap d' t O | Some _ ⇒ false ]
334 | false ⇒ match h with
335 [ None ⇒ false | Some _ ⇒ check_map_env_align_auxMap d' t (pred res) ]
339 (* esprimendolo in lingua umana il vincolo che controlla e':
341 la map_list "cur" deve avere la seguente struttura
342 - Some _ ; ... ; Some _ ; None ; ... None
343 - il numero di Some _ deve essere pari a (d + 1 - x) con x
344 ricavato scandendo in avanti tutti gli ambienti e
345 numerando quanti ambienti CONSECUTIVI non contengono la definizione di name
347 ex: scandendo e in avanti si trova la seguente sequenza di check per il nome "pippo"
349 quindi sapendo che d=5 (6 partendo da 0) e che check_env_align_aux ha restituito 2
350 sappiamo che la mappa alla voce "pippo" deve avere la seguente struttura scandita in avanti
351 Some _ ; Some _ ; Some _ ; Some _ ; None ; None
352 cioe' 5+1-2 Some seguiti da solo None
354 NB: e' solo meta' perche' cosi' si asserisce map ≤ env
357 let rec check_map_env_align (d:nat) (e:aux_env_type d) (map:aux_map_type d) on map ≝
360 | cons h t ⇒ (check_map_env_align_auxMap (S d) (get_cur_mapElem d h) (d + 1 - (check_map_env_align_auxEnv d e (get_name_mapElem d h) O)))⊗
361 (check_map_env_align d e t)
364 let rec check_env_map_align_aux (d:nat) (map:aux_map_type d) (le:list var_elem) on le ≝
367 | cons h t ⇒ match get_id_map_aux d map (get_name_var h) with
368 [ None ⇒ false | Some _ ⇒ check_env_map_align_aux d map t ]
371 (* esprimendolo in lingua umana il vincolo che controlla e':
374 NB: e' l'altra meta' perche' cosi' asserisce env ≤ map
376 let rec check_env_map_align (de:nat) (e:aux_env_type de) (dm:nat) (map:aux_map_type dm) on e ≝
378 [ env_nil h ⇒ check_env_map_align_aux dm map h
379 | env_cons d' h t ⇒ (check_env_map_align_aux dm map h)⊗(check_env_map_align d' t dm map)
383 definition env_to_flatEnv_inv ≝
384 λd.λe:aux_env_type d.λmap:aux_map_type d.λfe:aux_flatEnv_type.
386 check_desc_env d e str →
387 (((check_env_map_align d e d map)⊗(check_map_env_align d e map)) = true ∧
388 check_id_map d map str ∧
389 check_desc_flatEnv fe (STR_ID str (get_id_map d map str)) ∧
390 get_desc_env d e str = get_desc_flatEnv fe (STR_ID str (get_id_map d map str))).
392 lemma inv_to_checkdescflatenv :
393 ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.
394 env_to_flatEnv_inv d e map fe →
395 (∀str.check_desc_env d e str → check_desc_flatEnv fe (STR_ID str (get_id_map d map str))).
397 unfold env_to_flatEnv_inv in H:(%);
399 apply (proj2 ?? (proj1 ?? Hletin));
402 lemma env_map_flatEnv_empty_aux : env_to_flatEnv_inv O empty_env empty_map empty_flatEnv.
403 unfold env_to_flatEnv_inv;
406 unfold empty_flatEnv;
412 lemma leflatenv_to_inv :
413 ∀d.∀e.∀map:aux_map_type d.∀fe,fe'.
414 le_flatEnv fe fe' = true →
415 env_to_flatEnv_inv d e map fe →
416 env_to_flatEnv_inv d e map fe'.
418 unfold env_to_flatEnv_inv;
422 [ lapply (H1 str H2);
423 apply (proj1 ?? (proj1 ?? Hletin))
424 | lapply (H1 str H2);
425 apply (leflatenv_to_check fe fe' ? H (proj2 ?? (proj1 ?? Hletin)))
427 | lapply (H1 str H2);
428 rewrite < (leflatenv_to_get fe fe' ? H (proj2 ?? (proj1 ?? Hletin)));
429 apply (proj2 ?? Hletin)
433 lemma leflatenv_trans :
435 le_flatEnv fe fe' = true →
436 le_flatEnv fe' fe'' = true →
437 le_flatEnv fe fe'' = true.
439 cases (leflatenv_to_le fe ? H);
442 cases (leflatenv_to_le (fe@x) fe'' H2);
444 rewrite > associative_append;
445 apply (le_to_leflatenv fe ?).
448 (* enter: propaga in testa la vecchia testa (il "cur" precedente) *)
449 let rec enter_map d (map:aux_map_type d) on map ≝
454 (get_name_mapElem d h)
455 (get_max_mapElem d h)
457 (get_first_mapList ? (get_cur_mapElem d h) (defined_mapList_get ??))
458 (get_cur_mapElem d h))
462 lemma getidmap_to_enter :
463 ∀d.∀m:aux_map_type d.∀str.
464 get_id_map_aux (S d) (enter_map d m) str = get_id_map_aux d m str.
467 [ simplify; reflexivity
468 | simplify; rewrite > H; reflexivity
472 (* leave: elimina la testa (il "cur" corrente) *)
473 let rec leave_map d (map:aux_map_type (S d)) on map ≝
478 (get_name_mapElem (S d) h)
479 (get_max_mapElem (S d) h)
480 (cut_first_mapList ? (get_cur_mapElem (S d) h) (defined_mapList_get ??))
484 (* aggiungi descrittore *)
485 let rec new_map_elem_from_depth_aux (d:nat) on d ≝
490 | S n ⇒ map_cons n (None ?) (new_map_elem_from_depth_aux n)
493 let rec new_max_map_aux d (map:aux_map_type d) (name:aux_str_type) (max:nat) on map ≝
496 | cons h t ⇒ match eqStr_str name (get_name_mapElem d h) with
497 [ true ⇒ MAP_ELEM d name max (map_cons d (Some ? max) (cut_first_mapList (S d) (get_cur_mapElem d h) (defined_mapList_get ??)))
499 ]::(new_max_map_aux d t name max)
502 definition add_desc_env_flatEnv_map ≝
503 λd.λmap:aux_map_type d.λstr.
504 match get_max_map_aux d map str with
505 [ None ⇒ map@[ MAP_ELEM d str O (map_cons d (Some ? O) (new_map_elem_from_depth_aux d)) ]
506 | Some x ⇒ new_max_map_aux d map str (S x)
509 definition add_desc_env_flatEnv_fe ≝
510 λd.λmap:aux_map_type d.λfe.λstr.λc.λdesc.
511 fe@[ VAR_FLAT_ELEM (STR_ID str match get_max_map_aux d map str with [ None ⇒ O | Some x ⇒ (S x)])
512 (DESC_ELEM c desc) ].
514 let rec build_trasfEnv_env (d:nat) (trsf:list (Prod3T aux_str_type bool ast_type)) on trsf : aux_env_type d → aux_env_type d ≝
517 | cons h t ⇒ (λx.(build_trasfEnv_env d t) (add_desc_env d x (fst3T ??? h) (snd3T ??? h) (thd3T ??? h)))
520 let rec build_trasfEnv_mapFe (d:nat) (trsf:list (Prod3T aux_str_type bool ast_type)) on trsf :
521 Prod (aux_map_type d) aux_flatEnv_type → Prod (aux_map_type d) aux_flatEnv_type ≝
524 | cons h t ⇒ (λx.(build_trasfEnv_mapFe d t)
525 (pair ?? (add_desc_env_flatEnv_map d (fst ?? x) (fst3T ??? h))
526 (add_desc_env_flatEnv_fe d (fst ?? x) (snd ?? x) (fst3T ??? h) (snd3T ??? h) (thd3T ??? h))))
529 (* avanzamento dell'invariante *)
530 axiom env_map_flatEnv_enter_aux :
531 ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.
532 env_to_flatEnv_inv d e map fe →
533 env_to_flatEnv_inv (S d) (enter_env d e) (enter_map d map) fe.
535 axiom env_map_flatEnv_add_aux :
536 ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.∀trsf.
537 env_to_flatEnv_inv d e map fe →
539 (build_trasfEnv_env d trsf e)
540 (fst ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe)))
541 (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))).
543 lemma env_map_flatEnv_addNil_aux :
544 ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.
545 env_to_flatEnv_inv d e map fe →
547 (build_trasfEnv_env d [] e)
548 (fst ?? (build_trasfEnv_mapFe d [] (pair ?? map fe)))
549 (snd ?? (build_trasfEnv_mapFe d [] (pair ?? map fe))).
555 lemma env_map_flatEnv_addSingle_aux :
556 ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe.∀name,const,desc.
557 env_to_flatEnv_inv d e map fe →
559 (add_desc_env d e name const desc)
560 (fst ?? (build_trasfEnv_mapFe d [ tripleT ??? name const desc ] (pair ?? map fe)))
561 (snd ?? (build_trasfEnv_mapFe d [ tripleT ??? name const desc ] (pair ?? map fe))).
563 apply (env_map_flatEnv_add_aux d e map fe [ tripleT ??? name const desc ]);
567 lemma env_map_flatEnv_addJoin_aux :
568 ∀d.∀e:aux_env_type d.∀map:aux_map_type d.∀fe:aux_flatEnv_type.∀name,const,desc,trsf.
570 (build_trasfEnv_env d trsf (add_desc_env d e name const desc))
573 (build_trasfEnv_env d ([ tripleT ??? name const desc ]@trsf) e)
580 lemma env_map_flatEnv_add_aux_fe_al :
581 ∀trsf.∀d.∀m:aux_map_type d.∀a,l.
582 snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m (a::l))) =
583 a::(snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m l))).
586 [ simplify; reflexivity
595 lemma env_map_flatEnv_add_aux_fe_l :
596 ∀trsf.∀d.∀m:aux_map_type d.∀l.
597 snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m l)) =
598 l@(snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m []))).
601 [ simplify; reflexivity
602 | rewrite > (env_map_flatEnv_add_aux_fe_al ????);
608 lemma env_map_flatEnv_add_aux_fe :
609 ∀d.∀map:aux_map_type d.∀fe,trsf.
610 ∃x.fe@x = (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map fe))).
616 [ apply (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map [])))
621 [ apply (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? map [])))
622 | rewrite > (env_map_flatEnv_add_aux_fe_al trsf d map a l);
623 rewrite > (env_map_flatEnv_add_aux_fe_l trsf d map l);
624 rewrite < (cons_append_commute ????);
630 lemma buildtrasfenvadd_to_le :
631 ∀d.∀m:aux_map_type d.∀fe,trsf.
632 le_flatEnv fe (snd ?? (build_trasfEnv_mapFe d trsf (pair ?? m fe))) = true.
634 cases (env_map_flatEnv_add_aux_fe d m fe trsf);
636 rewrite > (le_to_leflatenv fe x);
640 axiom env_map_flatEnv_leave_aux :
641 ∀d.∀e:aux_env_type (S d).∀map:aux_map_type (S d).∀fe.∀trsf.
642 env_to_flatEnv_inv (S d) (build_trasfEnv_env (S d) trsf e) map fe →
643 env_to_flatEnv_inv d (leave_env d (build_trasfEnv_env (S d) trsf e)) (leave_map d map) fe.
645 lemma leave_add_enter_env_aux :
646 ∀d.∀a:aux_env_type d.∀trsf.∀c.
647 ∃b.build_trasfEnv_env (S d) trsf (env_cons d c a) = (env_cons d b a).
650 [ simplify; exists; [ apply c | reflexivity ]
655 lemma leave_add_enter_env :
656 ∀d.∀e:aux_env_type d.∀trsf.
657 leave_env d (build_trasfEnv_env (S d) trsf (enter_env d e)) = e.
660 lapply (leave_add_enter_env_aux d e trsf []);
667 lemma newid_from_init :
668 ∀d.∀e:aux_env_type d.∀name,const,desc.
669 ast_id d (add_desc_env d e name const desc) const desc.
671 lapply (AST_ID d (add_desc_env d e name const desc) name ?);
674 rewrite > (eq_to_eqstr ?? (refl_eq ??));
677 | cut (const = get_const_desc (get_desc_env d (add_desc_env d e name const desc) name) ∧
678 desc = get_type_desc (get_desc_env d (add_desc_env d e name const desc) name));
679 [ rewrite > (proj1 ?? Hcut) in ⊢ (? ? ? % ?);
680 rewrite > (proj2 ?? Hcut) in ⊢ (? ? ? ? %);
685 rewrite > (eq_to_eqstr ?? (refl_eq ??));
690 rewrite > (eq_to_eqstr ?? (refl_eq ??));