Changeset 990 for src/ASM/FoldStuff.ma
 Timestamp:
 Jun 17, 2011, 1:30:01 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/FoldStuff.ma
r980 r990 76 76 foldl_strong_internal A P l H [ ] l acc (refl …). 77 77 78 let rec foldr_strong_internal 79 (A:Type[0]) 80 (P: list A → Type[0]) 81 (l: list A) 82 (H: ∀prefix,hd,tl. l = prefix @ [hd] @ tl → P tl → P (hd::tl)) 83 (prefix: list A) (suffix: list A) (acc: P [ ]) on suffix : l = prefix@suffix → P suffix ≝ 84 match suffix return λl'. l = prefix @ l' → P (l') with 85 [ nil ⇒ λprf. acc 86  cons hd tl ⇒ λprf. H prefix hd tl prf (foldr_strong_internal A P l H (prefix @ [hd]) tl acc ?) ]. 87 applyS prf 88 qed. 89 90 lemma foldr_strong: 91 ∀A:Type[0]. 92 ∀P: list A → Type[0]. 93 ∀l: list A. 94 ∀H: ∀prefix,hd,tl. l = prefix @ [hd] @ tl → P tl → P (hd::tl). 95 ∀acc:P [ ]. P l 96 ≝ λA,P,l,H,acc. foldr_strong_internal A P l H [ ] l acc (refl …). 97 78 98 lemma pair_destruct: ∀A,B,a1,a2,b1,b2. pair A B a1 a2 = 〈b1,b2〉 → a1=b1 ∧ a2=b2. 79 99 #A #B #a1 #a2 #b1 #b2 #EQ destruct /2/
Note: See TracChangeset
for help on using the changeset viewer.