HyPre.util.ApplyLf

From Coq Require Import Lists.List.
From Coq Require Import Program.Basics.
Open Scope program_scope.

Import ListNotations.

Definition lift {X Y : Type} (f : X -> Y) (P : X -> Prop) : Y -> Prop
  := fun y => exists x, P x /\ f x = y.

(* TODO fix code duplication (see HyperSimSpecial) *)
Fixpoint fold_right_lf {X X' Y : Type} (lf : X -> Y -> list X' * Y) (lf_init : Y) xl : list X' * Y
  := match xl with
     | [] => ([], lf_init)
     | x :: xl => let (xl', y) := fold_right_lf lf lf_init xl in
                let (x', y') := lf x y in
                (x' ++ xl', y')
     end.
(* TODO: just realized something:
   apply_lf is equivalent to fold_right (with app) where state information is preserved,
   e.g. using product types.
   and an additional use of map where state information is possibly removed.
   I am probably better of with separating both parts
   and using the lemmas existing for fold_right & map.
   It still might be useful to mask this combination of methods and prove lemmas about it.
 *)
Definition apply_lf {X X' Y : Type} (lf : X -> Y -> list X' * Y) (lf_init : Y) xl : list X'
  := fst (fold_right_lf lf lf_init xl).

Definition apply_lf' {X X' : Type} (lf : X -> list X')
  := apply_lf (fun x (_ : unit) => (lf x,tt)) tt.

Lemma fold_right_lf_cons (X X' Y : Type) (lf : X -> Y -> list X' * Y) (lf_init : Y) (xl : list X) (x : X)
  : fold_right_lf lf lf_init (x :: xl)
    = let (xl', y) := fold_right_lf lf lf_init xl in
      let (x', y') := lf x y in (x' ++ xl', y').
Proof.
  cbn. reflexivity.
Qed.

Lemma fold_right_lf_app {X X' Y : Type} (lf : X -> Y -> list X' * Y) (y0 : Y) xl1 xl2
  : fold_right_lf lf y0 (xl2 ++ xl1)
    = let (xl1',y1) := fold_right_lf lf y0 xl1 in
      let (xl2',y2) := fold_right_lf lf y1 xl2 in
      (xl2' ++ xl1', y2).
Proof.
  induction xl2;cbn.
  - destruct (fold_right_lf lf y0 xl1).
    reflexivity.
  - rewrite IHxl2.
    destruct (fold_right_lf lf y0 xl1).
    destruct (fold_right_lf lf y xl2).
    destruct (lf a y1).
    f_equal.
    eapply app_assoc.
Qed.

Lemma apply_lf_app {X X' Y : Type} (lf : X -> Y -> list X' * Y) (y0 : Y) xl1 xl2
  : apply_lf lf y0 (xl2 ++ xl1) = apply_lf lf (snd (fold_right_lf lf y0 xl1)) xl2 ++ apply_lf lf y0 xl1.
Proof.
  unfold apply_lf.
  rewrite fold_right_lf_app.
  destruct (fold_right_lf lf y0 xl1).
  cbn.
  destruct (fold_right_lf lf y xl2).
  cbn.
  reflexivity.
Qed.

Lemma apply_lf'_S {X X' : Type} (lf : X -> list X') b a
  : apply_lf' lf (b :: a) = lf b ++ apply_lf' lf a.
Proof.
  revert b.
  induction a;intros;cbn.
  - reflexivity.
  - rewrite IHa.
    unfold apply_lf', apply_lf.
    cbn.
    match goal with |- _ = _ ++ _ ++ fst ?x => destruct x end.
    cbn.
    reflexivity.
Qed.

Lemma apply_lf'_app {X X' : Type} (a b : list X) (lf : X -> list X')
  : apply_lf' lf (b ++ a) = apply_lf' lf b ++ apply_lf' lf a.
Proof.
  revert a.
  induction b;intros;cbn.
  - reflexivity.
  - setoid_rewrite apply_lf'_S.
    rewrite IHb.
    rewrite app_assoc.
    reflexivity.
Qed.

Lemma apply_lf'_compose {L1 L2 L3 : Type} (l1 : L1 -> L2) (l2 : L2 -> list L3) x
  : apply_lf' (l2 ∘ l1) x = apply_lf' l2 (map l1 x).
Proof.
  induction x;cbn.
  - reflexivity.
  - setoid_rewrite apply_lf'_S.
    rewrite IHx.
    f_equal.
Qed.