Set Implicit Arguments.

Require Import notations decidable_prop list_dec.
Require Import equiv_obs.

Section s.

  Context {G : Graph}.
  Context {A : relation observation}.
  Notation "A⁺" := (ha_ax (+) A).
  Remark HA_A s t : s =ha t → A⁺ ⊢ s ≡ t.
  Hint Resolve HA_A : core.

  Remark eo_and_ass a b c : A⁺ ⊢ a ⟑ (b ⟑ c) ≡ (a ⟑ b) ⟑ c.
  Remark eo_and_comm a b : A⁺ ⊢ a ⟑ b ≡ b ⟑ a.
  Remark eo_and_top a : A⁺ ⊢ a ⟑ ⊤o ≡ a.
  Remark eo_or_ass a b c : A⁺ ⊢ a ⟇ (b ⟇ c) ≡ (a ⟇ b) ⟇ c.
  Remark eo_or_comm a b : A⁺ ⊢ a ⟇ b ≡ b ⟇ a.
  Remark eo_or_bot a : A⁺ ⊢ a ⟇ ⊥o ≡ a.
  Remark eo_abs1 a b : A⁺ ⊢ a ⟇ (a ⟑ b) ≡ a.
  Remark eo_abs2 a b : A⁺ ⊢ a ⟑ (a ⟇ b) ≡ a.
  Remark eo_tauto a : A⁺ ⊢ a → a ≡ ⊤o.
  Remark eo_impl_premise a b : A⁺ ⊢ a ⟑ (a→b) ≡ a ⟑ b.
  Remark eo_impl_concl a b : A⁺ ⊢ b ⟑ (a→b) ≡ b.
  Remark eo_impl_distr a b c : A⁺ ⊢ a → (b ⟑ c) ≡ (a→b) ⟑ (a→c).

  Hint Resolve eo_and_ass eo_and_comm eo_and_top eo_or_ass eo_or_comm
       eo_or_bot eo_abs1 eo_abs2 eo_tauto eo_impl_premise eo_impl_concl
       eo_impl_distr : core.

  Remark eo_and_bot a : A⁺ ⊢ a ⟑ ⊥o ≡ ⊥o.

  Remark eo_or_top a : A⁺ ⊢ a ⟇ ⊤o ≡ ⊤o.

  Remark eo_and_idem a : A⁺ ⊢ a ⟑ a ≡ a.

  Remark eo_or_idem a : A⁺ ⊢ a ⟇ a ≡ a.

  Hint Resolve eo_or_idem eo_and_idem eo_or_top eo_and_bot: core.

  Global Instance inf_obs_preorder : PreOrder (inf_obs A⁺).

  Global Instance inf_obs_partialorder :
    PartialOrder (equiv_Obs A⁺) (inf_obs A⁺).

  Remark eq_obs_inf_obs :
    subrelation (equiv_Obs A⁺) (inf_obs A⁺).

  Hint Resolve eq_obs_inf_obs : core.

  Global Instance o_or_inf :
    Proper ((inf_obs A⁺) ==> (inf_obs A⁺) ==> (inf_obs A⁺)) o_or.

  Remark obs_join a b c : A⁺ ⊢ a ≦ c → A⁺ ⊢ b ≦ c → A⁺ ⊢ a⟇b ≦ c.
  Remark eo_inf_o_and a b : A⁺ ⊢ a ≦ b ↔ A⁺ ⊢ a ⟑ b ≡ a.
  Remark obs_meet a b c : A⁺ ⊢ a ≦ b → A⁺ ⊢ a ≦ c → A⁺ ⊢ a ≦ b⟑c.

  Remark eo_inf_or_l a b : A⁺ ⊢ a ≦ a ⟇ b.
  Remark eo_inf_or_r a b : A⁺ ⊢ b ≦ a ⟇ b.
  Remark eo_inf_and_l a b : A⁺ ⊢ a ⟑ b ≦ a.
  Remark eo_inf_and_r a b : A⁺ ⊢ a ⟑ b ≦ b.

  Hint Resolve eo_inf_or_l eo_inf_or_r eo_inf_and_l eo_inf_and_r : core.

  Remark eo_inf_or_left a c b : A⁺ ⊢ c ≦ a → A⁺ ⊢ c ≦ a ⟇ b.
  Remark eo_inf_or_right a b c : A⁺ ⊢ c ≦ b → A⁺ ⊢ c ≦ a ⟇ b.
  Remark eo_inf_and_left a b c : A⁺ ⊢ a ≦ c → A⁺ ⊢ a ⟑ b ≦ c.
  Remark eo_inf_and_right a b c : A⁺ ⊢ b ≦ c → A⁺ ⊢ a ⟑ b ≦ c.

  Global Instance o_and_inf :
    Proper ((inf_obs A⁺) ==> (inf_obs A⁺) ==> (inf_obs A⁺)) o_and.

  Lemma eo_inf_impl_right_mon a b c : A⁺ ⊢ b ≦ c → A⁺ ⊢ (a → b) ≦ (a → c).
  Lemma eo_inf_impl_concl a b : A⁺ ⊢ b ≦ a → b.
  Lemma eo_impl_mp a b : A⁺ ⊢ a ⟑ (a → b) ≦ b.
  Lemma eo_inf_o_impl a b : A⁺ ⊢ a ≦ b ↔ A⁺ ⊢ ⊤o ≦ a → b.

  Proposition eo_heyting a b c : A⁺ ⊢ a ⟑ b ≦ c ↔ A⁺ ⊢ a ≦ b→c.
  Lemma eo_curry a b c : A⁺ ⊢ (a ⟑ b) → c ≡ a → (b→c).

  Global Instance o_impl_inf :
    Proper (Basics.flip (inf_obs A⁺) ==> (inf_obs A⁺) ==> (inf_obs A⁺))
           o_impl.

  Lemma eo_distr1 a b c : A⁺ ⊢ a ⟇ (b ⟑ c) ≡ (a ⟇ b) ⟑ (a ⟇ c).
  Lemma eo_distr2 a b c : A⁺ ⊢ a ⟑ (b ⟇ c) ≡ (a ⟑ b) ⟇ (a ⟑ c).

  Lemma eo_impl_distr_left a b c : A⁺ ⊢ (a ⟇ b) → c ≡ (a → c) ⟑ (b→c).
  Lemma eo_inf_top a : A⁺ ⊢ a ≦ ⊤o.
  Lemma eo_inf_bot a : A⁺ ⊢ ⊥o ≦ a.
  Lemma eo_eq_top_iff_top_inf a : A⁺ ⊢ a ≡ ⊤o ↔ A⁺ ⊢ ⊤o ≦ a.
  Lemma eo_eq_bot_iff_inf_bot a : A⁺ ⊢ a ≡ ⊥o ↔ A⁺ ⊢ a ≦ ⊥o.
  Lemma eo_contradict s : A⁺ ⊢ s ⟑ (s → ⊥o) ≡ ⊥o.
  Remark eo_top_impl s : A⁺ ⊢ (⊤o → s) ≡ s.

  Remark obs_Meet a X : (∀ b, b ∈ X → A⁺ ⊢ a ≦ b) → A⁺ ⊢ a ≦ ⋀ X.

  Remark obs_Join a X : (∀ b, b ∈ X → A⁺ ⊢ b ≦ a) → A⁺ ⊢ ⋁ X ≦ a.

  Remark Join_app X Y : A⁺ ⊢ ⋁ (X++Y) ≡ ⋁ X ⟇ ⋁ Y.
  Remark Meet_app X Y : A⁺ ⊢ ⋀ (X++Y) ≡ ⋀ X ⟑ ⋀ Y.

  Remark eo_inf_in_Join a X : a ∈ X → A⁺ ⊢ a ≦ ⋁ X.
  Remark eo_inf_in_Meet a X : a ∈ X → A⁺ ⊢ ⋀ X ≦ a.

  Lemma and_Join a X : A⁺ ⊢ a ⟑ ⋁ X ≡ ⋁ (map (fun b ⇒ a ⟑ b) X).

  Lemma or_Meet a X : A⁺ ⊢ a ⟇ ⋀ X ≡ ⋀ (map (fun b ⇒ a ⟇ b) X).

  Lemma Join_and_Join X Y :
    A⁺ ⊢ ⋁ X ⟑ ⋁ Y ≡ ⋁ (map (fun p ⇒ fst p ⟑ snd p) (pairs X Y)).

  Lemma Meet_or_Meet X Y :
    A⁺ ⊢ ⋀ X ⟇ ⋀ Y ≡ ⋀ (map (fun p ⇒ fst p ⟇ snd p) (pairs X Y)).

  Instance Meet_monotone :
    Proper (@incl observation ==> Basics.flip (inf_obs A⁺)) ⋀.
  Instance Join_monotone : Proper (@incl observation ==> (inf_obs A⁺)) ⋁.
  Instance Meet_equiv :
    Proper (@equivalent observation ==> equiv_Obs A⁺) ⋀.
  Instance Join_equiv :
    Proper (@equivalent observation ==> equiv_Obs A⁺) ⋁.


  Lemma Meet_map_equiv_pointwise {X Ax} f g l :
    (∀ x : X, x ∈ l → Ax ⊢ f x ≡ g x) →
    Ax ⊢ ⋀ (map f l) ≡ ⋀ (map g l).

  Lemma flat_map_Meet {X}:
    ∀ f (l : list X), A⁺ ⊢ ⋀ (flat_map f l) ≡ ⋀ (map ⋀ (map f l)).

  Lemma Join_map_equiv_pointwise {X Ax} f g l :
    (∀ x : X, x ∈ l → Ax ⊢ f x ≡ g x) →
    Ax ⊢ ⋁ (map f l) ≡ ⋁ (map g l).

  Lemma flat_map_Join {X} :
    ∀ f (l : list X), A⁺ ⊢ ⋁ (flat_map f l) ≡ ⋁ (map ⋁ (map f l)).
  Lemma eo_impl_Join u s :
    A⁺ ⊢ ⋁ u → s ≡ ⋀ (map (fun x ⇒ x → s) u).
  Corollary impl_Join u s :
    A⁺ ⊢ ⋁ (map o_obs u) → s ≡ ⋀ (map (fun a ⇒ ⦑a⦒ → s) u).

  Lemma eo_Meet_impl u s :
    A⁺ ⊢ s → ⋀ u ≡ ⋀ (map (fun x ⇒ s → x) u).
  Corollary Meet_impl u s :
    A⁺ ⊢ s → ⋀ (map o_obs u) ≡ ⋀ (map (fun a ⇒ s → ⦑a⦒) u).

  Context {decG : DecidableGraph G}.

  Global Instance π_proper : Proper (inf_fcliques ==> (inf_obs A⁺)) π.

  Remark var_clique a : A⁺ ⊢ π (sgl__f a) ≡ ⦑a⦒.

End s.

Ltac split_order :=
  apply inf_obs_partialorder;unfold Basics.flip;split.
Ltac unfold__lat :=
  repeat apply obs_meet || apply obs_join
  ||((apply obs_Join||apply obs_Meet);
    let x := fresh "x" in
    let hx := fresh "hx" in
    let a := fresh "a" in
    let ha := fresh "ha" in
    intros x hx;apply in_map_iff in hx as (a&<-&ha)).
Ltac unfold_meet :=
  apply obs_Meet;
  let x := fresh "x" in
  let hx := fresh "hx" in
  let a := fresh "a" in
  let ha := fresh "ha" in
  intros x hx;apply in_map_iff in hx as (a&<-&ha).
Ltac unfold_join :=
  apply obs_Join;
  let x := fresh "x" in
  let hx := fresh "hx" in
  let a := fresh "a" in
  let ha := fresh "ha" in
  intros x hx;apply in_map_iff in hx as (a&<-&ha).

Global Hint Resolve eo_or_idem eo_and_idem eo_or_top eo_and_bot
       eo_inf_or_l eo_inf_or_r eo_inf_and_l eo_inf_and_r
       eo_and_ass eo_and_comm eo_and_top eo_or_ass eo_or_comm
       eo_or_bot eo_abs1 eo_abs2 eo_tauto eo_impl_premise eo_impl_concl
       eo_impl_distr : equiv_obs.