Module ListAdom


Require Import
  Utf8 Coqlib Util AdomLib.

Local Unset Elimination Schemes.
Set Implicit Arguments.

Section DOM.

  Context (t B: Type)
          (GAMMA: gamma_op t B).

Pre-lattice structure: point-wise order, point-wise join (give up if the lists have different lenghts.

  Let list_join_func (j: t → t → t+⊤) :=
    λ acc x y,
    do acc <- acc;
    do z <- j x y;
    ret (z :: acc).

  Let list_join_rev_app j x y acc :=
    fold_left2 (list_join_func j) (λ _ _, All) (λ _ _, All) x y acc.

  Lemma list_join_All j :
    ∀ x y, fold_left2 (list_join_func j) (λ _ _, All) (λ _ _, All) x y All = All.
Proof.
    induction x; destruct y; simpl; auto.
  Qed.

  Lemma list_join_prop j :
    ∀ x a b y acc,
      list_join_rev_app j (a::x) (b::y) acc =
      do acc <- acc;
      do c <- j a b;
      list_join_rev_app j x y (Just (c :: acc)).
Proof.
    intros x a b y [|acc]; simpl.
    apply list_join_All. unfold list_join_func. simpl.
    destruct (j a b) as [|c]. apply (list_join_All j x y). reflexivity.
  Qed.

  Let appt {A} a b := do a <- a; do b <- b; ret (@app A a b).

  Lemma lift_rev_appt {A} :
    ∀ x y,
      fmap (@rev' A) (appt x y) = appt (fmap (@rev' A) y) (fmap (@rev' A) x).
Proof.
    destruct y as [|y]; destruct x as [|x]; try reflexivity.
    simpl. apply (f_equal (@Just _)). unfold rev'. repeat rewrite <- rev_alt. apply rev_app_distr.
  Qed.

  Lemma list_join_app j x :
    ∀ y a b,
      list_join_rev_app j x y (appt a b) = appt (list_join_rev_app j x y a) b.
Proof.
    induction x as [|a x IH]. destruct y; reflexivity.
    destruct y as [|b y]. reflexivity.
    simpl.
    intros a' b'.
    rewrite <- IH. f_equal. unfold list_join_func, appt.
    destruct a' as [|a']. reflexivity.
    destruct b' as [|b']; destruct (j a b) as [|c]; reflexivity.
  Qed.

  Instance list_join (J:join_op t (t+⊤)) : join_op (list t) ((list t)+⊤) :=
    fun x y => fmap (@rev' t) (list_join_rev_app join x y (Just nil)).

  Lemma list_join_cons j a x b y :
    list_join j (a::x) (b::y) = do c <- a ⊔ b; do l <- list_join j x y; ret (c :: l).
Proof.
    unfold list_join at 1. rewrite list_join_prop.
    simpl.
    destruct (a ⊔ b) as [|c]. reflexivity. simpl.
    change (Just (c::nil)) with (appt (Just nil) (Just (c :: nil))).
    rewrite list_join_app. etransitivity. apply lift_rev_appt. reflexivity.
  Qed.

  Definition list_widen (widen:t -> t -> (t+⊤)) : list t -> list t -> (list t)+⊤ :=
    fun x y => fmap (@rev' t) (list_join_rev_app widen x y (Just nil)).

  Lemma list_widen_cons w a x b y :
    list_widen w (a::x) (b::y) = do c <- w a b; do l <- list_widen w x y; ret (c :: l).
Proof.
    unfold list_widen at 1. rewrite list_join_prop. simpl.
    destruct (w a b) as [|c]. reflexivity.
    simpl.
    change (Just (c::nil)) with (appt (Just nil) (Just (c :: nil))).
    rewrite list_join_app. etransitivity. apply lift_rev_appt. reflexivity.
  Qed.

  Instance list_leb (L:leb_op t) : leb_op (list t) := forallb2 leb.

  Instance list_gamma : gamma_op (list t) (list B) :=
    λ l lb, Forall2 (λ a b, b ∈ a) (map γ l) lb.

  Lemma Forall2_nil_l {X Y} (P: X → Y → Prop) (l: list X) :
    Forall2 P l nil →
    l = nil.
Proof.
    intros H.
    set (d (l': list X) (n: list Y) := if n then l' = nil else True).
    change (d l nil). destruct H; simpl; auto.
  Qed.

  Lemma gamma_cons_inv x b l :
    (b :: l) ∈ γ(x) →
    ∃ a y,
      x = a :: y ∧ b ∈ γ(a) ∧ l ∈ γ(y).
Proof.
    inversion 1.
    match goal with
      | H : appcontext[map] |- _ =>
        destruct (map_cons_inv _ _ (eq_sym H)) as (? & ? & ? & ? & ?);
        subst
    end.
    repeat econstructor; eauto.
  Qed.

  Lemma gamma_cons_inv_r a x l :
    l ∈ γ(a :: x) →
    ∃ b y,
      l = b :: y ∧ b ∈ γ(a) ∧ y ∈ γ(x).
Proof.
    inversion 1. subst.
    eexists _, _. split. reflexivity. intuition.
  Qed.

  Lemma gamma_nil_r l : l ∈ γ(nil) → l = nil.
Proof.
    exact (λ H,
    match H in Forall2 _ u v return match u return Prop with nil => v = nil | _ => True end with
    | Forall2_nil => eq_refl
    | Forall2_cons _ _ _ _ _ _ => I
    end).
  Qed.

  Lemma gamma_nil_l l : nil ∈ γ(l) → l = nil.
Proof.
    exact (λ H, map_eq_nil _ _ (Forall2_nil_l H)).
  Qed.

  Instance list_leb_correct (L:leb_op t) :
    leb_op_correct t B -> leb_op_correct (list t) (list B).
Proof.
    intros HH x y H. unfold leb, list_leb in H. rewrite forallb2_forall in H.
    induction H; intros a A; inv A.
    constructor.
    constructor.
    eapply leb_correct; eauto.
    fold (map γ l'). apply IHForall2. auto.
  Qed.

  Instance list_join_correct (J:join_op t (t+⊤)) :
    join_op_correct t (t+⊤) B -> join_op_correct (list t) (list t+⊤) (list B).
Proof.
    intros HH x y a. revert y x.
    induction a as [|b a IH].
    + intros y x [K|K];
      apply Forall2_nil_l in K; apply map_eq_nil in K; subst.
      destruct y; constructor.
      destruct x; constructor.
    + intros y x [K|K]; destruct (gamma_cons_inv K) as (u & v & ? & U & V); clear K;
      subst.
      destruct y as [|c y]. constructor. unfold join. rewrite list_join_cons.
      specialize (HH _ c _ (or_introl U)).
      specialize (IH y _ (or_introl V)).
      destruct join. constructor. simpl.
      unfold join in IH. simpl in IH.
      destruct list_join; constructor; auto.
      destruct x as [|c x]. constructor. simpl. unfold join. rewrite list_join_cons.
      specialize (HH c _ _ (or_intror U)).
      specialize (IH _ x (or_intror V)).
      destruct join. constructor. simpl.
      unfold join in IH. simpl in IH.
      destruct list_join; constructor; auto.
  Qed.

  Lemma list_widen_incr (W:t->t->t+⊤) :
    (∀ x y, γ x ⊆ γ (W x y)) ->
    ∀ x y, γ x ⊆ γ (list_widen W x y).
Proof.
    intros HH x y a. revert y x.
    induction a as [|b a IH].
    + intros y x K;
      apply Forall2_nil_l in K; apply map_eq_nil in K; subst.
      destruct y; constructor.
    + intros y x K; destruct (gamma_cons_inv K) as (u & v & ? & U & V); clear K;
      subst.
      destruct y as [|c y]. constructor. simpl. rewrite list_widen_cons.
      specialize (HH _ c _ U).
      specialize (IH y _ V).
      destruct (W u c). constructor. simpl.
      simpl in IH. destruct list_widen; constructor; auto.
  Qed.

End DOM.

Existing Instances list_join list_leb list_gamma.
Existing Instances list_join_correct list_leb_correct.
Generated by coq2html