Library Obs.sem_obs

Set Implicit Arguments.

Require Import notations decidable_prop list_dec.
Require Export syntax_obs equiv_obs.

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

Semantics of observation terms

The semantics is given by a satisfaction relation, specifying which cliques belong to the language of a term.

  Global Instance satObs : Satisfaction clique observation :=
    fix satObs (x : clique) (o : observation) :=
      match o with
      | ⊤o ⇒ True
      | ⊥o ⇒ False
      | ⦑u⦒ ⇒ u ⊨ x
      | o1 ⟇ o2 ⇒ satObs x o1 ∨ satObs x o2
      | o1 ⟑ o2 ⇒ satObs x o1 ∧ satObs x o2
      | o1 → o2 ⇒
          ∀ y, satObs y o1 → y ⊃ x → satObs y o2
      end.

  Remark sat_top x : x ⊨ ⊤o ↔ True.
  Remark sat_bot x : x ⊨ ⊥o ↔ False.
  Remark sat_at x u : x ⊨ ⦑u ⦒ ↔ u ⊨ x.
  Remark sat_disj x o1 o2 : x ⊨ (o1 ⟇ o2 ) ↔ x ⊨ o1 ∨ x ⊨ o2.
  Remark sat_conj x o1 o2 : x ⊨ (o1 ⟑ o2 ) ↔ x ⊨ o1 ∧ x ⊨ o2.
  Remark sat_impl x o1 o2 :
    x ⊨ (o1 → o2 ) ↔ ∀ y, y ⊨ o1 → y ⊃ x → y ⊨ o2.

  Hint Rewrite sat_top sat_bot sat_at sat_disj sat_conj sat_impl
    : simpl_typeclasses.

  Global Instance satObs_proper :
    Proper (sequiv ==> sequiv ==> iff) satisfies.

  Global Instance satisfies_inf :
    Proper (ssmaller ==> ssmaller ==> Basics.impl) satisfies.

n-ary meets and joins.

Lemma satisfies_Join x A : x ⊨ (⋁ A ) ↔ ∃ a , a ∈ A ∧ x ⊨ a.

Lemma satisfies_Meet x A : x ⊨ (⋀ A ) ↔ ∀ a, a ∈ A → x ⊨ a.

Finite cliques

Remark π _spec x y : x ⊨ (π y ) ↔ x ⊃ ! y.

The problems of 1) satifiability for finite cliques 2) semantic containment of a pair of terms 3) semantic equivalence of a pair of terms are all equi-decidable.

  Remark dec_fsat_impl_dec_ssmaller :
    (∀ α s, DecidableProp (!α ⊨ s)) → ∀ s t, DecidableProp ( s ≲ t ).
  Remark dec_ssmaller_impl_dec_fsat :
    (∀ s t, DecidableProp ( s ≲ t )) → (∀ α s, DecidableProp (!α ⊨ s)).
  Remark dec_sequiv_impl_dec_ssmaller :
    (∀ s t, DecidableProp (s ≃ t)) → ∀ s t, DecidableProp ( s ≲ t ).
  Remark dec_ssmaller_impl_dec_sequiv :
    (∀ s t, DecidableProp (s ≲ t)) → ∀ s t, DecidableProp ( s ≃ t ).

The following property will be useful to combine observation algebras.

  Definition choose_clique :=
    ∀ (α : clique) (s t : observation),
      {∀ β, β ⊃ α → β ⊨ s → β ⊨ t } + {∃ β , β ⊃ α ∧ β ⊨ s ∧ ¬ β ⊨ t }.

It implies the decidability of satisfiability.

  Lemma choose_clique_sat_dec :
    choose_clique → ∀ α s, DecidableProp (α ⊨ s).

End s.

Infix " ⊨ " := satisfies (at level 10).
Arguments choose_clique : clear implicits.
Global Hint Rewrite @sat_top @sat_bot @sat_at @sat_disj @sat_conj
       @sat_impl
    : simpl_typeclasses.

Proposition eo_sound `{Graph} 𝖠 :
  (subrelation 𝖠 sequiv ) → ∀ a b, 𝖠 ⊢ a ≡ b → a ≃ b.

Proposition ha_sound `{Graph} : subrelation ha_ax sequiv.

Proposition Obs_sound `{DecidableGraph} :
  subrelation Obs sequiv.

Proposition Obs'_sound {G : Graph} {decG : DecidableGraph G} :
  subrelation Obs' sequiv.