source: src/ASM/FoldStuff.ma @ 3033

Last change on this file since 3033 was 1600, checked in by sacerdot, 8 years ago

utilities and ASM ported to the new standard library

File size: 1.7 KB
Line 
1include "ASM/Util.ma".
2include "basics/russell.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. mk_Prod 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.