Set Implicit Arguments.

Require Import notations Bool.
Require Import decidable_prop.
Require Import list_dec.

Class Graph :=
  {
  vertex : Set ;
  coh : relation vertex ;
  coh_refl :> Reflexive coh;
  coh_sym :> Symmetric coh
  }.

Section s.
  Context {G : Graph}.
  Infix " ⁐ " := coh (at level 40).

  Definition incoh : relation vertex := fun a b ⇒ ¬ a ⁐ b.
  Infix " ⌣ " := incoh (at level 40).

  Global Instance incoh_irrefl : Irreflexive incoh.

  Global Instance incoh_sym : Symmetric incoh.

  Class clique : Set :=
    {
    member : vertex → bool;
    incompat : vertex → option vertex;
    members_are_coh :
      ∀ a b, Is_true (member a) → Is_true (member b) → a ⁐ b;
    incompat_Some :
      ∀ a b, incompat a = Some b → Is_true (member b) ∧ a ⌣ b;
    incompat_None :
      ∀ a b, incompat a = None → Is_true (member b) → a ⁐ b
    }.

  Arguments member α a : rename, clear implicits.
  Arguments incompat α a : rename, clear implicits.

  Arguments members_are_coh α : rename, clear implicits.
  Arguments incompat_Some α : rename, clear implicits.
  Arguments incompat_None { α a b}: rename.

  Notation " u ⋊ x " := (∃ b, (incompat x u) = Some b) (at level 20).
  Notation " u ∝ x " := (incompat x u = None) (at level 20).

  Global Instance satClique : Satisfaction vertex clique :=
    (fun u x ⇒ Is_true (member x u)).

  Lemma incompat_are_incoh a α :
    a ⋊ α ↔ ∃ b, b ⊨ α ∧ a ⌣ b.

  Lemma compat_are_coh a α :
    a ∝ α ↔ ∀ b, b ⊨ α → a ⁐ b.

  Global Instance incompat_dec a α : DecidableProp (a ⋊ α).

  Global Instance compat_dec a α : DecidableProp (a ∝ α).

  Notation inf_cliques := (fun a b ⇒ b ≲ a).
  Infix " ⊃ " := inf_cliques (at level 20).

  Lemma inf_clique_compat α β :
    α ⊃ β → ∀ a, a ⋊ β → a ⋊ α.

  Definition incompatible : relation clique :=
    fun x y ⇒ ∃ a b, a ⊨ x ∧ b ⊨ y ∧ a ⌣ b.

  Infix " ↯ " := incompatible (at level 50).

  Remark incompatible_incompat α β :
    α ↯ β ↔ ∃ a, a ⊨ α ∧ a ⋊ β.

  Global Instance irrefl_incompatible : Irreflexive incompatible.

  Global Instance sym_incompatible : Symmetric incompatible.

  Global Instance incompatible_inf :
    Proper (inf_cliques ==> inf_cliques ==> Basics.flip Basics.impl)
           incompatible.

  Global Instance incompatible_eq :
    Proper (sequiv ==> sequiv ==> iff) incompatible.

  Definition empt : clique.

  Lemma empt_spec a : ¬ a ⊨ empt.
  Opaque empt.

  Remark empt_max x : x ⊃ empt.

  Definition joins (x y z : clique) :=
    ∀ a, a ⊨ z ↔ a ⊨ x ∨ a ⊨ y.

  Global Instance joins_proper :
    Proper (sequiv ==> sequiv ==> sequiv ==> iff) joins.

End s.
Infix " ⁐ " := coh (at level 40).
Infix " ⌣ " := incoh (at level 40).
Arguments member {G} α a : rename.
Arguments incompat {G} α a : rename.

Notation " u ⋊ x " := (∃ b, (incompat x u) = Some b) (at level 20).
Notation " u ∝ x " := (incompat x u = None) (at level 20).
Infix " ↯ " := incompatible (at level 50).

Arguments members_are_coh {G} α : rename.
Arguments incompat_are_incoh {G} α : rename.
Arguments incompat_Some α : rename, clear implicits.
Arguments incompat_None { α a b}: rename.

Notation inf_cliques := (fun a b ⇒ b ≲ a).
Infix " ⊃ " := inf_cliques (at level 20).

Class DecidableGraph G :=
  {
    decidable_vertex :> decidable_set (@vertex G);
    decidale_coh :> ∀ u v, DecidableProp (u ⁐ v)
  }.

Section decidable_graph.

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

  Global Instance decidable_incoh u v : DecidableProp (u ⌣ v).

  Lemma not_incompatible_is_joins x y : ¬ x ↯ y ↔ ∃ z, joins x y z.

  Lemma joins_is_meet x y z :
    joins x y z ↔ (z ⊃ x ∧ z ⊃ y ∧ ∀ t, t ⊃ x → t ⊃ y → t ⊃ z).

End decidable_graph.

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

  Definition is_coherent (α : list vertex) :=
    ∀ a b, a ∈ α → b∈α → a ⁐ b.

  Global Instance decidable_is_coherent α :
    DecidableProp (is_coherent α).

  Definition fcliques :=
    { α : list vertex | test (is_coherent α) = true}.

  Remark fcliques_coherent (α : fcliques) : is_coherent ($α).

  Arguments fcliques_coherent : clear implicits.

  Notation inf_fcliques := (fun a b : fcliques ⇒ $ b ⊆ $ a).
  Infix " ⊃f " := inf_fcliques (at level 20).
  Notation eq_fcliques := (fun a b : fcliques ⇒ $ a ≈ $ b).

  Definition fcmem (α : fcliques) := fun a ⇒ inb a $α.

  Lemma fcmem_coh α a b :
    Is_true (fcmem α a) → Is_true (fcmem α b) → a ⁐ b.

  Definition fcic (α : fcliques) :=
    fun a ⇒ match (fun b ⇒ test (a ⌣ b)):> $α with
          | [] ⇒ None
          | b::_ ⇒ Some b
          end.

  Lemma fcic_Some α a b :
    fcic α a = Some b → Is_true (fcmem α b) ∧ a ⌣ b.
  Lemma fcic_None α a b :
    fcic α a = None → Is_true (fcmem α b) → a ⁐ b.

  Definition fc_to_clique (α : fcliques) : clique
    := Build_clique (@fcmem_coh α) (@fcic_Some α) (@fcic_None α).

  Notation " ! " := fc_to_clique.

  Lemma fc_to_clique_spec a α : a ⊨ (! α) ↔ a ∈ $ α.

  Ltac simpl_fc :=
    repeat (rewrite fc_to_clique_spec in *).
  Opaque fc_to_clique.

  Global Instance fc_to_clique_proper :
    Proper (inf_fcliques ==> inf_cliques) fc_to_clique.

  Global Instance fc_to_clique_proper_eq :
    Proper (eq_fcliques ==> sequiv) fc_to_clique.

  Remark fc_to_clique_iff α β : α ⊃f β ↔ ! α ⊃ ! β.

  Definition fincompatible (x y : fcliques) :=
    ∃ a b, a ∈ $x ∧ b ∈ $y ∧ a ⌣ b.
  Infix " ↯↯ " := fincompatible (at level 50).

  Lemma fincompatible_incompatible x y :
    x ↯↯ y ↔ ! x ↯ ! y.

  Global Instance irrefl_fincompatible : Irreflexive fincompatible.

  Global Instance sym_fincompatible : Symmetric fincompatible.

  Global Instance fincompatible_inf :
    Proper (inf_fcliques ==> inf_fcliques ==> Basics.flip Basics.impl)
           fincompatible.

  Global Instance fincompatible_eq :
    Proper (eq_fcliques ==> eq_fcliques ==> iff) fincompatible.

  Global Instance decidable_incompatible_f x y :
    DecidableProp (x ↯↯ y).

  Definition fjoins (x y z : fcliques) := ($ z ≈ $ x ++ $y).

  Global Instance fjoins_proper :
    Proper (eq_fcliques ==> eq_fcliques ==> eq_fcliques ==> iff) fjoins.

  Lemma fjoins_iff_joins x y z :
    fjoins x y z ↔ joins (! x) (! y) (! z).

  Lemma joins_is_meet_f x y z :
    fjoins x y z ↔ (z ⊃f x ∧ z ⊃f y ∧ ∀ t, t ⊃f x → t ⊃f y → t ⊃f z).

  Lemma not_incompatible_is_joins_f x y :
    ¬ x ↯↯ y ↔ ∃ z : fcliques, fjoins x y z.

  Lemma incompatible_or_joins_f x y :
    {x ↯↯ y} + {∃ z, fjoins x y z}.

  Lemma decidable_incompatible_with_fcliques x α :
    DecidableProp (x ↯ ! α).

  Definition project_list : list vertex → clique → list vertex :=
    fun l x ⇒ member x :> l.

  Lemma is_coherent_project_list l x : is_coherent (project_list l x).
  Lemma project_proof l x : test (is_coherent (project_list l x)) = true.

  Definition project l (x : clique) : fcliques :=
    exist _ (project_list l x) (project_proof l x).

  Infix " @@ " := project (at level 20).

  Lemma project_spec a l x : a ∈ $ (l@@x) ↔ a ⊨ x ∧ a ∈ l.

  Lemma project_incl l x : $ (l @@ x) ⊆ l.

  Lemma project_larger l x : x ⊃ ! (l @@ x).

  Lemma project_max l x α : $ α ⊆ l → x ⊃ ! α → l @@ x ⊃f α.

  Lemma project_project l m α :
    $(l @@ !(m @@ α)) ≈ $((l∩m) @@ α).

  Global Instance project_proper :
    Proper (@equivalent _ ==> sequiv ==> eq_fcliques) project.

  Global Instance project_proper_inf :
    Proper (Basics.flip(@incl _) ==> inf_cliques ==> inf_fcliques) project.

  Lemma singleton_is_coherent a : is_coherent [a].

  Remark sglf_proof a : test (is_coherent [a]) = true.

  Definition sgl__f a : fcliques := (exist _ [a] (sglf_proof a)).

  Notation sgl := (fun a : vertex ⇒ !(sgl__f a) : clique).

  Lemma sgl_spec a b : a ⊨ (sgl b) ↔ a = b.

End finite_cliques.
Arguments fcliques_coherent : clear implicits.
Arguments fcliques_coherent {G} {decG}.
Ltac simpl_fc := repeat rewrite fc_to_clique_spec in ×.
Notation " ! " := fc_to_clique.
Infix " @@ " := project (at level 20).
Infix " ↯↯ " := fincompatible (at level 50).
Notation sgl := (fun a : vertex ⇒ !(sgl__f a) : clique).
Notation inf_fcliques := (fun a b : fcliques ⇒ $ b ⊆ $ a).
Infix " ⊃f " := inf_fcliques (at level 20).