weblib/Cerco/ASM/FoldStuff.ma

   1 include "ASM/Util.ma".
   2 include "ASM/JMCoercions.ma".
   3
   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
  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   ]
  20 qed.
  21
  22 definition 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
  30 let 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
  40 qed.
  41
  42 lemma 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
  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/
  52 qed.