Library Obs.fin_sem_obs

Set Implicit Arguments.

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 ↔ (∃ b, b ∈ u ∧ a ⌣ b) ∨ a ∈ v.

  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.

  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 ⇒
          ∀ y, fsatisfies y o1 →
               x ↯↯ y ∨ ∃ z, fjoins x y z ∧ fsatisfies z o2
      end.

  Remark fsat_top x : x ⊨ ⊤o ↔ True.
  Remark fsat_bot x : x ⊨ ⊥o ↔ False.
  Remark fsat_at x u : x ⊨ ⦑u⦒ ↔ u ⊨ x.
  Remark fsat_disj x o1 o2 : x ⊨ (o1 ⟇ o2) ↔ x ⊨ o1 ∨ x ⊨ o2.
  Remark fsat_conj x o1 o2 : x ⊨ (o1 ⟑ o2) ↔ x ⊨ o1 ∧ x ⊨ o2.
  Remark fsat_impl x o1 o2 :
    x ⊨ (o1 → o2) ↔
      (∀ y, y ⊨ o1 → x ↯↯ y ∨ ∃ z, fjoins x y z ∧ z ⊨ o2).

  Proposition fcliques_sat_iff_fsat s (α : fcliques) :
    ! α ⊨ s ↔ α ⊨ s.

  Corollary clique_sat_iff_fsat_proj s (α : clique) :
    α ⊨ s ↔ (⎣s⎦ @@ α) ⊨ s.

  Corollary incl_sem_iff_incl_fin_sem s t :
    @ssmaller _ clique _ s t ↔ @ssmaller _ fcliques _ s t.

End s.