Set Implicit Arguments.

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

Class FanGraph (G : Graph) :=
  {
  an : vertex → list vertex;
  an_spec : ∀ a b, a ∈ an b ↔ a ⌣ b
  }.

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

  Reserved Notation " x =fan y " (at level 80).

  Inductive fan_ax : relation observation :=
  | fan_clique_neg α :
      (π α → ⊥o) =fan ⋁ (map (fun a ⇒ ⦑a⦒) (flat_map an $α))
  where " x =fan y " := (fan_ax x y).
  Notation FAN := (ha_ax (+) (obs'_ax (+) fan_ax)).
  Hint Constructors fan_ax : core.

  Remark eo_fan_clique_neg α :
    FAN ⊢ (π α → ⊥o) ≡ ⋁ (map (fun a ⇒ ⦑a⦒) (flat_map an $α)).

  Global Instance FAN_Obs :
    subrelation (equiv_Obs Obs') (equiv_Obs FAN).

  Proposition FAN_sound : subrelation FAN sequiv.

  Definition join__f (p : fcliques×fcliques) :
    { l : list fcliques | FAN ⊢ ⋁ (map π l) ≡ π (fst p) ⟑ π(snd p) }.
  Defined.

  Fixpoint Conj (L : list (list fcliques)) : list fcliques :=
    match L with
    | [] ⇒ [[]@@empt]
    | l::L ⇒ flat_map (fun p ⇒ $ (join__f p)) (pairs l (Conj L))
    end.

  Lemma Conj_spec L :
    FAN ⊢ ⋀ (map (fun l ⇒ ⋁ (map π l)) L) ≡ ⋁ (map π (Conj L)).

  Fixpoint nf (s : observation) : list fcliques :=
    match s with
    | ⊤o ⇒ [[]@@empt]
    | ⊥o ⇒ []
    | ⦑a⦒ ⇒ [sgl__f a]
    | s ⟇ t ⇒ nf s ++ nf t
    | s ⟑ t ⇒ Conj [nf s;nf t]
    | s → t ⇒
        Conj (map
                (fun x : fcliques ⇒
                   (map sgl__f (flat_map an $x))
                     ++ flat_map
                     (fun y : fcliques ⇒
                        Conj (map (fun b ⇒ [sgl__f b]) ($y − $x)))
                     (nf t))
                (nf s))
    end.

  Lemma impl_cliques x y :
    FAN ⊢ π x → π y ≡ (π x → ⊥o) ⟇ ⋀ (map o_obs ($y − $ x)).

  Lemma impl_disj x l :
    FAN ⊢ π x → ⋁ l ≡ (π x → ⊥o) ⟇ ⋁ (map (o_impl (π x)) l).

  Lemma impl_disj_cliques x l :
    FAN ⊢ (π x → ⋁ (map π l))
        ≡ (π x → ⊥o) ⟇ ⋁ (map (fun y ⇒ ⋀ (map o_obs ($y − $ x))) l).

  Proposition nf_spec s : FAN ⊢ ⋁ (map π (nf s)) ≡ s.

  Theorem eo_inf_complete :
    ∀ s t : observation, s ≲ t ↔ FAN ⊢ s ≦ t .

  Theorem eo_inf_dec :
    ∀ s t : observation, DecidableProp (s ≲ t).
  Corollary eo_ax_complete :
    ∀ s t : observation, s ≃ t ↔ FAN ⊢ s ≡ t .

  Proposition fan_choose_clique : choose_clique G.

  Fixpoint finsat (x : fcliques) s :=
    match s with
    | ⊤o ⇒ True
    | ⊥o ⇒ False
    | ⦑u⦒ ⇒ u ∈ $ x
    | o1 ⟇ o2 ⇒ finsat x o1 ∨ finsat x o2
    | o1 ⟑ o2 ⇒ finsat x o1 ∧ finsat x o2
    | o1 → o2 ⇒ ∀ y, finsat y o1 → $x ⊆ $y → finsat y o2
    end.

  Lemma finsat_spec x s : finsat x s ↔ !x ⊨ s.

  Lemma sat_iff_inf_finsat α s : α ⊨ s ↔ ∃ x, α ⊃ ! x ∧ finsat x s.
End s.