Library Obs.product

Set Implicit Arguments.

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

Section s.
  Context { Idx : Set } { decIdx : decidable_set Idx }.
  Context { 𝖦 : Idx β†’ Graph } { dec𝖦 : βˆ€ i, DecidableGraph (𝖦 i) }.
  Context { choose_clique_𝖦 : βˆ€ i, choose_clique (𝖦 i)}.
  Notation V := (fun i β‡’ @vertex (𝖦 i)).

  Inductive 𝒱 : Set :=
  | node (i : Idx) (a : V i).

  Arguments node i a : clear implicits.
  Notation " a @' i " := (node i a) (at level 5).

  Definition eq𝒱 (u v : 𝒱) : bool.
  Defined.
  Remark eq𝒱_proj1 i j a b : a@'i = b@'j β†’ i = j.
  Remark eq𝒱_proj2 i a b : a@'i = b@'i β†’ a = b.


  Inductive coh𝒒 : relation 𝒱 :=
  | coh_i i a b : a ⁐ b β†’ coh𝒒 a@'i b@'i
  | coh_ij i j a b : i β‰  j β†’ coh𝒒 a@'i b@'j.
  Hint Constructors coh𝒒 : core.

  Lemma coh𝒒_refl : Reflexive coh𝒒.
  Lemma coh𝒒_sym : Symmetric coh𝒒.

  Instance 𝒒 : Graph :=
    {
    vertex := 𝒱;
    coh := coh𝒒;
    coh_refl := coh𝒒_refl;
    coh_sym := coh𝒒_sym
    }.

  Notation " a @ i " := (a @' i : @vertex 𝒒) (at level 20).

  Instance dec𝒒 : DecidableGraph 𝒒.

  Lemma incoh_iff_same_component_and_incoh u v :
    u ⌣ v ↔ βˆƒ i a b, u = a@i ∧ v = b@i ∧ a ⌣ b.

  Lemma dec_in_proj i Ξ± v : DecidableProp (βˆƒ a, v = a@i ∧ a ⊨ Ξ±).
  Lemma dec_compat_proj i Ξ± v : DecidableProp (βˆƒ a, v = a@i ∧ a β‹Š Ξ±).

  Definition incompat_inject (i : Idx) (Ξ± : @clique (𝖦 i)) (a : 𝒱)
    : option 𝒱.
  Defined.



  Definition inject i (Ξ± : @clique (𝖦 i)) : @clique 𝒒.

  Remark inject_i_member (i : Idx) (v : @vertex 𝒒) (Ξ± : @clique (𝖦 i)) :
    v ⊨ (@inject i Ξ±) ↔ (βˆƒ a : V i, v = a@i ∧ a ⊨ Ξ±).
  Remark inject_i_incompat i v Ξ± :
    v β‹Š inject Ξ± ↔ (βˆƒ a, v = a@i ∧ a β‹Š Ξ±).

  Opaque inject.


  Definition incompat_project (i : Idx) (Ξ± : clique) (a : V i)
    : option (V i).
  Defined.
  Definition project i (Ξ± : clique) : @clique (𝖦 i).

  Arguments project i Ξ± : clear implicits.

  Notation " Ξ± ⇂ i " := (project i Ξ±) (at level 5).

  Lemma project_spec i a Ξ± : a ⊨ (Ξ± ⇂ i) ↔ (a @ i) ⊨ Ξ±.

  Lemma project_inject i Ξ± : (inject Ξ±) ⇂ i ≃ Ξ±.

  Lemma join_project i Ξ± Ξ² :
    Ξ± ⇂ i ≲ Ξ² β†’
    βˆƒ Ξ³ : clique, Ξ³ ⇂ i ≃ Ξ² ∧ βˆ€ j, j β‰  i β†’ Ξ³ ⇂ j ≃ Ξ± ⇂ j.
  Lemma join_project' i Ξ± Ξ² :
    Ξ± ⇂ i ≲ Ξ² β†’ βˆƒ Ξ³ : clique, Ξ³ ⇂ i ≃ Ξ² ∧ Ξ± ≲ Ξ³.

  Notation 𝖳 := (fun i β‡’ @observation (𝖦 i)).

  Definition 𝒯 := @observation 𝒒.

  Fixpoint obs𝖦_to_𝒯 i (s : 𝖳 i) : 𝒯 :=
    match s with
    | ⦑aβ¦’ β‡’ ⦑a@iβ¦’
    | ⊀o β‡’ ⊀o
    | βŠ₯o β‡’ βŠ₯o
    | s1 βŸ‡ s2 β‡’ obs𝖦_to_𝒯 s1 βŸ‡ obs𝖦_to_𝒯 s2
    | s1 βŸ‘ s2 β‡’ obs𝖦_to_𝒯 s1 βŸ‘ obs𝖦_to_𝒯 s2
    | s1 β†’ s2 β‡’ obs𝖦_to_𝒯 s1 β†’ obs𝖦_to_𝒯 s2
    end.
  Arguments obs𝖦_to_𝒯 i s : clear implicits.

  Notation " s .{ i }" := (obs𝖦_to_𝒯 i s) (at level 5).

  Lemma obs𝖦_to_𝒯_sat i s Ξ± :
    Ξ± ⊨ s.{i} ↔ Ξ± ⇂ i ⊨ s.

  Lemma choose_clique_aux I (c d : βˆ€ i : Idx, 𝖳 i) Ξ± :
    (βˆƒ i, i ∈ I ∧ βˆ€ Ξ², Ξ± ≲ Ξ² β†’ Ξ² ⊨ (d i).{i} β†’ Ξ² ⊨ (c i).{i})
    βˆ¨ (βˆƒ Ξ², Ξ± ≲ Ξ² ∧ βˆ€ i, i ∈ I β†’ Ξ² ⊨ (d i).{i} ∧ Β¬ Ξ² ⊨ (c i).{i}) .

  Definition termVect := βˆ€ i : Idx, 𝖳 i.
  Definition NF := list termVect.
  Definition mapNF : list Idx β†’ termVect β†’ list 𝒯 :=
    fun l x β‡’ map (fun i β‡’ (x i).{i}) l.

  Definition conj_interp : list Idx β†’ list termVect β†’ 𝒯 :=
    fun l v β‡’ β‹€ (map (fun x β‡’ ⋁ (mapNF l x)) v).
  Definition disj_interp : list Idx β†’ list termVect β†’ 𝒯 :=
    fun l v β‡’ ⋁ (map (fun x β‡’ β‹€ (mapNF l x)) v).


  Context { 𝖠 : βˆ€ i : Idx, relation (@observation (𝖦 i)) }.
  Arguments 𝖠 i : clear implicits.

  Hypothesis 𝖠_complete :
    βˆ€ i, βˆ€ s t : 𝖳 i, 𝖠 i ⊒ s ≑ t ↔ s ≃ t.
  Corollary 𝖠_complete_inf :
    βˆ€ i, βˆ€ s t : 𝖳 i, 𝖠 i ⊒ s ≦ t ↔ s ≲ t.

  Reserved Notation " x =π’œ y " (at level 80).
  Inductive prod_ax : relation 𝒯 :=
  | prod_idx i s t : 𝖠 i s t β†’ s.{i} =π’œ t.{i}
  | prod_impl idx x y :
      (β‹€ (mapNF idx x) β†’ ⋁ (mapNF idx y))
      =π’œ ⋁ (mapNF idx (fun i β‡’ x i β†’ y i))
  where " x =π’œ y " := (prod_ax x y).
  Notation π’œ := (ha_ax (+) (obs_ax (+) prod_ax)).

  Remark eo_prod_impl idx x y :
    π’œ ⊒ (β‹€ (mapNF idx x) β†’ ⋁ (mapNF idx y))
      β‰‘ ⋁ (mapNF idx (fun i β‡’ x i β†’ y i)).


  Instance obs𝖦_to_𝒯_proper i :
    Proper (equiv_Obs (𝖠 i) ==> equiv_Obs π’œ) (obs𝖦_to_𝒯 i).

  Instance obs𝖦_to_𝒯_proper_inf i :
    Proper (inf_obs (𝖠 i) ==> inf_obs π’œ) (obs𝖦_to_𝒯 i).




  Lemma π’œ_sound : subrelation π’œ sequiv.

  Definition dnf_support (dnf : NF) I :=
    βˆ€ n i, n ∈ dnf β†’ Β¬ i ∈ I β†’ (n i) = ⊀o.
  Definition cnf_support (cnf : NF) I :=
    βˆ€ n i, n ∈ cnf β†’ Β¬ i ∈ I β†’ (n i) = βŠ₯o.

  Fixpoint dnf_to_cnf I (dnf : NF) :=
    match dnf with
    | [] β‡’ [fun _ β‡’ βŠ₯o]
    | n::d β‡’ (flat_map (fun nc β‡’
                         map (fun i j β‡’
                                if i =?= j
                                then (n j βŸ‡ nc j)
                                else (nc j))
                             I) (dnf_to_cnf I d))
    end.
  Fixpoint cnf_to_dnf I (cnf : NF) :=
    match cnf with
    | [] β‡’ [fun _ β‡’ ⊀o]
    | n::c β‡’ (flat_map (fun nd β‡’
                         map (fun i j β‡’
                                if i =?= j
                                then (n j βŸ‘ nd j)
                                else (nd j))
                             I) (cnf_to_dnf I c))
    end.
  Lemma cnf_to_dnf_support I c : dnf_support (cnf_to_dnf I c) I.
  Lemma dnf_to_cnf_support I d : cnf_support (dnf_to_cnf I d) I.
  Lemma cnf_to_dnf_equiv I c :
    π’œ ⊒ disj_interp I (cnf_to_dnf I c) ≑ conj_interp I c.


  Lemma dnf_to_cnf_equiv I (dnf : NF) :
    π’œ ⊒ conj_interp I (dnf_to_cnf I dnf) ≑ disj_interp I dnf.

  Instance cnf_support_proper_incl c :
    Proper (@incl Idx ==> Basics.impl) (cnf_support c).
  Instance dnf_support_proper_incl d :
    Proper (@incl Idx ==> Basics.impl) (dnf_support d).
  Instance cnf_support_proper c :
    Proper (@equivalent Idx ==> iff) (cnf_support c).
  Instance dnf_support_proper d :
    Proper (@equivalent Idx ==> iff) (dnf_support d).

  Lemma cnf_support_incl I J (cnf : NF) :
    cnf_support cnf I β†’ I βŠ† J β†’
    π’œ ⊒ conj_interp I cnf ≑ conj_interp J cnf.

  Lemma dnf_support_incl I J (dnf : NF) :
     dnf_support dnf I β†’ I βŠ† J β†’
      π’œ ⊒ disj_interp I dnf ≑ disj_interp J dnf.

  Definition atTop i (a : V i) : termVect.
  Defined.

  Fixpoint sup s :=
    match s with
    | ⊀o | βŠ₯o β‡’ []
    | ⦑_@'iβ¦’ β‡’ [i]
    | sβŸ‡t | sβŸ‘t | s β†’ t β‡’ sup s ++ sup t
    end.

  Fixpoint normal_form s : list termVect:=
    match s with
    | ⊀o β‡’ [fun _ β‡’ ⊀o]
    | βŠ₯o β‡’ []
    | ⦑a@'iβ¦’ β‡’ [atTop a]
    | s βŸ‡ t β‡’ (normal_form s)++(normal_form t)
    | s βŸ‘ t β‡’
      cnf_to_dnf (sup s++sup t)
                 ((dnf_to_cnf (sup s++sup t) (normal_form s))
                    ++(dnf_to_cnf (sup s++sup t) (normal_form t)))
    | s β†’ t β‡’
      cnf_to_dnf (sup s++sup t)
                 (map (fun p i β‡’ (snd p iβ†’fst p i))
                      (pairs (dnf_to_cnf (sup s++sup t)
                                         (normal_form t))
                             (normal_form s)))
    end.

  Lemma normal_form_sup s : dnf_support (normal_form s) (sup s).

  Lemma normal_form_eq s :
    π’œ ⊒ s ≑ disj_interp (sup s) (normal_form s).


  Theorem π’œ_complete s t :
    π’œ ⊒ s ≑ t ↔ s ≃ t.

  Instance product_sat_dec :
    βˆ€ Ξ± s, DecidableProp (Ξ± ⊨ s).

  Lemma auxiliary i I Ξ± Ξ² Ξ³ :
     Ξ± ≲ Ξ² β†’ Ξ± ⇂ i ≲ Ξ³ β†’
    βˆƒ Ξ΄ : clique,
      (Ξ± ≲ Ξ΄) ∧ (Ξ΄ ⇂ i ≃ Ξ³)
      βˆ§ (βˆ€ j : Idx, i β‰  j β†’j ∈ I β†’ Ξ΄ ⇂ j ≃ Ξ² ⇂ j).

  Lemma product_choose_clique : choose_clique 𝒒.

End s.