Library Obs.laws

Set Implicit Arguments.

Require Import notations decidable_prop list_dec.
Require Import equiv_obs.

Useful laws of Heyting algebras


Section s.

Basic laws

  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 (ab) a b.
  Remark eo_impl_concl a b : A⁺ b (ab) b.
  Remark eo_impl_distr a b c : A⁺ a (b c) (ab) (ac).

  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.

inf_obs A⁺ is a partial order with respect to equiv_Obs

  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.

Lattice properties

  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⁺ ab 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 bc.

  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.

Properties of the implication

  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 bc.
  Lemma eo_curry a b c : A⁺ (a b) c a (bc).

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

Additional laws

n-ary meets and joins

  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).

Finite and singleton cliques

  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.