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
| ⦑a⦒ ⇒ ⦑a@i⦒
| ⊤o ⇒ ⊤o
| ⊥o ⇒ ⊥o
| s1 ⟇ s2 ⇒ obs𝖦_to_𝒯 s1 ⟇ obs𝖦_to_𝒯 s2
| s1 ⟑ s2 ⇒ obs𝖦_to_𝒯 s1 ⟑ obs𝖦_to_𝒯 s2
| s1 → s2 ⇒ obs𝖦_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 x ⇒ map (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]
| s⟇t | s⟑t | s → t ⇒ sup 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 i→fst 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.
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
| ⦑a⦒ ⇒ ⦑a@i⦒
| ⊤o ⇒ ⊤o
| ⊥o ⇒ ⊥o
| s1 ⟇ s2 ⇒ obs𝖦_to_𝒯 s1 ⟇ obs𝖦_to_𝒯 s2
| s1 ⟑ s2 ⇒ obs𝖦_to_𝒯 s1 ⟑ obs𝖦_to_𝒯 s2
| s1 → s2 ⇒ obs𝖦_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 x ⇒ map (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]
| s⟇t | s⟑t | s → t ⇒ sup 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 i→fst 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.