Obs.fin_sem_obs

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Require Import notations decidable_prop list_dec.
Require Import sem_obs fan.

Section s.
  Context {G : Graph}
          {decG : DecidableGraph G}
          {fanG : FanGraph G}.

  Definition impl_lst u v := flat_map an u ++ v.
  Lemma impl_lst_spec a u v :
    a impl_lst u v <-> (exists b, b u /\ a b) \/ a v.
  Proof.
    unfold impl_lst;rewrite in_app_iff,in_flat_map.
    setoid_rewrite an_spec;reflexivity.
  Qed.

  Fixpoint support s :=
    match s with
    | o | o => []
    | a => [a]
    | s t | s t => support s ++ support t
    | s t => impl_lst (support s) (support t)
    end.
  Notation " ⎣ s ⎦ " := (support s).

  Lemma support_dominates_sem s x :
    x s <-> ! (⎣ s @@ x) s.
  Proof.
    revert x;induction s;intro x;simpl;rsimpl.
    - tauto.
    - tauto.
    - etransitivity;[|symmetry;apply fc_to_clique_spec].
      rewrite project_spec;simpl;tauto.
    - rewrite (IHs1 (! _)),(IHs2 (! _)).
      pose proof (@project_project _ _ s1 (s1++s2) x) as e.
      apply fc_to_clique_proper_eq in e as ->.
      pose proof (@project_project _ _ s2 (s1++s2) x) as e.
      apply fc_to_clique_proper_eq in e as ->.
      rewrite intersect_meet_l by (apply incl_appl;reflexivity).
      rewrite intersect_meet_l by (apply incl_appr;reflexivity).
      rewrite IHs1,IHs2;reflexivity.
    - rewrite (IHs1 (! _)),(IHs2 (! _)).
      pose proof (@project_project _ _ s1 (s1++s2) x) as e.
      apply fc_to_clique_proper_eq in e as ->.
      pose proof (@project_project _ _ s2 (s1++s2) x) as e.
      apply fc_to_clique_proper_eq in e as ->.
      rewrite intersect_meet_l by (apply incl_appl;reflexivity).
      rewrite intersect_meet_l by (apply incl_appr;reflexivity).
      rewrite IHs1,IHs2;reflexivity.
    - unfold ssmaller.
      setoid_rewrite fc_to_clique_spec.
      setoid_rewrite project_spec.
      setoid_rewrite impl_lst_spec.
      split.
      + intros h1 y hy1 h2.
        cut (exists z : clique, x z
                           /\ s2@@y f (s2@@z)
                           /\ s1@@z f (s1@@y)).
        * intros (z&hz1&hz2&hz3);apply IHs2.
          apply fc_to_clique_iff in hz2.
          rewrite <- hz2,<-IHs2.
          apply h1,hz1.
          apply IHs1.
          apply fc_to_clique_iff in hz3.
          rewrite <- hz3,<-IHs1.
          apply hy1.
        * clear h1 hy1 IHs1 IHs2.
          destruct (decidable_incompatible_with_fcliques x (s1@@y))
            as [i|i].
          -- destruct i as (a&b&ha&hb&hab).
             rewrite fc_to_clique_spec, project_spec in hb.
             exfalso.
             apply hab,(members_are_coh y);[|tauto].
             apply h2;split;[|left;exists b];tauto.
          -- apply not_incompatible_is_joins in i as (z&hz).
             pose proof hz as e.
             apply joins_is_meet in e as (e1&e2&e3).
             exists z;split;[|split].
             ++ apply e1.
             ++ intros a;unfold satisfies;repeat rewrite project_spec.
                intros (ha1&ha2);split;[|assumption].
                apply hz in ha1 as [ha1|ha1].
                ** apply h2; tauto.
                ** apply fc_to_clique_spec,project_spec in ha1;tauto.
             ++ transitivity ($ (s1 @@ !(⎣s1⎦@@ y))).
                ** rewrite project_project,intersect_meet_l;reflexivity.
                ** apply project_proper_inf,e2;reflexivity.
      + intros h y h1 h2;apply h;[assumption|].
        intros;apply h2;tauto.
  Qed.

  Instance finSat : Satisfaction fcliques observation :=
    fix fsatisfies (x : fcliques) (o : observation) :=
      match o with
      | o => True
      | o => False
      | u => u $ x
      | o1 o2 => fsatisfies x o1 \/ fsatisfies x o2
      | o1 o2 => fsatisfies x o1 /\ fsatisfies x o2
      | o1 o2 =>
          forall y, fsatisfies y o1 ->
               x ↯↯ y \/ exists z, fjoins x y z /\ fsatisfies z o2
      end.

  Remark fsat_top x : x o <-> True.
  Proof. reflexivity. Qed.
  Remark fsat_bot x : x o <-> False.
  Proof. reflexivity. Qed.
  Remark fsat_at x u : x u <-> u x.
  Proof. reflexivity. Qed.
  Remark fsat_disj x o1 o2 : x (o1 o2) <-> x o1 \/ x o2.
  Proof. reflexivity. Qed.
  Remark fsat_conj x o1 o2 : x (o1 o2) <-> x o1 /\ x o2.
  Proof. reflexivity. Qed.
  Remark fsat_impl x o1 o2 :
    x (o1 o2) <->
      (forall y, y o1 -> x ↯↯ y \/ exists z, fjoins x y z /\ z o2).
  Proof. reflexivity. Qed.

  Proposition fcliques_sat_iff_fsat s (α : fcliques) :
    ! α s <-> α s.
  Proof.
    revert α;induction s; simpl;auto;try tauto.
    - intro;apply fc_to_clique_spec.
    - intro a;rsimpl.
      rewrite IHs1,IHs2;reflexivity.
    - intro a;rsimpl;rewrite IHs1,IHs2;reflexivity.
    - intro α;rsimpl;rewrite fsat_impl;split.
      + intros h y hy.
        destruct (incompatible_or_joins_f α y) as [h'|(j&hj)];[tauto|].
        right;exists j;split;[assumption|].
        apply IHs2.
        pose proof hj as hh;apply joins_is_meet_f in hh as (hzx&hzy&hm).
        apply h.
        * apply fc_to_clique_iff in hzy.
          rewrite <-hzy;apply IHs1;assumption.
        * apply fc_to_clique_iff,hzx.
      + intros h y hys hya.
        apply support_dominates_sem in hys.
        apply IHs1 in hys.
        apply h in hys as [hys|(z&hz&hys)].
        * destruct hys as (a&b&ha&hb&i).
          apply fc_to_clique_spec,hya in ha.
          apply project_spec in hb as (hb1&hb2).
          exfalso;apply i,(members_are_coh y a b);assumption.
        * pose proof hz as hz'.
          apply joins_is_meet_f in hz' as (h1&h2&h3).
          apply IHs2 in hys.
          cut (!z y);[intros <-;assumption|].
          intros a ha.
          apply fc_to_clique_spec,hz,in_app_iff in ha as [ha|ha].
          -- apply hya,fc_to_clique_spec,ha.
          -- apply project_spec in ha; tauto.
  Qed.

  Corollary clique_sat_iff_fsat_proj s (α : clique) :
    α s <-> (s @@ α) s.
  Proof.
    rewrite support_dominates_sem,fcliques_sat_iff_fsat.
    reflexivity.
  Qed.

  Corollary incl_sem_iff_incl_fin_sem s t :
    @ssmaller _ clique _ s t <-> @ssmaller _ fcliques _ s t.
  Proof.
    split;intros h α .
    - apply fcliques_sat_iff_fsat,h,fcliques_sat_iff_fsat,.
    - rewrite <-project_larger.
      apply fcliques_sat_iff_fsat,h,clique_sat_iff_fsat_proj,.
  Qed.

End s.