Library CharacteristicLogics
Require Import SfLib.
Require Import LibTactics.
Require Import BisimTheory.
Section HML_DecoupledBisimulation.
Variable lts: labeled_transition_system.
Import Stepping.
Require Import ClassicalFacts.
Inductive phiA : Type :=
| top: phiA
| conj: phiA→phiA→phiA
| all: list lts_L→phiE→phiA
with phiE: Type :=
| bot: phiE
| disj: phiE→phiE→phiE
| ext: list lts_L→phiA→phiE
.
Inductive phi : Type :=
| phi1: phiA→phi
| phi2: phiE→phi.
Fixpoint forcesA (p:lts_S) (f:phiA) : Prop := match f with
| top ⇒ True
| conj f1 f2 ⇒ forcesA p f1 ∧ forcesA p f2
| all la f ⇒ ∀ p', step_star p la p' → forcesE p' f
end
with forcesE (p:lts_S) (f:phiE) : Prop := match f with
| bot ⇒ False
| disj f1 f2 ⇒ forcesE p f1 ∨ forcesE p f2
| ext la f ⇒ ∃ p', step_star p la p' ∧ forcesA p' f
end.
Definition topE:= (ext nil top).
Definition botA:= (all nil bot).
Fixpoint negA f := match f with
| top ⇒ bot
| conj f1 f2 ⇒ disj (negA f1) (negA f2)
| all la f1 ⇒ ext la (negE f1)
end
with negE f := match f with
| bot ⇒ top
| disj f1 f2 ⇒ conj (negE f1) (negE f2)
| ext la f1 ⇒ all la (negA f1)
end.
Lemma topE_correct: ∀ p, forcesE p topE ↔ forcesA p top.
Proof.
simpl; split; intros.
auto.
∃ p; split; auto. apply step_nil.
Qed.
Lemma botA_correct: ∀ p, forcesA p botA ↔ forcesE p bot.
Proof.
simpl; split; intros; auto.
eapply H; apply step_nil.
Qed.
Lemma negA_correct1: ∀ p f, forcesE p (negA f) → ¬forcesA p f
with negE_correct1: ∀ p f, forcesA p (negE f) → ¬forcesE p f.
Proof.
× induction f; simpl; intros.
- intuition.
- intuition.
- intro.
destruct H as [p'[??]].
apply H0 in H.
eapply negE_correct1; eauto.
× induction f; simpl; intros.
intuition.
intuition.
intros [p'[??]].
apply H in H0.
eapply negA_correct1; eauto.
Qed.
Fixpoint list_conjA (lf: list phiA) := match lf with
| nil ⇒ top
| f::lf' ⇒ conj f (list_conjA lf')
end.
Lemma f_list_conjA: ∀ p lf,
forcesA p (list_conjA lf) ↔ (∀ f, In f lf → forcesA p f).
Proof.
induction lf; simpl; intros.
× intuition.
× setoid_rewrite IHlf. intuition. subst; eauto.
Qed.
Fixpoint list_disjE (lf: list phiE) := match lf with
| nil ⇒ bot
| f::lf' ⇒ disj f (list_disjE lf')
end.
Lemma f_list_disjE: ∀ p lf,
forcesE p (list_disjE lf) ↔ (∃ f, In f lf ∧ forcesE p f).
Proof.
induction lf; simpl; intros.
× intuition. destruct H as [?[??]]; auto.
× setoid_rewrite IHlf. clear IHlf. intuition. subst; eauto.
destruct H0 as [?[??]]; eauto.
destruct H as [?[[?|?]?]]; subst; eauto.
Qed.
Delimit Scope scopeA with scopeA.
Delimit Scope scopeE with scopeE.
Delimit Scope forces_scope with fores.
Notation "¬ f" := (negA f%scopeA) (at level 31, right associativity) : scopeE.
Notation "¬ f" := (negE f%scopeE) (at level 31, right associativity) : scopeA.
Notation "f1 ∧ f2" := (conj f1%scopeA f2%scopeA) (at level 41, right associativity) : scopeA.
Notation "f1 ∨ f2" := (disj f1%scopeE f2%scopeE) (at level 51, right associativity) : scopeE.
Notation "〈 la 〉 f" := (ext la f%scopeA) (at level 31, right associativity, format "〈 la 〉 f") : scopeE.
Notation "⦋ la ⦌ f" := (all la f%scopeE) (at level 31, right associativity, format "⦋ la ⦌ f") : scopeA.
Notation "p ⊨ᴱ f" := (forcesE p f%scopeE) (at level 100, no associativity) : forces_scope.
Notation "p ⊨ᴬ f" := (forcesA p f%scopeA) (at level 100, no associativity) : forces_scope.
Open Scope forces_scope.
Fixpoint forces (p:lts_S) (f:phi) : Prop := match f with
| phi1 f ⇒ forcesA p f
| phi2 f ⇒ forcesE p f
end.
Definition image_finite_R {A:Type} (R: A→A→Prop) := ∀ a,
∃ (la' : list A), (∀ a', R a a' ↔ In a' la').
Definition image_finite (lts:labeled_transition_system) :=
(∀ a, image_finite_R (fun p p' ⇒ lstep p a p')) ∧ image_finite_R tstep.
Definition weakly_image_finite (lts:labeled_transition_system) :=
(∀ la, image_finite_R (fun p p' ⇒ step_star p la p')).
Ltac by_contradiction:=
match goal with
| [H: excluded_middle |- ?G] ⇒ destruct (H G); auto; false
end.
Definition hml_implA p q:= ∀ f, forcesA p f → forcesA q f.
Definition hml_implE p q:= ∀ f, forcesE p f → forcesE q f.
Definition hml_equivA p q := hml_implA p q ∧ hml_implA q p.
Definition hml_equivE p q := hml_implE p q ∧ hml_implE q p.
Definition hml_equiv p q := hml_equivA p q ∧ hml_equivE p q.
Lemma pcsim_hmlA: ∀ f p q,
partial_contrasimilar q p → forcesA p f → forcesA q f
with pcsim_hmlE: ∀ f p q,
partial_contrasimilar p q → forcesE p f → forcesE q f.
Proof.
× induction f; try rename p into f; simpl; intros; auto.
- destruct H0; eauto.
- rename p' into q'.
edestruct step_star_pcsim as [p'[??]]; eauto.
× induction f; try rename p into f; simpl; intros; auto.
- destruct H0; eauto.
- destruct H0 as [p'[??]].
edestruct step_star_pcsim as [q'[??]]; eauto.
Qed.
Lemma csim_hmlA: ∀ p q,
contrasimilar p q → hml_equivA p q.
Proof.
split; intros; intro f; intros; eapply pcsim_hmlA; eauto.
apply csim_pcsim2; auto.
apply csim_pcsim1; auto.
Qed.
Lemma csim_hmlE: ∀ p q,
contrasimilar p q → hml_equivE p q.
Proof.
split; intros; intro f; intros; eapply pcsim_hmlE; eauto.
apply csim_pcsim1; auto.
apply csim_pcsim2; auto.
Qed.
Lemma csim_hml: ∀ p q,
contrasimilar p q → hml_equiv p q.
Proof.
split; intros.
apply csim_hmlA; auto.
apply csim_hmlE; auto.
Qed.
Lemma not_not: ∀ P,
excluded_middle → (~~P ↔ P).
Proof. intros; by_contradiction; intuition. Qed.
Lemma not_exists: ∀ A P, excluded_middle → (¬∃ (a:A), P a) → ∀ a, ¬P a.
Proof. intros; by_contradiction. apply H0. ∃ a. apply not_not; auto. Qed.
Lemma not_forall: ∀ A (P:A→Prop),
excluded_middle →
inhabited A →
(¬∀ a, P a) → ∃ a, ¬P a.
Proof.
intros; by_contradiction.
apply H1; intros.
by_contradiction. apply H2; eauto.
Qed.
Lemma not_impl: ∀ (P1 P2: Prop),
excluded_middle →
((~(P1→P2)) ↔ (P1 ∧ ¬P2)).
Proof. intros; by_contradiction; intuition. Qed.
Lemma not_and: ∀ P1 P2,
excluded_middle →
((~(P1∧P2)) ↔ (¬P1 ∨ ¬P2)).
Proof. intros; by_contradiction; intuition. Qed.
Lemma not_or: ∀ P1 P2,
excluded_middle →
((~(P1∨P2)) ↔ (¬P1 ∧ ¬P2)).
Proof. intros; by_contradiction; intuition. Qed.
Lemma not_iff: ∀ P1 P2,
excluded_middle →
((~(P1↔P2)) ↔ ((P1∧¬P2) ∨ (P2∧¬P1))).
Proof. intros; by_contradiction; intuition. Qed.
Lemma hml_implA_neg: ∀ p q,
excluded_middle →
¬hml_implA p q → ∃ f, forcesA p f ∧ ¬forcesA q f.
Proof.
intros.
by_contradiction.
apply H0.
generalize (not_exists _ _ H H1); clear H1; intros H1.
intro f; intros.
specialize (H1 f).
rewrite not_and in H1; auto.
rewrite not_not in H1; auto.
intuition.
Qed.
Lemma hml_implE_neg: ∀ p q,
excluded_middle →
¬hml_implE p q → ∃ f, forcesE p f ∧ ¬forcesE q f.
Proof.
intros.
by_contradiction.
apply H0.
generalize (not_exists _ _ H H1); clear H1; intros H1.
intro f; intros.
specialize (H1 f).
rewrite not_and in H1; auto.
rewrite not_not in H1; auto.
intuition.
Qed.
Lemma exists_list_unsatA: ∀ p lq,
excluded_middle →
(∀ q, In q lq → ¬hml_implA p q) →
∃ lf,
(∀ f, In f lf → ∃ q, In q lq ∧ forcesA p f ∧ ¬forcesA q f) ∧
(∀ q, In q lq → ∃ f, In f lf ∧ forcesA p f ∧ ¬forcesA q f).
Proof.
induction lq; introv Hem; intros.
× ∃ (@nil phiA); split; intros; inverts H0.
× lapply (H a); intros.
edestruct hml_implA_neg as [f[??]]; eauto.
edestruct IHlq as [lf[??]]; eauto.
intros. eapply H; right; auto.
∃ (f::lf); split; intros.
destruct H5; subst.
∃ a; splits; auto. left; auto.
edestruct H3 as [q[?[??]]]; eauto.
∃ q; splits; auto. right; auto.
destruct H5; subst.
∃ f; splits; auto. left; auto.
edestruct H4 as [f'[?[??]]]; eauto.
∃ f'; splits; auto. right; auto.
left; auto.
Qed.
Lemma exists_list_unsatE: ∀ p lq,
excluded_middle →
(∀ q, In q lq → ¬hml_implE q p) →
∃ lf,
(∀ f, In f lf → ∃ q, In q lq ∧ ¬forcesE p f ∧ forcesE q f) ∧
(∀ q, In q lq → ∃ f, In f lf ∧ ¬forcesE p f ∧ forcesE q f).
Proof.
induction lq; introv Hem; intros.
× ∃ (@nil phiE); split; intros; inverts H0.
× lapply (H a); intros.
edestruct hml_implE_neg as [f[??]]; eauto.
edestruct IHlq as [lf[??]]; eauto.
intros. eapply H; right; auto.
∃ (f::lf); split; intros.
destruct H5; subst.
∃ a; splits; auto. left; auto.
edestruct H3 as [q[?[??]]]; eauto.
∃ q; splits; auto. right; auto.
destruct H5; subst.
∃ f; splits; auto. left; auto.
edestruct H4 as [f'[?[??]]]; eauto.
∃ f'; splits; auto. right; auto.
left; auto.
Qed.
Lemma hml_pcsim: ∀ p q,
excluded_middle →
weakly_image_finite lts →
(∀ p, ¬is_halted p) →
(hml_implE p q ∨ hml_implA q p) →
partial_contrasimilar p q.
Proof.
introv Hem Hif Hnh ?.
∃ (fun p q ⇒ hml_implE p q ∨ hml_implA q p).
splits; auto; clear p q H; intros p q [?|?]; intros.
× apply Hnh in H0; false.
× apply Hnh in H0; false.
× by_contradiction.
assert (∀ q', step_star q la q' → ¬hml_implA p' q').
{ intros. apply not_exists with (a:=q') in H1; auto. }
clear H1. rename H2 into H1.
destruct (Hif la q) as [lq' ?].
setoid_rewrite H2 in H1.
edestruct exists_list_unsatA with (lq:=lq') as [lf[??]]; auto.
assert (forcesE p (ext la (list_conjA lf))).
{ simpl. ∃ p'; split; auto.
apply f_list_conjA.
intros.
destruct (H3 f) as [q'[?[??]]]; auto. }
apply H in H5.
destruct H5 as [q'[??]].
edestruct (H4 q') as [f[?[??]]].
apply H2; auto.
rewrite f_list_conjA in H6.
apply H6 in H7.
contradiction.
× by_contradiction.
assert (∀ q', step_star q la q' → ¬hml_implE q' p').
{ intros. apply not_exists with (a:=q') in H1; auto. }
clear H1. rename H2 into H1.
destruct (Hif la q) as [lq' ?].
setoid_rewrite H2 in H1.
edestruct exists_list_unsatE with (lq:=lq') as [lf[??]]; auto.
assert (forcesA q (all la (list_disjE lf))).
{ simpl. intros q' ?.
apply f_list_disjE.
edestruct (H4 q') as [f[?[??]]]; eauto. apply H2; auto. }
apply H in H5.
simpl in H5.
apply H5 in H0.
rewrite f_list_disjE in H0.
destruct H0 as [f[??]].
destruct (H3 f) as [q'[?[??]]]; auto.
Qed.
Lemma hml_csim: ∀ p q,
excluded_middle →
weakly_image_finite lts →
(∀ p, ¬is_halted p) →
(hml_implE p q ∨ hml_implA q p) →
(hml_implE q p ∨ hml_implA p q) →
contrasimilar p q.
Proof.
intros.
apply pcsim_csim;
apply hml_pcsim; auto.
Qed.
Lemma hmlE_csim: ∀ p q,
excluded_middle →
weakly_image_finite lts →
(∀ p, ¬is_halted p) →
hml_equivE p q →
contrasimilar p q.
Proof.
unfold hml_equivE; intros.
apply hml_csim; intuition.
Qed.
Lemma hmlA_csim: ∀ p q,
excluded_middle →
weakly_image_finite lts →
(∀ p, ¬is_halted p) →
hml_equivA p q →
contrasimilar p q.
Proof.
unfold hml_equivA; intros.
apply hml_csim; intuition.
Qed.
Corollary hmlA_hmlE: ∀ p q,
excluded_middle →
weakly_image_finite lts →
(∀ p, ¬is_halted p) →
(hml_equivA p q ↔ hml_equivE p q).
Proof.
split; intros.
apply csim_hmlE.
apply hmlA_csim; auto.
apply csim_hmlA.
apply hmlE_csim; auto.
Qed.
End HML_DecoupledBisimulation.
Require Import LibTactics.
Require Import BisimTheory.
Section HML_DecoupledBisimulation.
Variable lts: labeled_transition_system.
Import Stepping.
Require Import ClassicalFacts.
Inductive phiA : Type :=
| top: phiA
| conj: phiA→phiA→phiA
| all: list lts_L→phiE→phiA
with phiE: Type :=
| bot: phiE
| disj: phiE→phiE→phiE
| ext: list lts_L→phiA→phiE
.
Inductive phi : Type :=
| phi1: phiA→phi
| phi2: phiE→phi.
Fixpoint forcesA (p:lts_S) (f:phiA) : Prop := match f with
| top ⇒ True
| conj f1 f2 ⇒ forcesA p f1 ∧ forcesA p f2
| all la f ⇒ ∀ p', step_star p la p' → forcesE p' f
end
with forcesE (p:lts_S) (f:phiE) : Prop := match f with
| bot ⇒ False
| disj f1 f2 ⇒ forcesE p f1 ∨ forcesE p f2
| ext la f ⇒ ∃ p', step_star p la p' ∧ forcesA p' f
end.
Definition topE:= (ext nil top).
Definition botA:= (all nil bot).
Fixpoint negA f := match f with
| top ⇒ bot
| conj f1 f2 ⇒ disj (negA f1) (negA f2)
| all la f1 ⇒ ext la (negE f1)
end
with negE f := match f with
| bot ⇒ top
| disj f1 f2 ⇒ conj (negE f1) (negE f2)
| ext la f1 ⇒ all la (negA f1)
end.
Lemma topE_correct: ∀ p, forcesE p topE ↔ forcesA p top.
Proof.
simpl; split; intros.
auto.
∃ p; split; auto. apply step_nil.
Qed.
Lemma botA_correct: ∀ p, forcesA p botA ↔ forcesE p bot.
Proof.
simpl; split; intros; auto.
eapply H; apply step_nil.
Qed.
Lemma negA_correct1: ∀ p f, forcesE p (negA f) → ¬forcesA p f
with negE_correct1: ∀ p f, forcesA p (negE f) → ¬forcesE p f.
Proof.
× induction f; simpl; intros.
- intuition.
- intuition.
- intro.
destruct H as [p'[??]].
apply H0 in H.
eapply negE_correct1; eauto.
× induction f; simpl; intros.
intuition.
intuition.
intros [p'[??]].
apply H in H0.
eapply negA_correct1; eauto.
Qed.
Fixpoint list_conjA (lf: list phiA) := match lf with
| nil ⇒ top
| f::lf' ⇒ conj f (list_conjA lf')
end.
Lemma f_list_conjA: ∀ p lf,
forcesA p (list_conjA lf) ↔ (∀ f, In f lf → forcesA p f).
Proof.
induction lf; simpl; intros.
× intuition.
× setoid_rewrite IHlf. intuition. subst; eauto.
Qed.
Fixpoint list_disjE (lf: list phiE) := match lf with
| nil ⇒ bot
| f::lf' ⇒ disj f (list_disjE lf')
end.
Lemma f_list_disjE: ∀ p lf,
forcesE p (list_disjE lf) ↔ (∃ f, In f lf ∧ forcesE p f).
Proof.
induction lf; simpl; intros.
× intuition. destruct H as [?[??]]; auto.
× setoid_rewrite IHlf. clear IHlf. intuition. subst; eauto.
destruct H0 as [?[??]]; eauto.
destruct H as [?[[?|?]?]]; subst; eauto.
Qed.
Delimit Scope scopeA with scopeA.
Delimit Scope scopeE with scopeE.
Delimit Scope forces_scope with fores.
Notation "¬ f" := (negA f%scopeA) (at level 31, right associativity) : scopeE.
Notation "¬ f" := (negE f%scopeE) (at level 31, right associativity) : scopeA.
Notation "f1 ∧ f2" := (conj f1%scopeA f2%scopeA) (at level 41, right associativity) : scopeA.
Notation "f1 ∨ f2" := (disj f1%scopeE f2%scopeE) (at level 51, right associativity) : scopeE.
Notation "〈 la 〉 f" := (ext la f%scopeA) (at level 31, right associativity, format "〈 la 〉 f") : scopeE.
Notation "⦋ la ⦌ f" := (all la f%scopeE) (at level 31, right associativity, format "⦋ la ⦌ f") : scopeA.
Notation "p ⊨ᴱ f" := (forcesE p f%scopeE) (at level 100, no associativity) : forces_scope.
Notation "p ⊨ᴬ f" := (forcesA p f%scopeA) (at level 100, no associativity) : forces_scope.
Open Scope forces_scope.
Fixpoint forces (p:lts_S) (f:phi) : Prop := match f with
| phi1 f ⇒ forcesA p f
| phi2 f ⇒ forcesE p f
end.
Definition image_finite_R {A:Type} (R: A→A→Prop) := ∀ a,
∃ (la' : list A), (∀ a', R a a' ↔ In a' la').
Definition image_finite (lts:labeled_transition_system) :=
(∀ a, image_finite_R (fun p p' ⇒ lstep p a p')) ∧ image_finite_R tstep.
Definition weakly_image_finite (lts:labeled_transition_system) :=
(∀ la, image_finite_R (fun p p' ⇒ step_star p la p')).
Ltac by_contradiction:=
match goal with
| [H: excluded_middle |- ?G] ⇒ destruct (H G); auto; false
end.
Definition hml_implA p q:= ∀ f, forcesA p f → forcesA q f.
Definition hml_implE p q:= ∀ f, forcesE p f → forcesE q f.
Definition hml_equivA p q := hml_implA p q ∧ hml_implA q p.
Definition hml_equivE p q := hml_implE p q ∧ hml_implE q p.
Definition hml_equiv p q := hml_equivA p q ∧ hml_equivE p q.
Lemma pcsim_hmlA: ∀ f p q,
partial_contrasimilar q p → forcesA p f → forcesA q f
with pcsim_hmlE: ∀ f p q,
partial_contrasimilar p q → forcesE p f → forcesE q f.
Proof.
× induction f; try rename p into f; simpl; intros; auto.
- destruct H0; eauto.
- rename p' into q'.
edestruct step_star_pcsim as [p'[??]]; eauto.
× induction f; try rename p into f; simpl; intros; auto.
- destruct H0; eauto.
- destruct H0 as [p'[??]].
edestruct step_star_pcsim as [q'[??]]; eauto.
Qed.
Lemma csim_hmlA: ∀ p q,
contrasimilar p q → hml_equivA p q.
Proof.
split; intros; intro f; intros; eapply pcsim_hmlA; eauto.
apply csim_pcsim2; auto.
apply csim_pcsim1; auto.
Qed.
Lemma csim_hmlE: ∀ p q,
contrasimilar p q → hml_equivE p q.
Proof.
split; intros; intro f; intros; eapply pcsim_hmlE; eauto.
apply csim_pcsim1; auto.
apply csim_pcsim2; auto.
Qed.
Lemma csim_hml: ∀ p q,
contrasimilar p q → hml_equiv p q.
Proof.
split; intros.
apply csim_hmlA; auto.
apply csim_hmlE; auto.
Qed.
Lemma not_not: ∀ P,
excluded_middle → (~~P ↔ P).
Proof. intros; by_contradiction; intuition. Qed.
Lemma not_exists: ∀ A P, excluded_middle → (¬∃ (a:A), P a) → ∀ a, ¬P a.
Proof. intros; by_contradiction. apply H0. ∃ a. apply not_not; auto. Qed.
Lemma not_forall: ∀ A (P:A→Prop),
excluded_middle →
inhabited A →
(¬∀ a, P a) → ∃ a, ¬P a.
Proof.
intros; by_contradiction.
apply H1; intros.
by_contradiction. apply H2; eauto.
Qed.
Lemma not_impl: ∀ (P1 P2: Prop),
excluded_middle →
((~(P1→P2)) ↔ (P1 ∧ ¬P2)).
Proof. intros; by_contradiction; intuition. Qed.
Lemma not_and: ∀ P1 P2,
excluded_middle →
((~(P1∧P2)) ↔ (¬P1 ∨ ¬P2)).
Proof. intros; by_contradiction; intuition. Qed.
Lemma not_or: ∀ P1 P2,
excluded_middle →
((~(P1∨P2)) ↔ (¬P1 ∧ ¬P2)).
Proof. intros; by_contradiction; intuition. Qed.
Lemma not_iff: ∀ P1 P2,
excluded_middle →
((~(P1↔P2)) ↔ ((P1∧¬P2) ∨ (P2∧¬P1))).
Proof. intros; by_contradiction; intuition. Qed.
Lemma hml_implA_neg: ∀ p q,
excluded_middle →
¬hml_implA p q → ∃ f, forcesA p f ∧ ¬forcesA q f.
Proof.
intros.
by_contradiction.
apply H0.
generalize (not_exists _ _ H H1); clear H1; intros H1.
intro f; intros.
specialize (H1 f).
rewrite not_and in H1; auto.
rewrite not_not in H1; auto.
intuition.
Qed.
Lemma hml_implE_neg: ∀ p q,
excluded_middle →
¬hml_implE p q → ∃ f, forcesE p f ∧ ¬forcesE q f.
Proof.
intros.
by_contradiction.
apply H0.
generalize (not_exists _ _ H H1); clear H1; intros H1.
intro f; intros.
specialize (H1 f).
rewrite not_and in H1; auto.
rewrite not_not in H1; auto.
intuition.
Qed.
Lemma exists_list_unsatA: ∀ p lq,
excluded_middle →
(∀ q, In q lq → ¬hml_implA p q) →
∃ lf,
(∀ f, In f lf → ∃ q, In q lq ∧ forcesA p f ∧ ¬forcesA q f) ∧
(∀ q, In q lq → ∃ f, In f lf ∧ forcesA p f ∧ ¬forcesA q f).
Proof.
induction lq; introv Hem; intros.
× ∃ (@nil phiA); split; intros; inverts H0.
× lapply (H a); intros.
edestruct hml_implA_neg as [f[??]]; eauto.
edestruct IHlq as [lf[??]]; eauto.
intros. eapply H; right; auto.
∃ (f::lf); split; intros.
destruct H5; subst.
∃ a; splits; auto. left; auto.
edestruct H3 as [q[?[??]]]; eauto.
∃ q; splits; auto. right; auto.
destruct H5; subst.
∃ f; splits; auto. left; auto.
edestruct H4 as [f'[?[??]]]; eauto.
∃ f'; splits; auto. right; auto.
left; auto.
Qed.
Lemma exists_list_unsatE: ∀ p lq,
excluded_middle →
(∀ q, In q lq → ¬hml_implE q p) →
∃ lf,
(∀ f, In f lf → ∃ q, In q lq ∧ ¬forcesE p f ∧ forcesE q f) ∧
(∀ q, In q lq → ∃ f, In f lf ∧ ¬forcesE p f ∧ forcesE q f).
Proof.
induction lq; introv Hem; intros.
× ∃ (@nil phiE); split; intros; inverts H0.
× lapply (H a); intros.
edestruct hml_implE_neg as [f[??]]; eauto.
edestruct IHlq as [lf[??]]; eauto.
intros. eapply H; right; auto.
∃ (f::lf); split; intros.
destruct H5; subst.
∃ a; splits; auto. left; auto.
edestruct H3 as [q[?[??]]]; eauto.
∃ q; splits; auto. right; auto.
destruct H5; subst.
∃ f; splits; auto. left; auto.
edestruct H4 as [f'[?[??]]]; eauto.
∃ f'; splits; auto. right; auto.
left; auto.
Qed.
Lemma hml_pcsim: ∀ p q,
excluded_middle →
weakly_image_finite lts →
(∀ p, ¬is_halted p) →
(hml_implE p q ∨ hml_implA q p) →
partial_contrasimilar p q.
Proof.
introv Hem Hif Hnh ?.
∃ (fun p q ⇒ hml_implE p q ∨ hml_implA q p).
splits; auto; clear p q H; intros p q [?|?]; intros.
× apply Hnh in H0; false.
× apply Hnh in H0; false.
× by_contradiction.
assert (∀ q', step_star q la q' → ¬hml_implA p' q').
{ intros. apply not_exists with (a:=q') in H1; auto. }
clear H1. rename H2 into H1.
destruct (Hif la q) as [lq' ?].
setoid_rewrite H2 in H1.
edestruct exists_list_unsatA with (lq:=lq') as [lf[??]]; auto.
assert (forcesE p (ext la (list_conjA lf))).
{ simpl. ∃ p'; split; auto.
apply f_list_conjA.
intros.
destruct (H3 f) as [q'[?[??]]]; auto. }
apply H in H5.
destruct H5 as [q'[??]].
edestruct (H4 q') as [f[?[??]]].
apply H2; auto.
rewrite f_list_conjA in H6.
apply H6 in H7.
contradiction.
× by_contradiction.
assert (∀ q', step_star q la q' → ¬hml_implE q' p').
{ intros. apply not_exists with (a:=q') in H1; auto. }
clear H1. rename H2 into H1.
destruct (Hif la q) as [lq' ?].
setoid_rewrite H2 in H1.
edestruct exists_list_unsatE with (lq:=lq') as [lf[??]]; auto.
assert (forcesA q (all la (list_disjE lf))).
{ simpl. intros q' ?.
apply f_list_disjE.
edestruct (H4 q') as [f[?[??]]]; eauto. apply H2; auto. }
apply H in H5.
simpl in H5.
apply H5 in H0.
rewrite f_list_disjE in H0.
destruct H0 as [f[??]].
destruct (H3 f) as [q'[?[??]]]; auto.
Qed.
Lemma hml_csim: ∀ p q,
excluded_middle →
weakly_image_finite lts →
(∀ p, ¬is_halted p) →
(hml_implE p q ∨ hml_implA q p) →
(hml_implE q p ∨ hml_implA p q) →
contrasimilar p q.
Proof.
intros.
apply pcsim_csim;
apply hml_pcsim; auto.
Qed.
Lemma hmlE_csim: ∀ p q,
excluded_middle →
weakly_image_finite lts →
(∀ p, ¬is_halted p) →
hml_equivE p q →
contrasimilar p q.
Proof.
unfold hml_equivE; intros.
apply hml_csim; intuition.
Qed.
Lemma hmlA_csim: ∀ p q,
excluded_middle →
weakly_image_finite lts →
(∀ p, ¬is_halted p) →
hml_equivA p q →
contrasimilar p q.
Proof.
unfold hml_equivA; intros.
apply hml_csim; intuition.
Qed.
Corollary hmlA_hmlE: ∀ p q,
excluded_middle →
weakly_image_finite lts →
(∀ p, ¬is_halted p) →
(hml_equivA p q ↔ hml_equivE p q).
Proof.
split; intros.
apply csim_hmlE.
apply hmlA_csim; auto.
apply csim_hmlA.
apply hmlE_csim; auto.
Qed.
End HML_DecoupledBisimulation.