commit by user andrea

[helm.git] / weblib / Cerco / ASM / FoldStuff.ma

diff --git a/weblib/Cerco/ASM/FoldStuff.ma b/weblib/Cerco/ASM/FoldStuff.ma
new file mode 100644 (file)
index 0000000..a2b3a45
--- /dev/null
+++ b/weblib/Cerco/ASM/FoldStuff.ma
@@ -0,0 +1,52 @@
+include "ASM/Util.ma".
+include "ASM/JMCoercions.ma".
+
+let rec foldl_strong_internal
+  (A: Type[0]) (P: list A → Type[0]) (l: list A)
+  (H: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]))
+  (prefix: list A) (suffix: list A) (acc: P prefix) on suffix:
+    l = prefix @ suffix → P(prefix @ suffix) ≝
+  match suffix return λl'. l = prefix @ l' → P (prefix @ l') with
+  [ nil ⇒ λprf. ?
+  | cons hd tl ⇒ λprf. ?
+  ].
+  [ > (append_nil ?)
+    @ acc
+  | applyS (foldl_strong_internal A P l H (prefix @ [hd]) tl ? ?)
+    [ @ (H prefix hd tl prf acc)
+    | applyS prf
+    ]
+  ]
+qed.
+
+definition foldl_strong ≝
+  λA: Type[0].
+  λP: list A → Type[0].
+  λl: list A.
+  λH: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]).
+  λacc: P [ ].
+    foldl_strong_internal A P l H [ ] l acc (refl …).
+
+let rec foldr_strong_internal
+ (A:Type[0])
+ (P: list A → Type[0])
+ (l: list A)
+ (H: ∀prefix,hd,tl. l = prefix @ [hd] @ tl → P tl → P (hd::tl))
+ (prefix: list A) (suffix: list A) (acc: P [ ]) on suffix : l = prefix@suffix → P suffix ≝
+  match suffix return λl'. l = prefix @ l' → P (l') with
+   [ nil ⇒ λprf. acc
+   | cons hd tl ⇒ λprf. H prefix hd tl prf (foldr_strong_internal A P l H (prefix @ [hd]) tl acc ?) ].
+ applyS prf
+qed.
+
+lemma foldr_strong:
+ ∀A:Type[0].
+  ∀P: list A → Type[0].
+   ∀l: list A.
+    ∀H: ∀prefix,hd,tl. l = prefix @ [hd] @ tl → P tl → P (hd::tl).
+     ∀acc:P [ ]. P l
+ ≝ λA,P,l,H,acc. foldr_strong_internal A P l H [ ] l acc (refl …).
+
+lemma pair_destruct: ∀A,B,a1,a2,b1,b2. pair A B a1 a2 = 〈b1,b2〉 → a1=b1 ∧ a2=b2.
+ #A #B #a1 #a2 #b1 #b2 #EQ destruct /2/
+qed.