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
    | aa@i
    | oo
    | oo
    | s1 s2obs𝖦_to_𝒯 s1 obs𝖦_to_𝒯 s2
    | s1 s2obs𝖦_to_𝒯 s1 obs𝖦_to_𝒯 s2
    | s1 s2obs𝖦_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 xmap (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]
    | st | st | s tsup 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 ifst 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.