2 include "ASM/JMCoercions.ma".
4 let rec foldl_strong_internal
5 (A: Type[0]) (P: list A → Type[0]) (l: list A)
6 (H: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]))
7 (prefix: list A) (suffix: list A) (acc: P prefix) on suffix:
8 l = prefix @ suffix → P(prefix @ suffix) ≝
9 match suffix return λl'. l = prefix @ l' → P (prefix @ l') with
11 | cons hd tl ⇒ λprf. ?
15 | applyS (foldl_strong_internal A P l H (prefix @ [hd]) tl ? ?)
16 [ @ (H prefix hd tl prf acc)
22 definition foldl_strong ≝
26 λH: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]).
28 foldl_strong_internal A P l H [ ] l acc (refl …).
30 let rec foldr_strong_internal
34 (H: ∀prefix,hd,tl. l = prefix @ [hd] @ tl → P tl → P (hd::tl))
35 (prefix: list A) (suffix: list A) (acc: P [ ]) on suffix : l = prefix@suffix → P suffix ≝
36 match suffix return λl'. l = prefix @ l' → P (l') with
38 | cons hd tl ⇒ λprf. H prefix hd tl prf (foldr_strong_internal A P l H (prefix @ [hd]) tl acc ?) ].
46 ∀H: ∀prefix,hd,tl. l = prefix @ [hd] @ tl → P tl → P (hd::tl).
48 ≝ λA,P,l,H,acc. foldr_strong_internal A P l H [ ] l acc (refl …).
50 lemma pair_destruct: ∀A,B,a1,a2,b1,b2. pair A B a1 a2 = 〈b1,b2〉 → a1=b1 ∧ a2=b2.
51 #A #B #a1 #a2 #b1 #b2 #EQ destruct /2/