Require Import

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: ttt+⊤) :=
λ 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 <- ab; do l <- list_join j x y; ret (c :: l).
Proof.
unfold list_join at 1. rewrite list_join_prop.
simpl.
destruct (ab) 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, Forall2a b, ba) (map γ l) lb.

Lemma Forall2_nil_l {X Y} (P: XYProp) (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 :: yb ∈ γ(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 :: yb ∈ γ(a) ∧ y ∈ γ(x).
Proof.
inversion 1. subst.
eexists _, _. split. reflexivity. intuition.
Qed.

Lemma gamma_nil_r l : l ∈ γ(nil) → l = nil.
Proof.
exactH,
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.
exactH, 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.