F* tutorial : Exercise 4f

foldl.fst

(* https://www.fstar-lang.org/tutorial/ *)
module FoldLeft

val append : list 'a -> list 'a -> Tot (list 'a)
let rec append l1 l2 = match l1 with
  | [] -> l2
  | hd :: tl -> hd :: append tl l2

val reverse: list 'a -> Tot (list 'a)
let rec reverse = function 
  | [] -> []
  | hd::tl -> append (reverse tl) [hd]
let snoc l h = append l [h]

val fold_left: f:('b -> 'a -> Tot 'a) -> l:list 'b -> 'a -> Tot 'a
let rec fold_left f l a =
    match l with
    | [] -> a
    | hd::tl -> fold_left f tl (f hd a)

val append_assoc: l1:list 'a -> l2:list 'a -> l3:list 'a ->
        Lemma (append (append l1 l2) l3 = append l1 (append l2 l3))
let rec append_assoc l1 l2 l3 =
    match l1 with
    | [] -> ()
    | hd :: tl -> append_assoc tl l2 l3
(*induction_hyp:
append (append tl l2) l3 = append tl (append l2 l3)

append (append (hd::tl) l2) l3 =? append (hd::tl) (append l2 l3)
lhs
= append (hd :: (append tl l2)) l3
= hd :: (append (append tl l2) l3)
rhs
= hd :: (append tl (append l2 l3))
= hd :: (append (append tl l2) l3)

append (hd :: l) l3
= hd :: (append l l3)
*)

val fold_left_cons_is_reverse: l:list 'a -> l':list 'a ->
                             Lemma (fold_left Cons l l' = append (reverse l) l')
let rec fold_left_cons_is_reverse l l' =
    match l with
    | [] -> ()
    | hd::tl -> fold_left_cons_is_reverse tl (Cons hd l');
                append_assoc (reverse tl) [hd] l'
(*induction_hyp
fold_left Cons tl l' = append (reverse tl) l'

fold_left Cons (hd::tl) l' =? append (reverse (hd::tl)) l'
fold_left Cons (hd::tl) l'
= fold_left Cons tl (Cons hd l')        (fold_left)
= append (reverse tl) (Cons hd l')      (induction_hyp)
append (reverse (hd::tl)) l'
= append (append (reverse tl) [hd]) l'  (reverse)
= append (reverse tl) (hd :: l')        (append_assoc)
*)