source: src/ASM/FoldStuff.ma @ 1119

Last change on this file since 1119 was 1062, checked in by mulligan, 10 years ago

separated jmeq and coercions from foldstuff.ma in order to fix the ongoing mess in util.ma surrounding reduce_strong

File size: 1.7 KB
Line 
1include "ASM/Util.ma".
2include "ASM/JMCoercions.ma".
3
4let 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
10  [ nil ⇒ λprf. ?
11  | cons hd tl ⇒ λprf. ?
12  ].
13  [ > (append_nil ?)
14    @ acc
15  | applyS (foldl_strong_internal A P l H (prefix @ [hd]) tl ? ?)
16    [ @ (H prefix hd tl prf acc)
17    | applyS prf
18    ]
19  ]
20qed.
21
22definition foldl_strong ≝
23  λA: Type[0].
24  λP: list A → Type[0].
25  λl: list A.
26  λH: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]).
27  λacc: P [ ].
28    foldl_strong_internal A P l H [ ] l acc (refl …).
29
30let rec foldr_strong_internal
31 (A:Type[0])
32 (P: list A → Type[0])
33 (l: list A)
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
37   [ nil ⇒ λprf. acc
38   | cons hd tl ⇒ λprf. H prefix hd tl prf (foldr_strong_internal A P l H (prefix @ [hd]) tl acc ?) ].
39 applyS prf
40qed.
41
42lemma foldr_strong:
43 ∀A:Type[0].
44  ∀P: list A → Type[0].
45   ∀l: list A.
46    ∀H: ∀prefix,hd,tl. l = prefix @ [hd] @ tl → P tl → P (hd::tl).
47     ∀acc:P [ ]. P l
48 ≝ λA,P,l,H,acc. foldr_strong_internal A P l H [ ] l acc (refl …).
49
50lemma 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/
52qed.
Note: See TracBrowser for help on using the repository browser.