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.