Set Implicit Arguments.

Require Import notations decidable_prop list_dec.
Require Import equiv_obs sem_obs.
Require Import laws.

Section s.
  Context {V : Set} {decV : decidable_set V}.
  Hypothesis infiniteV : ∀ l : list V, ∃ a : V, ¬ a ∈ l.
  Context { a__o : V}.

  Instance Ω : Graph :=
    {
    vertex := V;
    coh := @eq V;
    coh_refl := @eq_Reflexive V;
    coh_sym := @eq_Symmetric V
    }.

  Instance decΩ : DecidableGraph Ω.

  Reserved Notation " x =Ω y " (at level 80).
  Inductive Ω_ax : relation observation :=
  | Ω_top' a b : ⦑a⦒⟇(⦑a⦒→⊥o) =Ω ⦑b⦒⟇(⦑b⦒→⊥o)
  | Ω_neg (X : list V) : ((⋁ (map o_obs X))→⊥o)→⊥o =Ω ⋁ (map o_obs X)
  where " x =Ω y " := (Ω_ax x y).
  Notation axΩ := (ha_ax (+) (obs_ax (+) Ω_ax)).
  Hint Constructors Ω_ax : core.

  Remark eo_Ω_top' a b : axΩ ⊢ ⦑a⦒⟇(⦑a⦒→⊥o) ≡ ⦑b⦒⟇(⦑b⦒→⊥o).
  Remark eo_Ω_neg X : axΩ ⊢ ((⋁ (map o_obs X))→⊥o)→⊥o ≡ ⋁ (map o_obs X).

  Notation "⊤'" := (⦑ a__o ⦒ ⟇ (⦑ a__o ⦒→⊥o)).

  Lemma top'_a a : axΩ ⊢ ⦑a⦒ ≦ ⊤'.

  Lemma top'_not_a a : axΩ ⊢ ⦑a⦒ → ⊥o ≦ ⊤'.

  Lemma top'_or_neg a b :
    a ≠ b → axΩ ⊢ ⊤' ≦ (⦑ a ⦒ → ⊥o) ⟇ (⦑ b ⦒ → ⊥o).
   Lemma neg_neg_axΩ a : axΩ ⊢ (⦑a⦒ → ⊥o)→ ⊥o ≡ ⦑a⦒.

  Lemma neg_top'_is_bot :
    axΩ ⊢ ⊤' → ⊥o ≡ ⊥o.

  Lemma weak_excluded_middle u :
    axΩ ⊢ ⊤' ≦ ⋁ (map o_obs u) ⟇ (⋁ (map o_obs u) → ⊥o).

  Remark Meet_not_and_sgl_not_in x u :
    ¬ x ∈ u → axΩ ⊢ ⋀ (map (fun a ⇒ ⦑ a ⦒ → ⊥o) u) ⟑ ⦑ x ⦒ ≡ ⦑ x ⦒.

  Remark Meet_not_and_sgl_in x u :
    x ∈ u →
    axΩ ⊢ ⋀ (map (fun a : V ⇒ ⦑ a ⦒ → ⊥o) u) ⟑ ⦑ x ⦒ ≡ ⊥o.

  Definition Obs__Ω := option (list V + list V)%type.
  Definition V' := option V.

  Instance sat__Ω : Satisfaction V' Obs__Ω :=
    fun x (o : Obs__Ω) ⇒
      match x,o with
      | _,None ⇒ True
      | Some a,Some (inl u) ⇒ ¬ a ∈ u
      | Some a,Some (inr u) ⇒ a ∈ u
      | _,_ ⇒ False
      end.

  Definition inf__Ω : Obs__Ω → Obs__Ω → bool :=
    fun x y ⇒
      match x,y with
      | _,None ⇒ true
      | Some(inl u),Some(inl v)
      | Some(inr v),Some(inr u) ⇒ inclb v u
      | Some(inr u),Some(inl v) ⇒ (u ∩ v) =?= []
      | _,_ ⇒ false
      end.

  Lemma complete_inf__Ω s t : inf__Ω s t = true ↔ s ≲ t.

  Remark cliques_at_most_one_elt (α : clique) a b :
    a ⊨ α → b ⊨ α → a = b.

  Corollary mem_is_sgl (α : clique) a : a ⊨ α ↔ α ≃ sgl a.

  Definition ξ : V' → clique :=
    fun x ⇒ match x with None ⇒ empt | Some a ⇒ sgl a end.

  Definition ζ : clique → V' :=
    fun α ⇒
      match (incompat α a__o) with
      | Some a ⇒ Some a
      | None ⇒ if member α a__o then Some a__o else None
      end.

  Lemma ζ_Some α a : ζ α = Some a → α ≃ sgl a.

  Lemma ζ_None α : ζ α = None → α ≃ empt.

  Corollary ξ_ζ α : ξ (ζ α) ≃ α.

  Lemma ζ_sgl a : ζ (sgl a) = Some a.

  Lemma ζ_empt : ζ empt = None.

  Corollary ζ_ξ x : ζ(ξ x) = x.

  Proposition axΩ_sound : subrelation axΩ sequiv.

  Corollary inf_axΩ_sound s t :
    axΩ ⊢ s ≦ t → s ≲ t.
  Corollary eq_axΩ_sound s t :
    axΩ ⊢ s ≡ t → s ≃ t.

  Definition τ (o : Obs__Ω) : observation :=
    match o with
    | None ⇒ ⊤o
    | Some (inl u) ⇒
      if u =?= []
      then ⊤'
      else ⋀ (map (fun a ⇒ ⦑ a ⦒ → ⊥o) u)
    | Some (inr u) ⇒ ⋁ (map o_obs u)
    end.

  Lemma τ_ζ α o : α ⊨ (τ o) → ζ α ⊨ o.

  Lemma τ_ξ α o : α ⊨ o → ξ α ⊨ (τ o).

  Lemma sound_τ_sat__Ω α o : α ⊨ (τ o) ↔ ζ α ⊨ o.

  Instance τ_proper_inf__Ω : Proper (ssmaller ==> inf_obs axΩ) τ.

  Instance dec_inf__Ω x y : DecidableProp (x ≲ y).

  Fixpoint to_Obs__Ω s : Obs__Ω :=
    match s with
    | ⊥o ⇒ Some (inr [])
    | ⊤o ⇒ None
    | ⦑a⦒ ⇒ Some (inr [a])
    | s⟇t ⇒ match (to_Obs__Ω s),(to_Obs__Ω t) with
            | None,_ | _,None ⇒ None
            | Some(inl u),Some(inl v) ⇒ Some(inl (u∩v))
            | Some(inr u),Some(inr v) ⇒ Some(inr (u++v))
            | Some(inl u),Some(inr v)
            | Some(inr v),Some(inl u) ⇒ Some(inl (u−v))
            end
    | s⟑t ⇒ match (to_Obs__Ω s),(to_Obs__Ω t) with
    | Some(inl u),Some(inl v) ⇒ Some(inl (u++v))
    | Some(inr u),Some(inr v) ⇒ Some(inr (u∩v))
    | Some(inl u),Some(inr v)
    | Some(inr v),Some(inl u) ⇒ Some(inr (v−u))
    | None,z | z,None ⇒ z
    end
    | s→t ⇒
        if inf__Ω (to_Obs__Ω s) (to_Obs__Ω t)
        then None
        else
          match (to_Obs__Ω s),(to_Obs__Ω t) with
          | x,None | None,x ⇒ x
          | Some (inl u),Some (inl v) ⇒ Some (inl (v − u))
          | Some (inr u),Some (inl v) ⇒ Some (inl (u ∩ v))
          | Some (inl u),Some (inr v) ⇒ Some (inr (u ++ v))
          | Some (inr u),Some (inr v) ⇒ Some (inl (u − v))
          end
    end.

  Lemma τ_join__Ω s t :
    axΩ ⊢ τ (to_Obs__Ω (s ⟇ t)) ≡ τ (to_Obs__Ω s) ⟇ τ (to_Obs__Ω t).

  Lemma τ_meet__Ω s t :
    axΩ ⊢ τ (to_Obs__Ω (s ⟑ t)) ≡ τ (to_Obs__Ω s) ⟑ τ (to_Obs__Ω t).

  Lemma τ_neg__Ω s : axΩ ⊢ τ (to_Obs__Ω (s→⊥o)) ≡ τ (to_Obs__Ω s) → ⊥o.

  Lemma τ_impl__Ω s t :
    axΩ ⊢ τ (to_Obs__Ω (s → t)) ≡ τ (to_Obs__Ω s) → τ (to_Obs__Ω t).

  Lemma τ_to_Obs__Ω s : axΩ ⊢ s ≡ τ (to_Obs__Ω s).

  Theorem completeness_anticlique s t :
    axΩ ⊢ s ≦ t ↔ s ≲ t.

  Corollary completeness_anticlique_eq s t :
    axΩ ⊢ s ≡ t ↔ s ≃ t.

    Corollary ξ_to_Obs__Ω x s : x ⊨ (to_Obs__Ω s) ↔ ξ x ⊨ s.

  Corollary sem_bij_to_Obs__Ω s t : to_Obs__Ω s ≲ to_Obs__Ω t ↔ s ≲ t.

  Instance dec_sat α (s : observation) : DecidableProp (α ⊨ s).

  Instance anticlique_dec_inf (s t : observation) :
    DecidableProp (s ≲ t).

  Lemma anticlique_inf_or_cntrex (s t : observation) :
    {s ≲ t} + {∃ β, β ⊨ s ∧ ¬ β ⊨ t}.

  Proposition anticlique_choose_clique : choose_clique Ω.

End s.