Changeset 1516 for src/common/AST.ma
 Timestamp:
 Nov 19, 2011, 12:38:20 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/AST.ma
r1465 r1516 145 145 lemma eq_intsize_elim : ∀sz1,sz2. ∀P:bool → Type[0]. 146 146 (sz1 ≠ sz2 → P false) → (sz1 = sz2 → P true) → P (eq_intsize sz1 sz2). 147 * * #P #Hne #Heq whd in ⊢ (?%) try (@Heq @refl) @Hne % #E destruct147 * * #P #Hne #Heq whd in ⊢ (?%); try (@Heq @refl) @Hne % #E destruct 148 148 qed. 149 149 … … 175 175 (sz1 ≠ sz2 → Q d) → (∀E:sz1 = sz2. match sym_eq ??? E return λx.λ_.P x → Type[0] with [ refl ⇒ λp. Q (f p) ] p ) → Q (intsize_eq_elim A sz1 sz2 P p f d). 176 176 #A * * #P #p #f #d #Q #Hne #Heq 177 [ 1,5,9: whd in ⊢ (?%) @(Heq (refl ??))178  *: whd in ⊢ (?%) @Hne % #E destruct177 [ 1,5,9: whd in ⊢ (?%); @(Heq (refl ??)) 178  *: whd in ⊢ (?%); @Hne % #E destruct 179 179 ] qed. 180 180 … … 351 351 #A #B #C #f #l elim l 352 352 [ #l' #E normalize in E; destruct % 353  * #a #b #tl #IH #l' normalize in ⊢ (??%? → ?) cases (f b) normalize in ⊢ (? → ??%? → ?)353  * #a #b #tl #IH #l' normalize in ⊢ (??%? → ?); cases (f b) normalize in ⊢ (? → ??%? → ?); 354 354 [2: #err #E destruct 355 355  #c change with (match map_partial … f tl with [ OK x ⇒ ?  Error y ⇒ ?] = ? → ?) 356 cases (map_partial … f tl) in IH ⊢ % 357 #x #IH normalize in ⊢ (??%? → ?) #ABS destruct normalize356 cases (map_partial … f tl) in IH ⊢ %; 357 #x #IH normalize in ⊢ (??%? → ?); #ABS destruct normalize 358 358 >(IH x) // ]] 359 359 qed. … … 487 487 [ #l' elim l' // #he #tl #IH #ABS normalize in ABS; destruct 488 488  #he1 #tl1 #IH #l' cases l' [ #ABS normalize in ABS; destruct ] 489 #he2 #tl2 #EQ whd in EQ:(??%%) ⊢ (??%%) >(IH tl2) destruct normalize in e1 ⊢ %>e0 //489 #he2 #tl2 #EQ whd in EQ:(??%%) ⊢ (??%%); >(IH tl2) destruct normalize in e1 ⊢ %; >e0 // 490 490 >e0 in e1; normalize #H @H ] 491 491 qed. … … 498 498 do fl ← map_partial … (*prefix_funct_name*) transf_partial_function (prog_funct ?? p); ?. 499 499 (*CSC: interactive mode because of dependent types *) 500 generalize in match (map_partial_preserves_first … transf_partial_variable (prog_vars … p)) 500 generalize in match (map_partial_preserves_first … transf_partial_variable (prog_vars … p)); 501 501 cases (map_partial … transf_partial_variable (prog_vars … p)) 502 502 [ #vl #EQ
Note: See TracChangeset
for help on using the changeset viewer.