Library iris.prelude.irelations
This file contains some definitions similar to relations.v, except for relations indexed
by a natural number representing which "thread" took a step.
For such relations, we can define a notion of "fairness" for infinite
reduction sequences.
We then prove a number of results about when, given a fair trace for one relation,
there is a corresponding fair trace for another relation.
From Coq Require Import Wf_nat Omega.
From iris.prelude Require Export tactics base relations list collections.
An element is reducible if a step is possible.
Index i is enabled in x if an i step is possible.
An element is in normal form if no further steps are possible.
Sequence of reductions with corresponding list of indices.
Inductive isteps : list nat → relation A :=
| isteps_nil x : isteps nil x x
| isteps_l i l x y z : R i x y → isteps l y z → isteps (i :: l) x z.
Inductive isteps_good φ : list nat → relation A :=
| isteps_good_nil x : φ x → isteps_good φ nil x x
| isteps_good_l i l x y z : R i x y → φ y → isteps_good φ l y z → isteps_good φ (i :: l) x z.
Inductive istepsS `{Equiv A}: list nat → relation A :=
| istepsS_O x y : x ≡ y → istepsS nil x y
| istepsS_l i l x y z : R i x y → istepsS l y z → istepsS (i :: l) x z.
Inductive isteps_aux: list (nat × A) → relation A :=
| isteps_aux_nil x : isteps_aux nil x x
| isteps_aux_l i l x y z : R i x y → isteps_aux l y z → isteps_aux ((i, y) :: l) x z.
Inductive isteps_aux': list (A × nat) → relation A :=
| isteps_aux'_nil x : isteps_aux' nil x x
| isteps_aux'_l i l x y z : R i x y → isteps_aux' l y z → isteps_aux' ((x, i) :: l) x z.
Lemma isteps_augment: ∀ l a a', isteps l a a' →
∃ l', map snd l' = l ∧
isteps_aux' l' a a'.
Proof.
induction 1.
- ∃ []; split; auto; econstructor; auto.
- edestruct IHisteps as (l'&?&?).
∃ ((x, i) :: l'); split; simpl; f_equal; auto.
econstructor; eauto.
Qed.
Lemma isteps_aux'_erase: ∀ l a a', isteps_aux' l a a' →
isteps (map snd l) a a'.
Proof.
induction 1; simpl; econstructor; eauto.
Qed.
| isteps_nil x : isteps nil x x
| isteps_l i l x y z : R i x y → isteps l y z → isteps (i :: l) x z.
Inductive isteps_good φ : list nat → relation A :=
| isteps_good_nil x : φ x → isteps_good φ nil x x
| isteps_good_l i l x y z : R i x y → φ y → isteps_good φ l y z → isteps_good φ (i :: l) x z.
Inductive istepsS `{Equiv A}: list nat → relation A :=
| istepsS_O x y : x ≡ y → istepsS nil x y
| istepsS_l i l x y z : R i x y → istepsS l y z → istepsS (i :: l) x z.
Inductive isteps_aux: list (nat × A) → relation A :=
| isteps_aux_nil x : isteps_aux nil x x
| isteps_aux_l i l x y z : R i x y → isteps_aux l y z → isteps_aux ((i, y) :: l) x z.
Inductive isteps_aux': list (A × nat) → relation A :=
| isteps_aux'_nil x : isteps_aux' nil x x
| isteps_aux'_l i l x y z : R i x y → isteps_aux' l y z → isteps_aux' ((x, i) :: l) x z.
Lemma isteps_augment: ∀ l a a', isteps l a a' →
∃ l', map snd l' = l ∧
isteps_aux' l' a a'.
Proof.
induction 1.
- ∃ []; split; auto; econstructor; auto.
- edestruct IHisteps as (l'&?&?).
∃ ((x, i) :: l'); split; simpl; f_equal; auto.
econstructor; eauto.
Qed.
Lemma isteps_aux'_erase: ∀ l a a', isteps_aux' l a a' →
isteps (map snd l) a a'.
Proof.
induction 1; simpl; econstructor; eauto.
Qed.
CoInductive all_loop : A → Prop :=
| all_loop_do_step x : red x → (∀ y i, R i x y → all_loop y) → all_loop x.
| all_loop_do_step x : red x → (∀ y i, R i x y → all_loop y) → all_loop x.
CoInductive ex_loop : A → Prop :=
| ex_loop_do_step i x y : R i x y → ex_loop y → ex_loop x.
CoInductive trace : A → Type :=
| trace_step i x y : R i x y → trace y → trace x.
CoInductive eq_ext: ∀ {x}, trace x → trace x → Prop :=
| eq_ext_hd: ∀ i x x' HR HR' (e e': trace x'),
eq_ext e e' →
eq_ext (trace_step i x x' HR e) (trace_step i x x' HR' e').
Inductive suffix: ∀ {x y}, trace x → trace y → Prop :=
| suffix_eq: ∀ x (e e': trace x), eq_ext e e' → suffix e e'
| suffix_tl i x x' HR (e: trace x') y (e': trace y):
suffix e e' →
suffix (trace_step i x x' HR e) e'.
Definition trace_aux {x} (e: trace x) :=
match e with
| trace_step i x y H e ⇒ trace_step i x y H e
end.
Definition hd {x} (e: trace x) :=
match e with
| trace_step i x y _ _ ⇒ x
end.
Lemma trace_aux_id:
∀ {x} (e: trace x), e = trace_aux e.
Proof.
destruct e. auto.
Qed.
CoInductive always (P: ∀ i x y, R i x y → trace y → Prop) : ∀ x, trace x → Prop :=
| al_hd i x y e (HR: R i x y):
P _ _ _ HR e → always P _ e → always P _ (trace_step i x y HR e).
Inductive eventually (P: ∀ i x y, R i x y → trace y → Prop) : ∀ x, trace x → Prop :=
| ev_now i x y e (HR: R i x y): P _ _ _ HR e → eventually P _ (trace_step i x y HR e)
| ev_later i x y e (HR: R i x y):
eventually P y e → eventually P x (trace_step i x y HR e).
| ex_loop_do_step i x y : R i x y → ex_loop y → ex_loop x.
CoInductive trace : A → Type :=
| trace_step i x y : R i x y → trace y → trace x.
CoInductive eq_ext: ∀ {x}, trace x → trace x → Prop :=
| eq_ext_hd: ∀ i x x' HR HR' (e e': trace x'),
eq_ext e e' →
eq_ext (trace_step i x x' HR e) (trace_step i x x' HR' e').
Inductive suffix: ∀ {x y}, trace x → trace y → Prop :=
| suffix_eq: ∀ x (e e': trace x), eq_ext e e' → suffix e e'
| suffix_tl i x x' HR (e: trace x') y (e': trace y):
suffix e e' →
suffix (trace_step i x x' HR e) e'.
Definition trace_aux {x} (e: trace x) :=
match e with
| trace_step i x y H e ⇒ trace_step i x y H e
end.
Definition hd {x} (e: trace x) :=
match e with
| trace_step i x y _ _ ⇒ x
end.
Lemma trace_aux_id:
∀ {x} (e: trace x), e = trace_aux e.
Proof.
destruct e. auto.
Qed.
CoInductive always (P: ∀ i x y, R i x y → trace y → Prop) : ∀ x, trace x → Prop :=
| al_hd i x y e (HR: R i x y):
P _ _ _ HR e → always P _ e → always P _ (trace_step i x y HR e).
Inductive eventually (P: ∀ i x y, R i x y → trace y → Prop) : ∀ x, trace x → Prop :=
| ev_now i x y e (HR: R i x y): P _ _ _ HR e → eventually P _ (trace_step i x y HR e)
| ev_later i x y e (HR: R i x y):
eventually P y e → eventually P x (trace_step i x y HR e).
Index i is always enabled in a trace if it's enabled at the head
and always enabled in the tail
CoInductive al_enabled: ∀ (x : A), trace x → nat → Prop :=
| al_enabled_hd i i' x y e (HR: R i' x y):
enabled x i → al_enabled _ e i → al_enabled _ (trace_step i' x y HR e) i.
Definition al_enabled' x e i := always (λ _ x y _ _, enabled x i) x e.
Definition al_disabled x e i := always (λ _ x y _ _, ¬ enabled x i) x e.
Lemma al_enabled_equiv: ∀ x e i, al_enabled x e i ↔ al_enabled' x e i.
Proof.
unfold al_enabled'.
split.
- revert x e i. cofix.
intros x e i Hae.
destruct Hae. econstructor; eauto.
- revert x e i. cofix.
intros x e i Hae.
destruct Hae. econstructor; eauto.
Qed.
Index i is eventually always enabled in a trace if it's either always enabled
or it's eventually always enabled in the tail
Inductive ea_enabled: ∀ (x : A), trace x → nat → Prop :=
| ea_enabled_now i x e: al_enabled x e i → ea_enabled x e i
| ea_enabled_later i i' x y e (HR: R i' x y):
ea_enabled y e i → ea_enabled x (trace_step i' x y HR e) i.
Definition ea_enabled' x (e: trace x) i :=
eventually (λ _ _ _ HR e', al_enabled' _ (trace_step _ _ _ HR e') i) _ e.
Lemma ea_enabled_equiv: ∀ x e i,
ea_enabled x e i ↔ ea_enabled' x e i.
Proof.
unfold ea_enabled'.
split.
- revert x e i. induction 1.
× destruct e.
eapply ev_now.
eapply al_enabled_equiv; eauto.
× destruct e.
eapply ev_later.
eauto.
- revert x e i. induction 1.
× destruct e.
eapply ea_enabled_now.
eapply al_enabled_equiv; eauto.
× destruct e.
eapply ea_enabled_later.
eauto.
Qed.
Definition ea_disabled x (e: trace x) i :=
eventually (λ _ _ _ HR e', al_disabled _ (trace_step _ _ _ HR e') i) _ e.
Index i takes a step eventually if it takes a step at the head or
or it eventually takes a step in the tail
Inductive ev_taken: ∀ (x : A), trace x → nat → Prop :=
| ev_taken_now i x y e (HR: R i x y): ev_taken x (trace_step i x y HR e) i
| ev_taken_later i i' x y e (HR: R i' x y):
ev_taken y e i → ev_taken x (trace_step i' x y HR e) i.
Definition ev_taken' x (e: trace x) i :=
eventually (λ i' _ _ HR e', i = i') _ e.
Lemma ev_taken_equiv: ∀ x e i,
ev_taken x e i ↔ ev_taken' x e i.
Proof.
unfold ev_taken'.
split.
- revert x e i. induction 1.
× destruct e.
eapply ev_now; auto.
× destruct e.
eapply ev_later; eauto.
- revert x e i. induction 1.
× subst. destruct e.
eapply ev_taken_now.
× destruct e.
eapply ev_taken_later.
eauto.
Qed.
Inductive ev_taken_k: ∀ (x : A), trace x → nat → nat → Prop :=
| ev_taken_now_O i x y e (HR: R i x y): ev_taken_k x (trace_step i x y HR e) i 0
| ev_taken_now_S i x y e (HR: R i x y) k:
ev_taken_k y e i k →
ev_taken_k x (trace_step i x y HR e) i (S k)
| ev_taken_later_k i i' x y e (HR: R i' x y) k:
ev_taken_k y e i k → ev_taken_k x (trace_step i' x y HR e) i k.
CoInductive ae_taken: ∀ (x : A), trace x → nat → Prop :=
| ae_taken_hd i i' x y e (HR: R i' x y):
ev_taken x (trace_step i' x y HR e) i →
ae_taken y e i →
ae_taken x (trace_step i' x y HR e) i.
Definition ae_taken' x e i :=
always (λ _ x y HR e, ev_taken' x (trace_step _ _ _ HR e) i) x e.
Lemma ae_taken_equiv: ∀ x e i,
ae_taken x e i ↔ ae_taken' x e i.
Proof.
unfold ae_taken'.
split.
- revert x e i. cofix.
intros x e i Hae.
destruct Hae. econstructor; eauto.
apply ev_taken_equiv; auto.
- revert x e i. cofix.
intros x e i Hae.
destruct Hae. econstructor; eauto.
apply ev_taken_equiv; auto.
Qed.
CoInductive ae_taken_k: ∀ (x : A), trace x → nat → nat → Prop :=
| ae_taken_k_hd i i' x y e (HR: R i' x y) k:
ev_taken_k x (trace_step i' x y HR e) i k →
ae_taken_k y e i k →
ae_taken_k x (trace_step i' x y HR e) i k.
Fixpoint tr2fun {x: A} (e: trace x) (i: nat) : A × nat :=
match i, e with
| O, trace_step i _ _ _ _ ⇒ (x, i)
| S i', trace_step _ _ _ _ e' ⇒ tr2fun e' i'
end.
Definition tfun (f: nat → A × nat) :=
∀ k, R (snd (f k)) (fst (f k)) (fst (f (S k))).
CoFixpoint fun2tr k (f: nat → A × nat) (HTr: tfun f) : trace (fst (f k)) :=
trace_step (snd (f k)) (fst (f k)) (fst (f (S k))) (HTr k) (fun2tr (S k) f HTr).
Lemma tr2fun_fun2tr:
∀ k f HTr idx, tr2fun (fun2tr k f HTr) idx = f (k + idx).
Proof.
intros.
revert k f HTr.
induction idx; simpl; intros.
- rewrite plus_0_r. destruct (f k); auto.
- rewrite IHidx.
replace (S k + idx) with (k + S idx) by omega; auto.
Qed.
Lemma tr2fun_hd x (e: trace x):
fst (tr2fun e O) = x.
Proof.
destruct e; auto.
Qed.
Lemma tr2fun_succ x (e: trace x) k:
R (snd (tr2fun e k)) (fst (tr2fun e k)) (fst (tr2fun e (S k))).
Proof.
revert x e.
induction k; intros.
- destruct e; simpl; destruct e; eauto.
- destruct e; simpl; eauto.
Qed.
Lemma tr2fun_tfun x (e: trace x): tfun (tr2fun e).
Proof.
unfold tfun; intros k.
revert x e.
induction k; intros.
- destruct e; simpl; destruct e; eauto.
- destruct e; simpl; eauto.
Qed.
Lemma tr2fun_ev x (e: trace x) P:
eventually (λ i x y HR _, P (x, i)) x e ↔ ∃ k, P (tr2fun e k).
Proof.
split.
- induction 1.
× ∃ 0; simpl; eauto.
× edestruct IHeventually as (k&?). ∃ (S k); eauto.
- intros Hf. edestruct Hf as (k & Hk).
clear -Hk. revert x e Hk. induction k; intros.
× destruct e. simpl in *; subst; econstructor; eauto.
× eauto. destruct e. eapply ev_later. eapply IHk. eauto.
Qed.
Lemma tr2fun_al x (e: trace x) P:
always (λ i x _ _ _, P (x, i)) x e
↔ ∀ k, P (tr2fun e k).
Proof.
split.
- intros Hae k. revert x e Hae.
induction k.
× intros. destruct Hae.
simpl; auto.
× intros. destruct Hae.
simpl. eapply IHk. eauto.
- revert x e. cofix.
intros x e Hf. destruct e.
econstructor.
× eapply (Hf 0).
× eapply tr2fun_al; eauto.
intros k. specialize (Hf (S k)); auto.
Qed.
Lemma tr2fun_al_ev x (e: trace x) P:
always (λ i x y HR e, eventually (λ i x _ _ _, P (x, i)) x (trace_step _ _ _ HR e)) x e
↔ ∀ k, ∃ k', k' ≥ k ∧ P (tr2fun e k').
Proof.
split.
- intros Hae k. revert x e Hae.
induction k.
× intros. destruct Hae.
edestruct tr2fun_ev as ((k&Hk)&_); eauto.
∃ k; split; eauto.
destruct k; auto.
omega.
× intros. destruct Hae.
edestruct IHk as (k'&?&?); eauto.
∃ (S k'); split; auto.
omega.
- revert x e. cofix.
intros x e Hf. destruct e. econstructor.
× edestruct (Hf O) as (k'&?&?).
eapply tr2fun_ev. ∃ k'. eauto.
× eapply tr2fun_al_ev.
intros k.
edestruct (Hf (S k)) as (k'&?&?).
destruct k' as [| k']; [omega|].
∃ k'. split; auto; omega.
Qed.
Lemma tr2fun_ev_al x (e: trace x) P:
eventually (λ i x y HR e, always (λ i x _ _ _, P (x, i)) x (trace_step _ _ _ HR e)) x e
↔ ∃ k, ∀ k', k' ≥ k → P (tr2fun e k').
Proof.
split.
- intros Hea.
induction Hea as [? ? ? ? ? Hal|].
× ∃ O. rewrite tr2fun_al in Hal.
eauto.
× edestruct IHHea as (k & Hk).
∃ (S k). intros k' ?. destruct k'; [omega|].
simpl. eapply Hk. omega.
- intros (k & Hk).
revert x e Hk. induction k.
× intros x e Hk. destruct e.
econstructor. rewrite tr2fun_al.
intros k'; eapply Hk; eauto.
omega.
× intros x e Hk. destruct e.
eapply (ev_later). eapply IHk.
intros k' ?.
specialize (Hk (S k')); simpl in Hk; eapply Hk.
omega.
Qed.
Lemma tr2fun_ev_2 x (e: trace x) P:
eventually (λ i x y HR _, P (x, i) y) x e ↔ ∃ k, P (tr2fun e k) (fst (tr2fun e (S k))).
Proof.
split.
- induction 1.
× ∃ 0; simpl; eauto. destruct e. auto.
× edestruct IHeventually as (k&?). ∃ (S k); eauto.
- intros Hf. edestruct Hf as (k & Hk).
clear -Hk. revert x e Hk. induction k; intros.
× destruct e. simpl in *; subst; econstructor; eauto. destruct e; auto.
× eauto. destruct e. eapply ev_later. eapply IHk. eauto.
Qed.
Lemma tr2fun_al_2 x (e: trace x) P:
always (λ i x y _ _, P (x, i) y) x e
↔ ∀ k, P (tr2fun e k) (fst (tr2fun e (S k))).
Proof.
split.
- intros Hae k. revert x e Hae.
induction k.
× intros. destruct Hae.
simpl; destruct e;auto.
× intros. destruct Hae.
simpl. eapply IHk. eauto.
- revert x e. cofix.
intros x e Hf. destruct e.
econstructor.
× simpl in Hf. specialize (Hf 0). simpl in Hf. destruct e; auto.
× eapply tr2fun_al_2; eauto.
intros k. specialize (Hf (S k)); auto.
Qed.
Lemma tr2fun_al_ev_2 x (e: trace x) P:
always (λ i x y HR e, eventually (λ i x y _ _, P (x, i) y) x (trace_step _ _ _ HR e)) x e
↔ ∀ k, ∃ k', k' ≥ k ∧ P (tr2fun e k') (fst (tr2fun e (S k'))).
Proof.
split.
- intros Hae k. revert x e Hae.
induction k.
× intros. destruct Hae.
edestruct tr2fun_ev_2 as ((k&Hk)&_); eauto.
∃ k; split; eauto.
destruct k; auto.
omega.
× intros. destruct Hae.
edestruct IHk as (k'&?&?); eauto.
∃ (S k'); split; auto.
omega.
- revert x e. cofix.
intros x e Hf. destruct e. econstructor.
× edestruct (Hf O) as (k'&?&?).
eapply tr2fun_ev_2. ∃ k'. eauto.
× eapply tr2fun_al_ev_2.
intros k.
edestruct (Hf (S k)) as (k'&?&?).
destruct k' as [| k']; [omega|].
∃ k'. split; auto; omega.
Qed.
Lemma tr2fun_ev_al_2 x (e: trace x) P:
eventually (λ i x y HR e, always (λ i x y _ _, P (x, i) y) x (trace_step _ _ _ HR e)) x e
↔ ∃ k, ∀ k', k' ≥ k → P (tr2fun e k') (fst (tr2fun e (S k'))).
Proof.
split.
- intros Hea.
induction Hea as [? ? ? ? ? Hal|].
× ∃ O. rewrite tr2fun_al_2 in Hal.
eauto.
× edestruct IHHea as (k & Hk).
∃ (S k). intros k' ?. destruct k'; [omega|].
simpl. eapply Hk. omega.
- intros (k & Hk).
revert x e Hk. induction k.
× intros x e Hk. destruct e.
econstructor. rewrite tr2fun_al_2.
intros k'; eapply Hk; eauto.
omega.
× intros x e Hk. destruct e.
eapply (ev_later). eapply IHk.
intros k' ?.
specialize (Hk (S k')); simpl in Hk; eapply Hk.
omega.
Qed.
Lemma tr2fun_ev_taken x (e: trace x) i:
ev_taken x e i ↔ ∃ k, (snd (tr2fun e k)) = i.
Proof.
rewrite ev_taken_equiv.
unfold ev_taken'. rewrite (tr2fun_ev _ _ (λ p, i = snd p)).
split; intros (?&?); eauto.
Qed.
Lemma tr2fun_ae_taken x (e: trace x) i:
ae_taken x e i ↔ ∀ k, ∃ k', k' ≥ k ∧ (snd (tr2fun e k')) = i.
Proof.
rewrite ae_taken_equiv.
unfold ae_taken', ev_taken'.
rewrite (tr2fun_al_ev _ _ (λ p, i = snd p)).
split; intros Hp k; edestruct Hp as (?&?&?); eauto.
Qed.
Fixpoint inc_list (l: list nat) :=
match l with
| [] ⇒ True
| n :: l' ⇒
match l' with
| [] ⇒ True
| n' :: _ ⇒ n < n' ∧ inc_list l'
end
end.
Lemma inc_list_tl:
∀ l a, inc_list (a :: l) → inc_list l.
Proof.
induction l; auto; intros ? (?&?).
destruct l; auto.
Qed.
Lemma inc_list_max_snoc:
∀ l k b, inc_list l → k > fold_left max l b → inc_list (l ++ [k]).
Proof.
induction l; auto.
intros k b Hinc. simpl in ×.
destruct l; simpl in ×.
- split; auto.
eapply le_lt_trans.
eapply Nat.le_max_r.
eauto.
- destruct Hinc as (?&?).
split; auto.
eapply IHl; eauto.
Qed.
Lemma inc_list_map_S:
∀ l, inc_list l → inc_list (map S l).
Proof.
induction l; auto.
simpl. destruct l; auto.
intros (?&?).
simpl. split; [omega|].
eapply IHl; eauto.
Qed.
Lemma inc_list_map_pred:
∀ l a, inc_list (a :: l) → inc_list (map pred l).
Proof.
induction l; auto.
intros a' (?&Hl).
simpl. destruct l; auto.
simpl. split.
× destruct a; [omega|].
destruct Hl as (?&?).
destruct n; [omega|].
simpl. omega.
× eapply IHl; eauto.
Qed.
Lemma inc_list_map_pred':
∀ l a, inc_list (S a :: l) → inc_list (a :: map pred l).
Proof.
induction l; auto.
intros a' (?&Hl).
simpl. split.
× omega.
× eapply IHl. destruct a; auto. omega.
Qed.
Lemma ev_taken_O (x: A) (e: trace x) i:
ev_taken x e i ↔ ev_taken_k x e i O.
Proof.
split; by induction 1; econstructor.
Qed.
Lemma tr2fun_ev_taken_k x (e: trace x) i k:
ev_taken_k x e i k ↔ ∃ l, inc_list l ∧ length l = (S k) ∧ Forall (λ n, snd (tr2fun e n) = i) l.
Proof.
split.
- induction 1.
× ∃ [0]; simpl; eauto.
× edestruct IHev_taken_k as (l&?&?&?).
∃ (0 :: map S l). intros.
split_and!.
** simpl. specialize (inc_list_map_S l); intros HS.
destruct l; simpl; auto.
split; [omega|].
simpl in ×. eapply HS. eauto.
** simpl. rewrite map_length. auto.
** econstructor; eauto.
eapply Forall_fmap.
unfold compose; auto.
× edestruct IHev_taken_k as (l&?&?&?).
∃ (map S l). intros.
split_and!.
** simpl. eapply inc_list_map_S; auto.
** simpl. rewrite map_length. auto.
** eapply Forall_fmap.
unfold compose; auto.
- intros (l&Hl). revert x e i l Hl.
induction k as [|k].
× destruct l; [ simpl in *; intros; omega|].
intros (?&?&Hl).
apply Forall_cons in Hl as (Hhd&Htl).
apply ev_taken_O. apply tr2fun_ev_taken.
eauto.
× intros x e i l (Hinc&Hlen&Hl).
destruct l; [ simpl in *; intros; omega|].
revert x e i l Hinc Hlen Hl.
induction n; intros x e i l Hinc Hlen (Hhd&Htl)%Forall_cons.
** destruct e. simpl in Hhd; subst. econstructor.
eapply (IHk _ _ _ (map pred l)).
split_and!.
*** eapply inc_list_map_pred; eauto.
*** rewrite map_length. auto.
*** rewrite Forall_fmap.
unfold compose; auto.
clear -Hinc Htl. induction l.
**** econstructor.
**** destruct a; [simpl in *; omega|].
simpl in ×.
eapply Forall_cons in Htl as (?&?).
eapply Forall_cons; split; eauto.
destruct Hinc as (?&Hinc').
eapply IHl; eauto.
destruct l; eauto.
destruct Hinc' as (?&?).
split; auto. omega.
** destruct e.
econstructor. simpl in Hhd.
eapply (IHn _ _ _ (map pred l)).
*** eapply inc_list_map_pred' in Hinc; auto.
*** simpl. rewrite map_length. simpl in ×. auto.
*** eapply Forall_cons; split; auto. rewrite Forall_fmap.
clear -Hinc Htl. induction l.
**** econstructor.
**** destruct a; [simpl in *; omega|].
simpl in ×.
eapply Forall_cons in Htl as (?&?).
eapply Forall_cons; split; eauto.
destruct Hinc as (?&Hinc').
eapply IHl; eauto.
destruct l; eauto.
destruct Hinc' as (?&?).
split; auto. omega.
Qed.
Lemma ae_taken_tr2fun_k x (e: trace x) i k:
ae_taken x e i → ∃ l, inc_list l ∧ length l = k ∧ Forall (λ n, snd (tr2fun e n) = i) l.
Proof.
intros Hae.
induction k.
- ∃ nil. split_and!; simpl; eauto.
- edestruct IHk as (l&?&?&?).
edestruct (tr2fun_ae_taken) as (Hbase&_).
edestruct (Hbase Hae (S (fold_left max l 0))) as (k'&?&?).
∃ (l ++ [k']). split_and!.
× eapply inc_list_max_snoc; eauto.
× rewrite app_length. simpl; omega.
× eapply Forall_app; eauto.
Qed.
Lemma ae_taken_ev_taken_k (x: A) (e: trace x) i k:
ae_taken x e i → ev_taken_k x e i k.
Proof.
intros Hae.
by apply tr2fun_ev_taken_k, ae_taken_tr2fun_k.
Qed.
Definition weak_fair (x: A) (e: trace x) : Prop :=
∀ i, ea_enabled x e i → ae_taken x e i.
Lemma eq_ext_tr2fun (x: A) (e e': trace x):
eq_ext e e' ↔ ∀ i, tr2fun e i = tr2fun e' i.
Proof.
split.
- intros Heq i. revert x e e' Heq.
induction i.
× intros; destruct Heq; auto.
× intros. destruct Heq; eauto.
- revert x e e'. cofix.
intros x e e' Hf.
destruct e as [i x y r e].
destruct e' as [i' x y' r' e'].
specialize (tr2fun_succ _ (trace_step i x y r e) O). intros.
specialize (tr2fun_succ _ (trace_step i' x y' r' e') O). intros.
generalize (Hf O); intros HfO; simpl in HfO; inversion HfO; subst.
generalize (Hf 1); intros Hf1; simpl in Hf1.
destruct e, e'. simpl in ×.
inversion Hf1. subst. econstructor.
eapply eq_ext_tr2fun. eauto.
intros. specialize (Hf (S i)); eauto.
Qed.
Lemma suffix_tr2fun (x y: A) (e: trace x) (e': trace y):
suffix e e' ↔ ∃ k, ∀ i, tr2fun e' i = tr2fun e (k + i).
Proof.
split.
- induction 1.
× ∃ O. symmetry. eapply eq_ext_tr2fun; auto.
× edestruct IHsuffix as (k & ?).
∃ (S k). intros i'. simpl; eauto.
- intros (k&Hf). revert x y e e' Hf. induction k.
× intros. simpl in Hf.
assert (x = y).
{
specialize (tr2fun_hd x e). specialize (tr2fun_hd y e').
specialize (Hf O). rewrite Hf. congruence.
}
subst.
eapply suffix_eq.
eapply eq_ext_tr2fun; auto.
× intros. destruct e. econstructor.
eapply IHk. intros i'. eapply Hf.
Qed.
Lemma suffix_always (x y: A) (e: trace x) (e': trace y) P:
suffix e e' → always (λ i x _ _ _, P (x, i)) _ e → always (λ i x _ _ _ , P (x, i)) _ e'.
Proof.
rewrite suffix_tr2fun.
rewrite ?tr2fun_al.
intros (k & Hshift) Hal i.
rewrite Hshift. eauto.
Qed.
Lemma suffix_eventually (x y: A) (e: trace x) (e': trace y) P:
suffix e e' → eventually (λ i x _ _ _, P (x, i)) _ e' → eventually (λ i x _ _ _ , P (x, i)) _ e.
Proof.
rewrite suffix_tr2fun.
rewrite ?tr2fun_ev.
intros (k & Hshift) (k' & Hev).
∃ (k + k').
rewrite <-Hshift. eauto.
Qed.
Lemma suffix_al_ev P (x y: A) (e: trace x) (e': trace y) (HS: suffix e e'):
always (λ i x y HR e, eventually (λ i x _ _ _, P (x, i)) x (trace_step _ _ _ HR e)) x e ↔
always (λ i x y HR e, eventually (λ i x _ _ _, P (x, i)) x (trace_step _ _ _ HR e)) y e'.
Proof.
rewrite suffix_tr2fun in HS.
rewrite ?tr2fun_al_ev.
destruct HS as (kshift & Hshift).
split; intros Hae.
- intros k.
specialize (Hae (kshift + k)).
destruct Hae as (k' & ? & ?).
assert (∃ k'0, kshift + k'0 = k') as (k'0 & Heq).
{ ∃ (k' - kshift). omega. }
∃ k'0; split.
× omega.
× rewrite Hshift. rewrite Heq. auto.
- intros k.
specialize (Hae k).
destruct Hae as (k' & ? & ?).
∃ (kshift + k'); split.
× omega.
× rewrite <-Hshift. auto.
Qed.
Lemma suffix_ev_al P (x y: A) (e: trace x) (e': trace y) (HS: suffix e e'):
eventually (λ i x y HR e, always (λ i x _ _ _, P (x, i)) x (trace_step _ _ _ HR e)) x e ↔
eventually (λ i x y HR e, always (λ i x _ _ _, P (x, i)) x (trace_step _ _ _ HR e)) y e'.
Proof.
rewrite suffix_tr2fun in HS.
rewrite ?tr2fun_ev_al.
destruct HS as (kshift & Hshift).
split; intros (ke & Hev).
- ∃ (kshift + ke). intros k' ?.
rewrite Hshift. eapply Hev. omega.
- ∃ (kshift + ke). intros k' ?.
replace k' with (kshift + (k' - kshift)) by omega.
rewrite <-Hshift.
eapply Hev. omega.
Qed.
Lemma suffix_weak_fair:
∀ x y (e: trace x) (e': trace y),
suffix e e' →
weak_fair x e ↔ weak_fair y e'.
Proof.
unfold weak_fair. intros HS.
split; intros Hwf i;
specialize (Hwf i);
rewrite ea_enabled_equiv in *;
rewrite ae_taken_equiv in *;
unfold ea_enabled', al_enabled' in *;
unfold ae_taken', ev_taken' in ×.
- rewrite <-(suffix_ev_al (λ p, enabled (fst p) i)); eauto.
rewrite <-(suffix_al_ev (λ p, i = snd p)); eauto.
- rewrite (suffix_ev_al (λ p, enabled (fst p) i)); eauto.
rewrite (suffix_al_ev (λ p, i = snd p)); eauto.
Qed.
End definitions.
Arguments suffix {_ _ _ _} _ _.
Arguments weak_fair {_ _ _} _.
Arguments trace_step {_ _} _ _ _ _ _.
Arguments tr2fun {_ _ _} _ _.
Arguments al_enabled {_ _ _} _ _.
Arguments al_disabled {_ _ _} _ _.
Arguments ea_enabled {_ _ _} _ _.
Arguments ea_disabled {_ _ _} _ _.
Arguments ev_taken {_ _ _} _ _.
Arguments ev_taken_k {_ _ _} _ _ _.
Arguments ae_taken {_ _ _} _ _.
Arguments ae_taken_k {_ _ _} _ _ _.
Section weak.
Context `{R : nat → relation A}.
Hint Constructors nsteps isteps isteps_aux isteps_aux'.
Definition R' : relation A := λ x y, ∃ i, R i x y.
Lemma nsteps_isteps:
∀ n x y, nsteps R' n x y → ∃ l, isteps R l x y ∧ length l = n.
Proof.
induction 1 as [| n' x y z (i&HR) Hn' (l&?&?)]; simpl; eauto.
∃ (i :: l); split; simpl; eauto.
Qed.
Lemma isteps_nsteps:
∀ l x y, isteps R l x y → nsteps R' (length l) x y.
Proof.
induction 1 as [| i l' x y z HR Hl' IH]; simpl; eauto.
econstructor; [∃ i; eauto|]; auto.
Qed.
Lemma isteps_once i x y: R i x y ↔ isteps R [i] x y.
Proof.
split; eauto.
intros H. inversion H as [|? ? ? ? ? ? Hnil].
inversion Hnil; subst. auto.
Qed.
Lemma isteps_app x y z l1 l2: isteps R l1 x y → isteps R l2 y z → isteps R (l1 ++ l2) x z.
Proof. induction 1; simpl; eauto. Qed.
Lemma isteps_aux_app x y z l1 l2:
isteps_aux R l1 x y → isteps_aux R l2 y z → isteps_aux R (l1 ++ l2) x z.
Proof. induction 1; simpl; eauto. Qed.
Lemma isteps_aux'_app x y z l1 l2:
isteps_aux' R l1 x y → isteps_aux' R l2 y z → isteps_aux' R (l1 ++ l2) x z.
Proof. induction 1; simpl; eauto. Qed.
Lemma isteps_r l i x y z : isteps R l x y → R i y z → isteps R (l ++ [i]) x z.
Proof. induction 1; simpl; eauto. Qed.
Lemma isteps_aux_r l i x y z : isteps_aux R l x y → R i y z → isteps_aux R (l ++ [(i, z)]) x z.
Proof. induction 1; simpl; eauto. Qed.
Lemma isteps_aux'_cons l l' b i b' i' x y:
isteps_aux' R (l ++ (b, i) :: (b', i') :: l') x y →
R i b b'.
Proof.
revert l' b i b' i' x y.
induction l; intros l' b i b' i' x y.
- rewrite app_nil_l. inversion 1 as [|? ? x' y' ? HS Histeps].
subst. inversion Histeps. subst. eauto.
- inversion 1. subst. eauto.
Qed.
End weak.
Section cofair.
Context `(R1: nat → relation A).
Context `(R2: nat → relation B).
Context (A_dec_eq: ∀ (x y: A), {x = y} + {x ≠ y}).
Context (B_dec_eq: ∀ (x y: B), {x = y} + {x ≠ y}).
Ltac existT_eq_elim :=
repeat (match goal with
[ H: existT ?x ?e1 = existT ?x ?e2 |- _ ] ⇒
apply Eqdep_dec.inj_pair2_eq_dec in H; eauto
end).
Lemma ae_taken_k_ev_taken_k (x: A) (e: trace R1 x) i k:
ae_taken_k e i k → ev_taken_k e i k.
Proof.
destruct 1; auto.
Qed.
Definition fair_pres {x y} (e: trace R1 x) (e': trace R2 y) : Prop :=
weak_fair e → weak_fair e'.
CoInductive enabled_reflecting: ∀ {x y}, trace R1 x → trace R2 y → Prop :=
| enabled_reflecting_hd x1 i1 x1' HR1 e1 x2 i2 x2' HR2 e2:
(∀ i, enabled R2 x2 i → enabled R1 x1 i) →
enabled_reflecting e1 e2 →
enabled_reflecting (trace_step i1 x1 x1' HR1 e1) (trace_step i2 x2 x2' HR2 e2).
Lemma enabled_reflecting_al_enabled:
∀ {x y} (e: trace R1 x) (e': trace R2 y) i,
enabled_reflecting e e' → al_enabled e' i → al_enabled e i.
Proof.
cofix. intros x y e e' i Hco Hale.
destruct Hco.
inversion Hale; subst.
econstructor.
× naive_solver.
× eapply enabled_reflecting_al_enabled; eauto.
existT_eq_elim; subst; auto.
Qed.
Lemma enabled_reflecting_ea_enabled:
∀ {x y} (e: trace R1 x) (e': trace R2 y) i,
enabled_reflecting e e' → ea_enabled e' i → ea_enabled e i.
Proof.
intros x y e e' i Hcoe Hea.
revert x e Hcoe.
induction Hea.
× econstructor. eapply enabled_reflecting_al_enabled; eauto.
× intros. inversion Hcoe.
existT_eq_elim; subst.
eapply ea_enabled_later; eauto.
Qed.
CoInductive co_step: ∀ {x y}, trace R1 x → trace R2 y → Prop :=
| co_step_hd i x1 x1' HR1 e1 x2 x2' HR2 e2:
co_step e1 e2 →
co_step (trace_step i x1 x1' HR1 e1) (trace_step i x2 x2' HR2 e2).
Lemma co_step_ev_taken:
∀ {x y} (e: trace R1 x) (e': trace R2 y) i,
co_step e e' → ev_taken e i → ev_taken e' i.
Proof.
intros x y e e' i Hcoe Hea.
revert y e' Hcoe.
induction Hea as [| ? ? ? ? ? ? ? IHHea].
× intros. inversion Hcoe. repeat (existT_eq_elim; subst).
econstructor.
× intros. inversion Hcoe.
existT_eq_elim; subst.
eapply ev_taken_later; eauto.
Qed.
Lemma co_step_ae_taken:
∀ {x y} (e: trace R1 x) (e': trace R2 y) i,
co_step e e' → ae_taken e i → ae_taken e' i.
Proof.
cofix. intros x y e e' i Hco Hae.
destruct Hco.
inversion Hae; repeat (existT_eq_elim; subst).
econstructor.
× eapply co_step_ev_taken; eauto.
econstructor; eauto.
× eapply co_step_ae_taken; eauto.
Qed.
Lemma co_se_fair_pres:
∀ {x y} (e: trace R1 x) (e': trace R2 y),
enabled_reflecting e e' → co_step e e' → fair_pres e e'.
Proof.
intros ? ? e e' Hcoe Hcos.
unfold fair_pres, weak_fair; intro Hwf.
intros i Hea. specialize (Hwf i).
eapply co_step_ae_taken; eauto.
eapply Hwf.
eapply enabled_reflecting_ea_enabled; eauto.
Qed.
CoInductive co_se: ∀ {x1 x2}, trace R1 x1 → trace R2 x2 → Type :=
| co_se_hd i x1 x1' HR1 e1 x2 x2' HR2 e2:
co_se e1 e2 →
(∀ i, enabled R2 x2 i → enabled R1 x1 i) →
co_se (trace_step i x1 x1' HR1 e1) (trace_step i x2 x2' HR2 e2).
CoInductive co_se_trace: ∀ {x}, trace R1 x → B → Type :=
| co_se_trace_hd i x1 x1' HR1 e1 x2 x2':
(∀ i, enabled R2 x2 i → enabled R1 x1 i) →
R2 i x2 x2' →
co_se_trace e1 x2' →
co_se_trace (trace_step i x1 x1' HR1 e1) x2.
Lemma co_se_elim {x1: A} {x2: B} (e1: trace R1 x1) (e2: trace R2 x2):
co_se e1 e2 → co_step e1 e2 ∧ enabled_reflecting e1 e2.
Proof.
intros Hcose.
split; revert x1 x2 e1 e2 Hcose; cofix.
- intros. destruct Hcose. econstructor; eauto.
- intros. destruct Hcose. econstructor; eauto.
Qed.
CoFixpoint co_se_trace_extract {x1: A} {e: trace R1 x1} {x2: B} (ST: co_se_trace e x2) : trace R2 x2.
destruct ST. econstructor; eauto.
Defined.
Lemma co_se_trace_valid {x1} {e: trace R1 x1} {x2} (ST: co_se_trace e x2):
co_se e (co_se_trace_extract ST).
Proof.
revert x1 e x2 ST; cofix; intros.
destruct ST; subst.
unfold co_se_trace_extract.
rewrite trace_aux_id; simpl.
econstructor; eauto.
Qed.
Lemma co_se_trace_fair_pres:
∀ x1 (e: trace R1 x1) x2,
co_se_trace e x2 →
∃ (e': trace R2 x2), fair_pres e e'.
Proof.
intros x1 e x2 ST.
generalize (co_se_elim e _ (co_se_trace_valid ST)).
intros (?&?).
∃ (co_se_trace_extract ST).
eapply co_se_fair_pres; auto.
Qed.
Section erasure.
Require Import ClassicalEpsilon.
Context (erasure: A → B).
Context (enabled_reflecting: ∀ i a, enabled R2 (erasure a) i → enabled R1 a i).
Context (estep_dec: ∀ `(HR: R1 i a b), {R2 i (erasure a) (erasure b)} +
{¬ (R2 i (erasure a) (erasure b)) ∧
erasure a = erasure b}).
Definition estep `(HR: R1 i a b) := R2 i (erasure a) (erasure b).
Inductive ev_estep: ∀ (x : A), trace R1 x → nat → Prop :=
| ev_estep_now i x y e (HR: R1 i x y): estep HR → ev_estep x (trace_step i x y HR e) i
| ev_estep_later i i' x y e (HR: R1 i' x y):
ev_estep y e i → ev_estep x (trace_step i' x y HR e) i.
Definition ev_estep' x (e: trace R1 x) i :=
eventually R1 (λ i' x y _ _, i = i' ∧ R2 i (erasure x) (erasure y)) _ e.
Definition ae_estep x (e: trace R1 x) i :=
always R1 (λ _ x y HR e, ev_estep' x (trace_step _ _ _ HR e) i) x e.
Lemma ev_estep_equiv: ∀ x e i,
ev_estep x e i ↔ ev_estep' x e i.
Proof.
unfold ev_estep'.
split.
- revert x e i. induction 1.
× destruct e.
eapply ev_now; auto.
× destruct e.
eapply ev_later; eauto.
- revert x e i. induction 1 as [ ? ? ? ? ? (?&?) | ?].
× subst. destruct e.
eapply ev_estep_now; eauto.
× destruct e.
eapply ev_estep_later.
eauto.
Qed.
CoInductive ae_ev_estep: ∀ (x : A), trace R1 x → Prop :=
| ae_ev_estep_hd i x y e (HR: R1 i x y):
(∀ i', ae_taken (trace_step i x y HR e) i' → ae_estep x (trace_step i x y HR e) i') →
(∃ i', ev_estep x (trace_step i x y HR e) i') →
ae_ev_estep y e →
ae_ev_estep x (trace_step i x y HR e).
Lemma ae_ev_estep_intro_all:
(∀ x (e: trace R1 x) i', ae_taken e i' → ae_estep x e i') →
(∀ x e, ∃ i', ev_estep x e i') →
(∀ x e, ae_ev_estep x e).
Proof.
cofix. intros. destruct e; econstructor; [| | eauto]; eauto.
Qed.
Lemma ae_ev_estep_destr_clean x e:
ae_ev_estep x e →
∃ i, ev_estep x e i.
Proof.
intros Hae. destruct Hae. auto.
Qed.
Lemma ae_ev_estep_yield_fun_init x (e: trace R1 x):
ae_ev_estep x e →
∃ k', k' ≥ 0 ∧ R2 (snd (tr2fun e k'))
(erasure (fst (tr2fun e k')))
(erasure (fst (tr2fun e (S k'))))
∧ (∀ k'', k'' ≥ 0 ∧ k'' < k' →
(¬ R2 (snd (tr2fun e k''))
(erasure (fst (tr2fun e k'')))
(erasure (fst (tr2fun e (S k''))))))
∧ (∀ k'', k'' ≥ 0 ∧ k'' ≤ k' →
erasure (fst (tr2fun e 0)) = erasure (fst (tr2fun e k''))).
Proof.
intros Hae.
generalize (ae_ev_estep_destr_clean _ _ Hae).
intros (i & Hev).
revert Hae.
induction Hev.
× intros. ∃ O.
split_and!; auto.
** simpl. destruct e; auto.
** intros; omega.
** intros. assert (k'' = 0) by omega. subst. auto.
× intros.
destruct (estep_dec _ _ _ HR) as [? | (?&?)].
** ∃ 0. split_and!; auto.
*** simpl. destruct e; auto.
*** intros. omega.
*** intros. assert (k'' = 0) by omega. subst. auto.
** edestruct IHHev as (k' & ? & Hstep & Hnstep & Heq).
{ inversion Hae. subst. existT_eq_elim. }
∃ (S k'). split_and!; auto.
*** intros.
destruct k''.
**** simpl. destruct e; auto.
**** simpl. destruct e. simpl in *; eapply Hnstep. omega.
*** intros.
destruct k''.
**** simpl. destruct e; auto.
**** simpl. destruct e. rewrite <-Heq; simpl; auto.
omega.
Qed.
Lemma ae_ev_estep_shift x (e: trace R1 x):
ae_ev_estep x e →
∀ k, ∃ x' e', ae_ev_estep x' e' ∧ (∀ i, tr2fun e' i = tr2fun e (k + i)).
Proof.
intros Hae k.
revert x e Hae.
induction k; eauto.
intros.
destruct Hae. edestruct (IHk _ _ Hae) as (y' & e' & ? & ?).
∃ y', e'; split_and!; auto.
Qed.
Lemma ae_ev_estep_yield_fun x (e: trace R1 x):
ae_ev_estep x e →
∀ k, ∃ k', k' ≥ k ∧ R2 (snd (tr2fun e k'))
(erasure (fst (tr2fun e k')))
(erasure (fst (tr2fun e (S k'))))
∧ (∀ k'', k'' ≥ k ∧ k'' < k' →
(¬ R2 (snd (tr2fun e k''))
(erasure (fst (tr2fun e k'')))
(erasure (fst (tr2fun e (S k''))))))
∧ (∀ k'', k'' ≥ k ∧ k'' ≤ k' →
erasure (fst (tr2fun e k)) = erasure (fst (tr2fun e k''))).
Proof.
intros Hae k.
edestruct (ae_ev_estep_shift _ _ Hae k) as (e' & ? & Hae' & Hshifteq).
eapply ae_ev_estep_yield_fun_init in Hae'.
destruct Hae' as (k' & ? & Hs & Hns & Heq).
∃ (k + k').
split_and!; intros; rewrite <-?Hshifteq.
- omega.
- replace (S (k + k')) with (k + S k') by omega. rewrite <-Hshifteq.
auto.
- replace (k'') with (k + (k'' - k)) by omega.
replace (S (k + (k'' - k))) with (k + S (k'' - k)) by omega.
rewrite <-?Hshifteq. eapply Hns. omega.
- replace (k) with (k + 0) by omega.
replace (k'') with (k + (k'' - k)) by omega.
rewrite <-?Hshifteq. eapply Heq. omega.
Qed.
Definition aes_fun {x} (e: trace R1 x) (Hae: ae_ev_estep x e) :=
λ k, proj1_sig (constructive_indefinite_description _ (ae_ev_estep_yield_fun x e Hae k)).
Fixpoint skip_fun' {x} (e: trace R1 x) (Hae: ae_ev_estep x e) k :=
match k with
| O ⇒ aes_fun e Hae 0
| S k' ⇒ aes_fun e Hae (S (skip_fun' e Hae k'))
end.
Definition skip_fun {x} (e: trace R1 x) (Hae: ae_ev_estep x e) k :=
(erasure (fst (tr2fun e (skip_fun' e Hae k))), snd (tr2fun e (skip_fun' e Hae k))).
Lemma skip_fun_tfun: ∀ {x} (e: trace R1 x) Hae, tfun R2 (skip_fun e Hae).
Proof.
unfold tfun. intros.
destruct k.
- unfold skip_fun, skip_fun'.
unfold aes_fun.
destruct (constructive_indefinite_description) as (k1&Hge1&Hestep1&Hnext1&Heq1).
destruct (constructive_indefinite_description) as (k2&Hge2&Hestep2&Hnext2&Heq2).
simpl proj1_sig in ×.
simpl. rewrite <-(Heq2 k2); eauto.
- simpl.
unfold aes_fun.
destruct (constructive_indefinite_description) as (k1&Hge1&Hestep1&Hnext1&Heq1).
destruct (constructive_indefinite_description) as (k2&Hge2&Hestep2&Hnext2&Heq2).
simpl proj1_sig in ×.
simpl. rewrite <-(Heq2 k2); eauto.
Qed.
Lemma skip_fun'_strict_S {x} (e: trace R1 x) Hae:
∀ k, skip_fun' e Hae k < skip_fun' e Hae (S k).
Proof.
intros. simpl.
unfold aes_fun at 1.
destruct (constructive_indefinite_description) as (k1&Hge1&Hestep1&Hnext1&Heq1).
simpl. omega.
Qed.
Lemma skip_fun'_strict_monotone {x} (e: trace R1 x) Hae:
∀ k k', k < k' → skip_fun' e Hae k < skip_fun' e Hae k'.
Proof.
induction 1; eauto using skip_fun'_strict_S.
etransitivity; eauto; eapply skip_fun'_strict_S.
Qed.
Lemma skip_fun'_order_embedding {x} (e: trace R1 x) Hae:
∀ k k', skip_fun' e Hae k ≤ skip_fun' e Hae k' → k ≤ k'.
Proof.
intros; assert (k ≤ k' ∨ k' < k) as [?|Hlt] by omega; auto.
eapply (skip_fun'_strict_monotone e Hae _ _) in Hlt.
omega.
Qed.
Lemma skip_fun'_between {x} (e: trace R1 x) Hae:
∀ k, ∃ k',
skip_fun' e Hae k' ≥ k ∧
match k' with
| 0 ⇒ True
| S k0 ⇒ skip_fun' e Hae k0 < k
end.
Proof.
induction k.
- ∃ O. simpl. split.
× omega.
× auto.
- destruct IHk as (k' & ? & ?).
assert (skip_fun' e Hae k' ≥ S k ∨ skip_fun' e Hae k' = k) as [? | ?] by omega.
× ∃ k'. split; auto.
destruct k'; auto.
× ∃ (S k'). split; auto.
** simpl. unfold aes_fun.
destruct (constructive_indefinite_description) as (k1&Hge1&Hestep1&Hnext1&Heq1).
simpl. omega.
** subst; auto.
Qed.
Lemma skip_fun'_hits_all {x} (e: trace R1 x) Hae:
∀ k, R2 (snd (tr2fun e k))
(erasure (fst (tr2fun e k)))
(erasure (fst (tr2fun e (S k))))
→ ∃ k', skip_fun' e Hae k' = k.
Proof.
intros k Hestep.
edestruct (skip_fun'_between _ Hae k) as (k'&Hk').
destruct Hk' as (Hge&Hlt).
assert (skip_fun' e Hae k' = k ∨ skip_fun' e Hae k' > k) as [?|Hgt] by omega; eauto.
destruct k'; simpl in Hgt; unfold aes_fun in Hgt;
destruct (constructive_indefinite_description) as (k1&Hge1&Hestep1&Hnext1&Heq1);
simpl in Hgt;
exfalso; eapply (Hnext1 k); eauto; omega.
Qed.
Lemma skip_fun'_infl_matching {x} (e: trace R1 x) Hae:
∀ k, ∃ j, skip_fun' e Hae j ≥ k ∧
(∀ k', skip_fun' e Hae j ≥ k' → k' ≥ k →
erasure (fst (tr2fun e (skip_fun' e Hae j))) =
erasure (fst (tr2fun e k'))).
Proof.
induction k.
- ∃ 0. simpl skip_fun'. unfold aes_fun.
destruct (constructive_indefinite_description) as (k1&Hge1&Hestep1&Hnext1&Heq1).
split_and!; auto.
symmetry. simpl. rewrite <-Heq1; [| simpl in *; omega].
eapply Heq1; omega.
- edestruct IHk as (j0&?&Heq).
assert (skip_fun' e Hae j0 ≥ S k ∨ skip_fun' e Hae j0 = k) as [?|?] by omega.
× ∃ j0; split_and!; eauto.
intros. eapply Heq; auto.
omega.
× ∃ (S j0).
simpl; unfold aes_fun.
destruct (constructive_indefinite_description) as (k1&Hge1&Hestep1&Hnext1&Heq1).
simpl.
split_and!.
** omega.
** intros. rewrite <-Heq1; [| simpl in *; omega].
eapply Heq1; omega.
Qed.
Lemma ae_ev_estep_yield_fun_fair x (e: trace R1 x):
ae_ev_estep x e →
∃ (e': trace R2 (erasure x)), fair_pres e e'.
Proof.
intros Hae.
pose (f := fun2tr R2 O (skip_fun e Hae) (skip_fun_tfun _ _)).
assert (Hhd: skip_fun e Hae 0.1 = erasure x).
{ simpl.
unfold aes_fun.
destruct (constructive_indefinite_description) as (k1&Hge1&Hestep1&Hnext1&Heq1).
simpl. rewrite <-Heq1; [|omega]. simpl; destruct e; auto.
}
eauto.
destruct Hhd.
∃ f.
unfold fair_pres, weak_fair.
intros Hfair i Hea_f.
assert (ea_enabled e i) as Hea_e.
{
eapply ea_enabled_equiv.
eapply ea_enabled_equiv in Hea_f.
unfold ea_enabled', al_enabled' in ×.
eapply (tr2fun_ev_al _ _ _ (λ p, enabled R1 (fst p) i)).
eapply (tr2fun_ev_al _ _ _ (λ p, enabled R2 (fst p) i)) in Hea_f.
unfold f in Hea_f. simpl in Hea_f.
setoid_rewrite (tr2fun_fun2tr R2 0 (skip_fun e Hae) (skip_fun_tfun e Hae)) in Hea_f.
setoid_rewrite plus_0_l in Hea_f.
unfold skip_fun in Hea_f. simpl in Hea_f.
destruct Hea_f as (k&Hea_f).
∃ (skip_fun' e Hae k). intros k' Hge.
edestruct (skip_fun'_infl_matching _ Hae k') as (k'' & ? & Heq).
eapply enabled_reflecting.
erewrite <-Heq; eauto.
eapply Hea_f.
cut (k ≤ k''); auto.
eapply (skip_fun'_order_embedding e Hae). omega.
}
generalize (Hfair i Hea_e) as Hae_e; intros.
eapply ae_taken_equiv.
unfold ae_taken', al_enabled' in ×.
rewrite (tr2fun_al_ev _ _ _ (λ p, i = snd p)).
assert (ae_estep x e i) as Hae_estep by (destruct Hae; eauto).
unfold ae_estep, ev_estep' in Hae_estep.
rewrite
(tr2fun_al_ev_2 R1 _ e (λ p y, i = snd p ∧ R2 i (erasure (fst p)) (erasure y))) in Hae_estep.
intros k.
specialize (Hae_estep (skip_fun' e Hae k)).
destruct Hae_estep as (k' & ? & ? & HR2).
subst.
edestruct (skip_fun'_hits_all e Hae) as (kchoice & ?); eauto.
∃ kchoice. unfold f.
rewrite tr2fun_fun2tr. rewrite plus_0_l.
split; [|subst; auto].
cut (k ≤ kchoice); auto.
eapply (skip_fun'_order_embedding e Hae). omega.
Qed.
End erasure.
Section block.
From iris.prelude Require Export set.
Context (flatten: A → B × (nat → set nat)).
Context (flatten_spec_step:
∀ i a a', R1 i a a' →
(∃ l, isteps R2 l ((flatten a).1) ((flatten a').1)
∧ ∀ j, j ∈ (flatten a).2 i →
j ∈ l ∨ ¬ enabled R2 ((flatten a').1) j)).
Context (flatten_spec_cover:
∀ a i, enabled R2 ((flatten a).1) i →
∃ j, i ∈ (flatten a).2 j).
Context (flatten_spec_enabled_reflect:
∀ a i j, enabled R2 ((flatten a).1) i ∧ i ∈ (flatten a).2 j →
enabled R1 a j).
Context (flatten_spec_enabled_some:
∀ a i, enabled R1 a i → ∃ j, j ∈ (flatten a).2 i ∧ enabled R2 ((flatten a).1) j).
Context (flatten_spec_nonstep_mono:
∀ a a' i, R1 i a a' →
(∀ j, j ≠ i → ((flatten a).2) j ⊆ ((flatten a').2) j)).
Lemma isteps_lookup: ∀ l b1 b2 n, isteps R2 l b1 b2 → n < length l →
∃ bi l1 l2, l = l1 ++ (bi.2) :: l2 ∧
isteps R2 l1 b1 (bi.1) ∧
isteps R2 (bi.2 :: l2) (bi.1) b2 ∧
length l1 = n.
Proof.
intros l b1 b2 n Hsteps. revert n. induction Hsteps.
- simpl. intros; omega.
- simpl. intros.
destruct n.
× ∃ (x, i).
∃ [], l. split_and!; rewrite ?app_nil_l; eauto; try econstructor; eauto.
× edestruct (IHHsteps n) as ((b&i')&l1&l2&?&?&?&?).
** omega.
** ∃ (b, i'), (i :: l1), l2; subst.
split_and!; eauto.
econstructor; eauto.
Qed.
Definition glue (a: A) (e: trace R1 a) (n: nat) : list (B × nat).
Proof.
revert a e.
induction n; intros.
- exact [].
- destruct e as [i x y HS e'].
destruct (constructive_indefinite_description _ (flatten_spec_step _ _ _ HS)) as (l&Histeps&?).
destruct (constructive_indefinite_description _ (isteps_augment _ _ _ _ Histeps)) as (l'&?&?).
eapply (l' ++ IHn _ e').
Defined.
Lemma glue_length: ∀ a e n, length (glue a e n) ≥ n.
Proof.
intros a e n. revert a e; induction n; intros; [omega|].
simpl. destruct e as [i x y HS e']. destruct constructive_indefinite_description
as (l & Histeps & Hdisj).
destruct constructive_indefinite_description as (l' &?&?).
rewrite app_length.
destruct l.
- exfalso. edestruct (flatten_spec_enabled_some x i) as (j&?&?).
{ econstructor; eauto. }
destruct (Hdisj j) as [?|Hne]; eauto.
** set_solver.
** eapply Hne. inversion Histeps. subst. eauto.
- simpl in ×. specialize (IHn _ e').
destruct l'; [simpl in *; congruence|].
simpl. omega.
Qed.
Lemma glue_length_S: ∀ a e n, n < length (glue a e (S n)).
Proof.
intros.
eapply (lt_le_trans n (S n)); auto.
apply glue_length.
Qed.
Lemma glue_prefix_S: ∀ a e n, prefix_of (glue a e n) (glue a e (S n)).
Proof.
intros a e n. revert a e; induction n; intros.
- simpl; eexists; eauto.
- destruct e as [i x y HS e'].
specialize (IHn _ e').
simpl in ×. destruct constructive_indefinite_description
as (l & Histeps & Hdisj).
destruct constructive_indefinite_description as (l'&?&?).
eapply prefix_of_app; eauto.
Qed.
Lemma glue_prefix_le: ∀ a e n n', n ≤ n' → prefix_of (glue a e n) (glue a e n').
Proof.
intros a e n n' Hle. revert a e; induction Hle; intros; auto.
etransitivity. eauto. eapply glue_prefix_S.
Qed.
Lemma glue_cons: ∀ i x y HS e n, glue _ (trace_step i x y HS e) (S n) =
glue _ (trace_step i x y HS e) 1 ++
glue _ e n.
Proof.
intros i x y HS e n. revert i x y HS e.
simpl.
destruct e.
destruct constructive_indefinite_description as (l & Histeps & Hdisj).
destruct constructive_indefinite_description as (l' & ? & ?).
rewrite ?app_nil_r. auto.
Qed.
Lemma glue_isteps:
∀ a e n, isteps_aux' R2 (glue a e n) ((flatten a).1) (flatten ((tr2fun e n).1).1).
Proof.
intros a e n. revert a e; induction n; intros.
- simpl. destruct e. simpl. econstructor.
- destruct e as [i x y HS e'].
specialize (IHn _ e').
simpl in ×. destruct constructive_indefinite_description
as (l & Histeps & Hdisj).
destruct constructive_indefinite_description as (l'&?&?).
eapply isteps_aux'_app; eauto.
Qed.
Definition glue_lookup a e (n: nat) : { bi: B × nat | ∃ l1 l2, glue a e (S n) = l1 ++ bi :: l2
∧ length l1 = n }.
Proof.
specialize (nth_error_None (glue a e (S n)) n). intros Herr.
specialize (nth_error_split (glue a e (S n)) n). intros Hsplit.
destruct nth_error as [|p].
- ∃ p.
eapply Hsplit; eauto.
- exfalso. destruct Herr as (Hfalse&?). specialize (Hfalse eq_refl).
specialize (glue_length_S a e n). intros. omega.
Qed.
Definition flatten_trace_fun (a: A) (e: trace R1 a) (n: nat) : B × nat :=
proj1_sig (glue_lookup a e n).
Lemma flatten_trace_tfun: ∀ a (e: trace R1 a), tfun R2 (flatten_trace_fun a e).
Proof.
intros a e n.
unfold flatten_trace_fun.
destruct glue_lookup as ((b&i)&l1&l2&Heq&Hlen).
destruct glue_lookup as ((b'&i')&l1'&l2'&Heq'&Hlen').
simpl.
destruct (glue_prefix_S a e (S n)) as (gext&Hext).
specialize (glue_isteps a e (S (S n))). intros Histeps.
assert (Heq'': l1 ++ [(b, i)] = l1').
{
rewrite Hext in Heq'.
rewrite Heq in Heq'.
replace (l1 ++ (b, i) :: l2) with ((l1 ++ [(b, i)]) ++ l2) in Heq'
by (simpl; rewrite <-app_assoc; auto).
rewrite <-app_assoc in Heq'.
apply app_inj_1 in Heq' as (?&?); auto.
rewrite app_length. simpl; omega.
}
rewrite <-Heq'' in Heq'.
rewrite Heq' in Histeps.
replace (((l1 ++ [(b, i)]) ++ (b', i') :: l2')) with
(l1 ++ (b, i) :: (b', i') :: l2') in Histeps
by (rewrite <-?app_assoc; simpl; auto).
eapply isteps_aux'_cons; eauto.
Qed.
Lemma al_ev_classical P:
¬ (∃ k, ∀ k', k' ≥ k → ¬ P k') → (∀ k, ∃ k', k' ≥ k ∧ P k').
Proof.
intros Hneg k. eapply not_all_not_ex. intros Hf.
eapply Hneg. ∃ k. intros k' Hge.
specialize (Hf k'). apply not_and_or in Hf.
destruct Hf; [omega|].
auto.
Qed.
Lemma flatten_trace_fun_cons_offset:
∀ i x y HS e, ∃ k', k' > 0 ∧ ∀ k,
flatten_trace_fun _ (trace_step i x y HS e) (k + k') =
flatten_trace_fun _ e k.
Proof.
intros. unfold flatten_trace_fun.
simpl.
∃ (length (glue _ (trace_step i x y HS e) 1)).
split.
- specialize (glue_length x (trace_step i x y HS e) 1).
omega.
- intros k.
destruct glue_lookup as ((b'&i')&l1&l2&Heq&Hlen).
destruct glue_lookup as ((b''&i'')&l1'&l2'&Heq'&Hlen').
simpl.
rewrite glue_cons in Heq.
assert (S k ≤ k + length (glue x (trace_step i x y HS e) 1)) as Hle.
{
specialize (glue_length _ (trace_step i x y HS e) 1).
omega.
}
edestruct (glue_prefix_le _ e _ _ Hle) as (lext&Hext).
rewrite Hext in Heq. rewrite Heq' in Heq.
rewrite <-(app_assoc _ _ lext) in Heq.
rewrite (app_assoc _ l1') in Heq.
apply app_inj_1 in Heq as (_&Heq); auto.
× rewrite <-app_comm_cons in Heq. inversion Heq. auto.
× rewrite ?app_length.
omega.
Qed.
Lemma flatten_trace_match:
∀ a e k, ∃ k', k ≤ k' ∧ (flatten ((tr2fun e k).1)).1 = (flatten_trace_fun a e k').1
∧ ∃ l, isteps_aux' R2 l ((flatten ((tr2fun e k).1)).1)
((flatten ((tr2fun e (S k)).1)).1)
∧ (∀ j, j ∈ (flatten ((tr2fun e k).1)).2 ((tr2fun e k).2) →
j ∈ (map snd l) ∨ ¬ enabled R2 ((flatten ((tr2fun e (S k)).1)).1) j)
∧ (∀ idx, idx < length l →
nth_error l idx = Some (flatten_trace_fun a e (k' + idx))).
Proof.
intros a e k. revert a e.
induction k.
- ∃ 0. split; auto.
unfold flatten_trace_fun at 1.
destruct glue_lookup as ((b&i)&l1&l2&Heq&Hlen). simpl. destruct e as [i' x y HS e].
destruct l1; [| simpl in *; omega].
simpl.
assert (flatten x.1 = b) as →.
{
simpl in ×. destruct constructive_indefinite_description as (?&Histep&?).
destruct constructive_indefinite_description as (?&?&Histep').
rewrite ?app_nil_l, ?app_nil_r in Heq.
subst. inversion Histep'; subst. auto.
}
split; auto.
∃ ((b, i) :: l2).
destruct e as [i'' x' y' HS' e]. simpl.
split_and!; auto.
** simpl in ×. destruct constructive_indefinite_description as (?&Histep&?).
destruct constructive_indefinite_description as (?&?&Histep').
rewrite ?app_nil_l, ?app_nil_r in Heq.
subst. inversion Histep'; subst. auto.
** simpl in ×. destruct constructive_indefinite_description as (?&Histep&?).
destruct constructive_indefinite_description as (?&?&Histep').
rewrite ?app_nil_l, ?app_nil_r in Heq.
subst. inversion Histep'; subst. auto.
** intros idx Hlt.
unfold flatten_trace_fun.
destruct glue_lookup as ((b2&i2)&l1'&l2'&Heq'&Hlen'). simpl.
edestruct (glue_prefix_le _ (trace_step i' x x' HS (trace_step i'' x' y' HS' e))
1 (S idx)) as (gext & Hext); [omega|].
rewrite Hext in Heq'.
rewrite Heq in Heq'.
rewrite ?app_nil_l, ?app_nil_r in Heq'.
rewrite <-(nth_error_app1 _ gext); [| simpl; omega].
rewrite Heq'.
rewrite nth_error_app2; [| simpl; omega].
replace (idx - length l1') with 0 by omega.
auto.
- intros.
destruct e as [i x y HS e]. destruct (IHk _ e) as (k' & ? & Hk' & ? & ? & ? & ?).
destruct (flatten_trace_fun_cons_offset _ _ _ HS e) as (k''&?&Hk'').
∃ (k' + k''). split; [omega|].
split.
× simpl. rewrite Hk'. symmetry; f_equal; eauto.
× eexists; split_and!; eauto.
intros. replace (k' + k'' + idx) with ((k' + idx) + k'') by omega.
erewrite Hk''; eauto.
Qed.
Lemma flatten_fair_pres (a: A) (e: trace R1 a):
∃ (e': trace R2 ((flatten a).1)), fair_pres e e'.
Proof.
pose (f := fun2tr R2 O (flatten_trace_fun a e) (flatten_trace_tfun _ _)).
assert (Hhd: flatten_trace_fun a e 0.1 = flatten a.1).
{
unfold flatten_trace_fun. destruct glue_lookup as (?&l1&l2&Heq&?); simpl.
specialize (glue_isteps a e 1); intros Histeps.
destruct l1; [| simpl in *; omega].
rewrite Heq in Histeps. rewrite app_nil_l in Histeps. inversion Histeps.
auto.
}
destruct Hhd.
∃ f.
unfold fair_pres, weak_fair.
intros Hfair i Hea_f.
eapply ae_taken_equiv.
unfold ae_taken', ev_taken'.
rewrite (tr2fun_al_ev _ _ _ (λ p, i = snd p)).
eapply al_ev_classical. intros (k1&Hk1).
eapply ea_enabled_equiv in Hea_f.
unfold ea_enabled', al_enabled' in Hea_f.
eapply (tr2fun_ev_al _ _ _ (λ p, enabled R2 (fst p) i)) in Hea_f.
destruct Hea_f as (k2&Hk2).
destruct (flatten_trace_match a e (k1 + k2)) as (kb&Hlt&Hmatch&l&?&Hinblock&Hoffset).
edestruct (flatten_spec_cover (tr2fun e (k1 + k2).1) i) as (j&Hin).
{ rewrite Hmatch.
specialize (Hk2 kb).
unfold f in Hk2. rewrite tr2fun_fun2tr in Hk2.
simpl in Hk2. eauto.
eapply Hk2. omega.
}
assert (enabled R1 (tr2fun e (k1 + k2).1) j) as Henj.
{
eapply flatten_spec_enabled_reflect.
rewrite Hmatch.
specialize (Hk2 kb).
unfold f in Hk2. rewrite tr2fun_fun2tr in Hk2.
simpl in Hk2. split; [eapply Hk2; omega|].
eauto.
}
assert (∀ ka', (k1 + k2) ≤ ka' → i ∈ ((flatten ((tr2fun e ka').1)).2) j →
(tr2fun e ka').2 ≠ j) as Hin_ns.
{
intros ka' Hle Hin' Heq.
subst.
destruct (flatten_trace_match a e ka') as (kb'&Hlt'&Hmatch'&l'&?&Hinblock'&Hoffset').
specialize (Hinblock' i Hin'). destruct Hinblock' as [Hi_step | Hi_ne].
× assert (In i (map snd l')) as Hi_step'.
{
clear -Hi_step. induction l'.
- simpl in ×. inversion Hi_step.
- inversion Hi_step; subst; auto.
× left; auto.
× right. auto.
}
eapply in_map_iff in Hi_step'.
destruct Hi_step' as ((b&i')&Heqi&Hin'').
simpl in Heqi; subst i'.
eapply In_nth_error in Hin'' as (n&Hnth_some).
assert (flatten_trace_fun a e (kb' + n) = (b, i)) as Heqkbn.
{
specialize (Hoffset' n).
rewrite Hnth_some in Hoffset'.
assert (n < length l') as Hlt''.
{ eapply nth_error_Some. congruence. }
specialize (Hoffset' Hlt''). inversion Hoffset'. auto.
}
eapply (Hk1 (kb' + n)); [omega|].
unfold f. rewrite tr2fun_fun2tr. simpl. rewrite Heqkbn. auto.
× destruct (flatten_trace_match a e (S ka')) as (kb''&Hl''&Hmatch''&_).
eapply Hi_ne. rewrite Hmatch''. unfold f in Hk2.
specialize (Hk2 kb'').
rewrite tr2fun_fun2tr in Hk2. eapply Hk2. omega.
}
assert (∀ ka', (k1 + k2) ≤ ka' → enabled R1 ((tr2fun e ka').1) j ∧
i ∈ ((flatten ((tr2fun e ka').1)).2) j) as Hen_in.
{
induction 1 as [| m Hle (IHen&IHin)].
- split_and!; auto.
- destruct (flatten_trace_match a e (S m)) as (kb'&Hlt'&Hmatch'&l'&?&Hinblock'&Hoffset').
specialize (tr2fun_succ _ _ e m). intros Hsucc_step.
assert (j ≠ (tr2fun e m).2) as IHns'.
{
intros Heq. subst. eapply (Hin_ns m); auto.
}
generalize (flatten_spec_nonstep_mono _ _ _ Hsucc_step j IHns'); intros Hmono.
split_and!.
× eapply flatten_spec_enabled_reflect. split.
** rewrite Hmatch'. specialize (Hk2 kb'). unfold f in Hk2. rewrite tr2fun_fun2tr in Hk2.
simpl in Hk2. eapply Hk2.
omega.
** set_solver.
× set_solver.
}
assert (ea_enabled e j) as Hea.
{
eapply ea_enabled_equiv.
unfold ea_enabled', al_enabled'.
eapply (tr2fun_ev_al _ _ _ (λ p, enabled R1 (fst p) j)).
∃ (k1+k2). intros k' Hgt.
edestruct Hen_in; eauto.
}
specialize (Hfair j Hea).
eapply ae_taken_equiv in Hfair.
unfold ae_taken', ev_taken' in Hfair.
rewrite (tr2fun_al_ev _ _ _ (λ p, j = snd p)) in Hfair.
destruct (Hfair (k1 + k2)) as (kstep&Hgt&Hstep).
eapply (Hin_ns kstep).
- omega.
- eapply Hen_in. omega.
- auto.
Qed.
End block.
End cofair.
Context `{R : nat → relation A}.
Hint Constructors nsteps isteps isteps_aux isteps_aux'.
Definition R' : relation A := λ x y, ∃ i, R i x y.
Lemma nsteps_isteps:
∀ n x y, nsteps R' n x y → ∃ l, isteps R l x y ∧ length l = n.
Proof.
induction 1 as [| n' x y z (i&HR) Hn' (l&?&?)]; simpl; eauto.
∃ (i :: l); split; simpl; eauto.
Qed.
Lemma isteps_nsteps:
∀ l x y, isteps R l x y → nsteps R' (length l) x y.
Proof.
induction 1 as [| i l' x y z HR Hl' IH]; simpl; eauto.
econstructor; [∃ i; eauto|]; auto.
Qed.
Lemma isteps_once i x y: R i x y ↔ isteps R [i] x y.
Proof.
split; eauto.
intros H. inversion H as [|? ? ? ? ? ? Hnil].
inversion Hnil; subst. auto.
Qed.
Lemma isteps_app x y z l1 l2: isteps R l1 x y → isteps R l2 y z → isteps R (l1 ++ l2) x z.
Proof. induction 1; simpl; eauto. Qed.
Lemma isteps_aux_app x y z l1 l2:
isteps_aux R l1 x y → isteps_aux R l2 y z → isteps_aux R (l1 ++ l2) x z.
Proof. induction 1; simpl; eauto. Qed.
Lemma isteps_aux'_app x y z l1 l2:
isteps_aux' R l1 x y → isteps_aux' R l2 y z → isteps_aux' R (l1 ++ l2) x z.
Proof. induction 1; simpl; eauto. Qed.
Lemma isteps_r l i x y z : isteps R l x y → R i y z → isteps R (l ++ [i]) x z.
Proof. induction 1; simpl; eauto. Qed.
Lemma isteps_aux_r l i x y z : isteps_aux R l x y → R i y z → isteps_aux R (l ++ [(i, z)]) x z.
Proof. induction 1; simpl; eauto. Qed.
Lemma isteps_aux'_cons l l' b i b' i' x y:
isteps_aux' R (l ++ (b, i) :: (b', i') :: l') x y →
R i b b'.
Proof.
revert l' b i b' i' x y.
induction l; intros l' b i b' i' x y.
- rewrite app_nil_l. inversion 1 as [|? ? x' y' ? HS Histeps].
subst. inversion Histeps. subst. eauto.
- inversion 1. subst. eauto.
Qed.
End weak.
Section cofair.
Context `(R1: nat → relation A).
Context `(R2: nat → relation B).
Context (A_dec_eq: ∀ (x y: A), {x = y} + {x ≠ y}).
Context (B_dec_eq: ∀ (x y: B), {x = y} + {x ≠ y}).
Ltac existT_eq_elim :=
repeat (match goal with
[ H: existT ?x ?e1 = existT ?x ?e2 |- _ ] ⇒
apply Eqdep_dec.inj_pair2_eq_dec in H; eauto
end).
Lemma ae_taken_k_ev_taken_k (x: A) (e: trace R1 x) i k:
ae_taken_k e i k → ev_taken_k e i k.
Proof.
destruct 1; auto.
Qed.
Definition fair_pres {x y} (e: trace R1 x) (e': trace R2 y) : Prop :=
weak_fair e → weak_fair e'.
CoInductive enabled_reflecting: ∀ {x y}, trace R1 x → trace R2 y → Prop :=
| enabled_reflecting_hd x1 i1 x1' HR1 e1 x2 i2 x2' HR2 e2:
(∀ i, enabled R2 x2 i → enabled R1 x1 i) →
enabled_reflecting e1 e2 →
enabled_reflecting (trace_step i1 x1 x1' HR1 e1) (trace_step i2 x2 x2' HR2 e2).
Lemma enabled_reflecting_al_enabled:
∀ {x y} (e: trace R1 x) (e': trace R2 y) i,
enabled_reflecting e e' → al_enabled e' i → al_enabled e i.
Proof.
cofix. intros x y e e' i Hco Hale.
destruct Hco.
inversion Hale; subst.
econstructor.
× naive_solver.
× eapply enabled_reflecting_al_enabled; eauto.
existT_eq_elim; subst; auto.
Qed.
Lemma enabled_reflecting_ea_enabled:
∀ {x y} (e: trace R1 x) (e': trace R2 y) i,
enabled_reflecting e e' → ea_enabled e' i → ea_enabled e i.
Proof.
intros x y e e' i Hcoe Hea.
revert x e Hcoe.
induction Hea.
× econstructor. eapply enabled_reflecting_al_enabled; eauto.
× intros. inversion Hcoe.
existT_eq_elim; subst.
eapply ea_enabled_later; eauto.
Qed.
CoInductive co_step: ∀ {x y}, trace R1 x → trace R2 y → Prop :=
| co_step_hd i x1 x1' HR1 e1 x2 x2' HR2 e2:
co_step e1 e2 →
co_step (trace_step i x1 x1' HR1 e1) (trace_step i x2 x2' HR2 e2).
Lemma co_step_ev_taken:
∀ {x y} (e: trace R1 x) (e': trace R2 y) i,
co_step e e' → ev_taken e i → ev_taken e' i.
Proof.
intros x y e e' i Hcoe Hea.
revert y e' Hcoe.
induction Hea as [| ? ? ? ? ? ? ? IHHea].
× intros. inversion Hcoe. repeat (existT_eq_elim; subst).
econstructor.
× intros. inversion Hcoe.
existT_eq_elim; subst.
eapply ev_taken_later; eauto.
Qed.
Lemma co_step_ae_taken:
∀ {x y} (e: trace R1 x) (e': trace R2 y) i,
co_step e e' → ae_taken e i → ae_taken e' i.
Proof.
cofix. intros x y e e' i Hco Hae.
destruct Hco.
inversion Hae; repeat (existT_eq_elim; subst).
econstructor.
× eapply co_step_ev_taken; eauto.
econstructor; eauto.
× eapply co_step_ae_taken; eauto.
Qed.
Lemma co_se_fair_pres:
∀ {x y} (e: trace R1 x) (e': trace R2 y),
enabled_reflecting e e' → co_step e e' → fair_pres e e'.
Proof.
intros ? ? e e' Hcoe Hcos.
unfold fair_pres, weak_fair; intro Hwf.
intros i Hea. specialize (Hwf i).
eapply co_step_ae_taken; eauto.
eapply Hwf.
eapply enabled_reflecting_ea_enabled; eauto.
Qed.
CoInductive co_se: ∀ {x1 x2}, trace R1 x1 → trace R2 x2 → Type :=
| co_se_hd i x1 x1' HR1 e1 x2 x2' HR2 e2:
co_se e1 e2 →
(∀ i, enabled R2 x2 i → enabled R1 x1 i) →
co_se (trace_step i x1 x1' HR1 e1) (trace_step i x2 x2' HR2 e2).
CoInductive co_se_trace: ∀ {x}, trace R1 x → B → Type :=
| co_se_trace_hd i x1 x1' HR1 e1 x2 x2':
(∀ i, enabled R2 x2 i → enabled R1 x1 i) →
R2 i x2 x2' →
co_se_trace e1 x2' →
co_se_trace (trace_step i x1 x1' HR1 e1) x2.
Lemma co_se_elim {x1: A} {x2: B} (e1: trace R1 x1) (e2: trace R2 x2):
co_se e1 e2 → co_step e1 e2 ∧ enabled_reflecting e1 e2.
Proof.
intros Hcose.
split; revert x1 x2 e1 e2 Hcose; cofix.
- intros. destruct Hcose. econstructor; eauto.
- intros. destruct Hcose. econstructor; eauto.
Qed.
CoFixpoint co_se_trace_extract {x1: A} {e: trace R1 x1} {x2: B} (ST: co_se_trace e x2) : trace R2 x2.
destruct ST. econstructor; eauto.
Defined.
Lemma co_se_trace_valid {x1} {e: trace R1 x1} {x2} (ST: co_se_trace e x2):
co_se e (co_se_trace_extract ST).
Proof.
revert x1 e x2 ST; cofix; intros.
destruct ST; subst.
unfold co_se_trace_extract.
rewrite trace_aux_id; simpl.
econstructor; eauto.
Qed.
Lemma co_se_trace_fair_pres:
∀ x1 (e: trace R1 x1) x2,
co_se_trace e x2 →
∃ (e': trace R2 x2), fair_pres e e'.
Proof.
intros x1 e x2 ST.
generalize (co_se_elim e _ (co_se_trace_valid ST)).
intros (?&?).
∃ (co_se_trace_extract ST).
eapply co_se_fair_pres; auto.
Qed.
Section erasure.
Require Import ClassicalEpsilon.
Context (erasure: A → B).
Context (enabled_reflecting: ∀ i a, enabled R2 (erasure a) i → enabled R1 a i).
Context (estep_dec: ∀ `(HR: R1 i a b), {R2 i (erasure a) (erasure b)} +
{¬ (R2 i (erasure a) (erasure b)) ∧
erasure a = erasure b}).
Definition estep `(HR: R1 i a b) := R2 i (erasure a) (erasure b).
Inductive ev_estep: ∀ (x : A), trace R1 x → nat → Prop :=
| ev_estep_now i x y e (HR: R1 i x y): estep HR → ev_estep x (trace_step i x y HR e) i
| ev_estep_later i i' x y e (HR: R1 i' x y):
ev_estep y e i → ev_estep x (trace_step i' x y HR e) i.
Definition ev_estep' x (e: trace R1 x) i :=
eventually R1 (λ i' x y _ _, i = i' ∧ R2 i (erasure x) (erasure y)) _ e.
Definition ae_estep x (e: trace R1 x) i :=
always R1 (λ _ x y HR e, ev_estep' x (trace_step _ _ _ HR e) i) x e.
Lemma ev_estep_equiv: ∀ x e i,
ev_estep x e i ↔ ev_estep' x e i.
Proof.
unfold ev_estep'.
split.
- revert x e i. induction 1.
× destruct e.
eapply ev_now; auto.
× destruct e.
eapply ev_later; eauto.
- revert x e i. induction 1 as [ ? ? ? ? ? (?&?) | ?].
× subst. destruct e.
eapply ev_estep_now; eauto.
× destruct e.
eapply ev_estep_later.
eauto.
Qed.
CoInductive ae_ev_estep: ∀ (x : A), trace R1 x → Prop :=
| ae_ev_estep_hd i x y e (HR: R1 i x y):
(∀ i', ae_taken (trace_step i x y HR e) i' → ae_estep x (trace_step i x y HR e) i') →
(∃ i', ev_estep x (trace_step i x y HR e) i') →
ae_ev_estep y e →
ae_ev_estep x (trace_step i x y HR e).
Lemma ae_ev_estep_intro_all:
(∀ x (e: trace R1 x) i', ae_taken e i' → ae_estep x e i') →
(∀ x e, ∃ i', ev_estep x e i') →
(∀ x e, ae_ev_estep x e).
Proof.
cofix. intros. destruct e; econstructor; [| | eauto]; eauto.
Qed.
Lemma ae_ev_estep_destr_clean x e:
ae_ev_estep x e →
∃ i, ev_estep x e i.
Proof.
intros Hae. destruct Hae. auto.
Qed.
Lemma ae_ev_estep_yield_fun_init x (e: trace R1 x):
ae_ev_estep x e →
∃ k', k' ≥ 0 ∧ R2 (snd (tr2fun e k'))
(erasure (fst (tr2fun e k')))
(erasure (fst (tr2fun e (S k'))))
∧ (∀ k'', k'' ≥ 0 ∧ k'' < k' →
(¬ R2 (snd (tr2fun e k''))
(erasure (fst (tr2fun e k'')))
(erasure (fst (tr2fun e (S k''))))))
∧ (∀ k'', k'' ≥ 0 ∧ k'' ≤ k' →
erasure (fst (tr2fun e 0)) = erasure (fst (tr2fun e k''))).
Proof.
intros Hae.
generalize (ae_ev_estep_destr_clean _ _ Hae).
intros (i & Hev).
revert Hae.
induction Hev.
× intros. ∃ O.
split_and!; auto.
** simpl. destruct e; auto.
** intros; omega.
** intros. assert (k'' = 0) by omega. subst. auto.
× intros.
destruct (estep_dec _ _ _ HR) as [? | (?&?)].
** ∃ 0. split_and!; auto.
*** simpl. destruct e; auto.
*** intros. omega.
*** intros. assert (k'' = 0) by omega. subst. auto.
** edestruct IHHev as (k' & ? & Hstep & Hnstep & Heq).
{ inversion Hae. subst. existT_eq_elim. }
∃ (S k'). split_and!; auto.
*** intros.
destruct k''.
**** simpl. destruct e; auto.
**** simpl. destruct e. simpl in *; eapply Hnstep. omega.
*** intros.
destruct k''.
**** simpl. destruct e; auto.
**** simpl. destruct e. rewrite <-Heq; simpl; auto.
omega.
Qed.
Lemma ae_ev_estep_shift x (e: trace R1 x):
ae_ev_estep x e →
∀ k, ∃ x' e', ae_ev_estep x' e' ∧ (∀ i, tr2fun e' i = tr2fun e (k + i)).
Proof.
intros Hae k.
revert x e Hae.
induction k; eauto.
intros.
destruct Hae. edestruct (IHk _ _ Hae) as (y' & e' & ? & ?).
∃ y', e'; split_and!; auto.
Qed.
Lemma ae_ev_estep_yield_fun x (e: trace R1 x):
ae_ev_estep x e →
∀ k, ∃ k', k' ≥ k ∧ R2 (snd (tr2fun e k'))
(erasure (fst (tr2fun e k')))
(erasure (fst (tr2fun e (S k'))))
∧ (∀ k'', k'' ≥ k ∧ k'' < k' →
(¬ R2 (snd (tr2fun e k''))
(erasure (fst (tr2fun e k'')))
(erasure (fst (tr2fun e (S k''))))))
∧ (∀ k'', k'' ≥ k ∧ k'' ≤ k' →
erasure (fst (tr2fun e k)) = erasure (fst (tr2fun e k''))).
Proof.
intros Hae k.
edestruct (ae_ev_estep_shift _ _ Hae k) as (e' & ? & Hae' & Hshifteq).
eapply ae_ev_estep_yield_fun_init in Hae'.
destruct Hae' as (k' & ? & Hs & Hns & Heq).
∃ (k + k').
split_and!; intros; rewrite <-?Hshifteq.
- omega.
- replace (S (k + k')) with (k + S k') by omega. rewrite <-Hshifteq.
auto.
- replace (k'') with (k + (k'' - k)) by omega.
replace (S (k + (k'' - k))) with (k + S (k'' - k)) by omega.
rewrite <-?Hshifteq. eapply Hns. omega.
- replace (k) with (k + 0) by omega.
replace (k'') with (k + (k'' - k)) by omega.
rewrite <-?Hshifteq. eapply Heq. omega.
Qed.
Definition aes_fun {x} (e: trace R1 x) (Hae: ae_ev_estep x e) :=
λ k, proj1_sig (constructive_indefinite_description _ (ae_ev_estep_yield_fun x e Hae k)).
Fixpoint skip_fun' {x} (e: trace R1 x) (Hae: ae_ev_estep x e) k :=
match k with
| O ⇒ aes_fun e Hae 0
| S k' ⇒ aes_fun e Hae (S (skip_fun' e Hae k'))
end.
Definition skip_fun {x} (e: trace R1 x) (Hae: ae_ev_estep x e) k :=
(erasure (fst (tr2fun e (skip_fun' e Hae k))), snd (tr2fun e (skip_fun' e Hae k))).
Lemma skip_fun_tfun: ∀ {x} (e: trace R1 x) Hae, tfun R2 (skip_fun e Hae).
Proof.
unfold tfun. intros.
destruct k.
- unfold skip_fun, skip_fun'.
unfold aes_fun.
destruct (constructive_indefinite_description) as (k1&Hge1&Hestep1&Hnext1&Heq1).
destruct (constructive_indefinite_description) as (k2&Hge2&Hestep2&Hnext2&Heq2).
simpl proj1_sig in ×.
simpl. rewrite <-(Heq2 k2); eauto.
- simpl.
unfold aes_fun.
destruct (constructive_indefinite_description) as (k1&Hge1&Hestep1&Hnext1&Heq1).
destruct (constructive_indefinite_description) as (k2&Hge2&Hestep2&Hnext2&Heq2).
simpl proj1_sig in ×.
simpl. rewrite <-(Heq2 k2); eauto.
Qed.
Lemma skip_fun'_strict_S {x} (e: trace R1 x) Hae:
∀ k, skip_fun' e Hae k < skip_fun' e Hae (S k).
Proof.
intros. simpl.
unfold aes_fun at 1.
destruct (constructive_indefinite_description) as (k1&Hge1&Hestep1&Hnext1&Heq1).
simpl. omega.
Qed.
Lemma skip_fun'_strict_monotone {x} (e: trace R1 x) Hae:
∀ k k', k < k' → skip_fun' e Hae k < skip_fun' e Hae k'.
Proof.
induction 1; eauto using skip_fun'_strict_S.
etransitivity; eauto; eapply skip_fun'_strict_S.
Qed.
Lemma skip_fun'_order_embedding {x} (e: trace R1 x) Hae:
∀ k k', skip_fun' e Hae k ≤ skip_fun' e Hae k' → k ≤ k'.
Proof.
intros; assert (k ≤ k' ∨ k' < k) as [?|Hlt] by omega; auto.
eapply (skip_fun'_strict_monotone e Hae _ _) in Hlt.
omega.
Qed.
Lemma skip_fun'_between {x} (e: trace R1 x) Hae:
∀ k, ∃ k',
skip_fun' e Hae k' ≥ k ∧
match k' with
| 0 ⇒ True
| S k0 ⇒ skip_fun' e Hae k0 < k
end.
Proof.
induction k.
- ∃ O. simpl. split.
× omega.
× auto.
- destruct IHk as (k' & ? & ?).
assert (skip_fun' e Hae k' ≥ S k ∨ skip_fun' e Hae k' = k) as [? | ?] by omega.
× ∃ k'. split; auto.
destruct k'; auto.
× ∃ (S k'). split; auto.
** simpl. unfold aes_fun.
destruct (constructive_indefinite_description) as (k1&Hge1&Hestep1&Hnext1&Heq1).
simpl. omega.
** subst; auto.
Qed.
Lemma skip_fun'_hits_all {x} (e: trace R1 x) Hae:
∀ k, R2 (snd (tr2fun e k))
(erasure (fst (tr2fun e k)))
(erasure (fst (tr2fun e (S k))))
→ ∃ k', skip_fun' e Hae k' = k.
Proof.
intros k Hestep.
edestruct (skip_fun'_between _ Hae k) as (k'&Hk').
destruct Hk' as (Hge&Hlt).
assert (skip_fun' e Hae k' = k ∨ skip_fun' e Hae k' > k) as [?|Hgt] by omega; eauto.
destruct k'; simpl in Hgt; unfold aes_fun in Hgt;
destruct (constructive_indefinite_description) as (k1&Hge1&Hestep1&Hnext1&Heq1);
simpl in Hgt;
exfalso; eapply (Hnext1 k); eauto; omega.
Qed.
Lemma skip_fun'_infl_matching {x} (e: trace R1 x) Hae:
∀ k, ∃ j, skip_fun' e Hae j ≥ k ∧
(∀ k', skip_fun' e Hae j ≥ k' → k' ≥ k →
erasure (fst (tr2fun e (skip_fun' e Hae j))) =
erasure (fst (tr2fun e k'))).
Proof.
induction k.
- ∃ 0. simpl skip_fun'. unfold aes_fun.
destruct (constructive_indefinite_description) as (k1&Hge1&Hestep1&Hnext1&Heq1).
split_and!; auto.
symmetry. simpl. rewrite <-Heq1; [| simpl in *; omega].
eapply Heq1; omega.
- edestruct IHk as (j0&?&Heq).
assert (skip_fun' e Hae j0 ≥ S k ∨ skip_fun' e Hae j0 = k) as [?|?] by omega.
× ∃ j0; split_and!; eauto.
intros. eapply Heq; auto.
omega.
× ∃ (S j0).
simpl; unfold aes_fun.
destruct (constructive_indefinite_description) as (k1&Hge1&Hestep1&Hnext1&Heq1).
simpl.
split_and!.
** omega.
** intros. rewrite <-Heq1; [| simpl in *; omega].
eapply Heq1; omega.
Qed.
Lemma ae_ev_estep_yield_fun_fair x (e: trace R1 x):
ae_ev_estep x e →
∃ (e': trace R2 (erasure x)), fair_pres e e'.
Proof.
intros Hae.
pose (f := fun2tr R2 O (skip_fun e Hae) (skip_fun_tfun _ _)).
assert (Hhd: skip_fun e Hae 0.1 = erasure x).
{ simpl.
unfold aes_fun.
destruct (constructive_indefinite_description) as (k1&Hge1&Hestep1&Hnext1&Heq1).
simpl. rewrite <-Heq1; [|omega]. simpl; destruct e; auto.
}
eauto.
destruct Hhd.
∃ f.
unfold fair_pres, weak_fair.
intros Hfair i Hea_f.
assert (ea_enabled e i) as Hea_e.
{
eapply ea_enabled_equiv.
eapply ea_enabled_equiv in Hea_f.
unfold ea_enabled', al_enabled' in ×.
eapply (tr2fun_ev_al _ _ _ (λ p, enabled R1 (fst p) i)).
eapply (tr2fun_ev_al _ _ _ (λ p, enabled R2 (fst p) i)) in Hea_f.
unfold f in Hea_f. simpl in Hea_f.
setoid_rewrite (tr2fun_fun2tr R2 0 (skip_fun e Hae) (skip_fun_tfun e Hae)) in Hea_f.
setoid_rewrite plus_0_l in Hea_f.
unfold skip_fun in Hea_f. simpl in Hea_f.
destruct Hea_f as (k&Hea_f).
∃ (skip_fun' e Hae k). intros k' Hge.
edestruct (skip_fun'_infl_matching _ Hae k') as (k'' & ? & Heq).
eapply enabled_reflecting.
erewrite <-Heq; eauto.
eapply Hea_f.
cut (k ≤ k''); auto.
eapply (skip_fun'_order_embedding e Hae). omega.
}
generalize (Hfair i Hea_e) as Hae_e; intros.
eapply ae_taken_equiv.
unfold ae_taken', al_enabled' in ×.
rewrite (tr2fun_al_ev _ _ _ (λ p, i = snd p)).
assert (ae_estep x e i) as Hae_estep by (destruct Hae; eauto).
unfold ae_estep, ev_estep' in Hae_estep.
rewrite
(tr2fun_al_ev_2 R1 _ e (λ p y, i = snd p ∧ R2 i (erasure (fst p)) (erasure y))) in Hae_estep.
intros k.
specialize (Hae_estep (skip_fun' e Hae k)).
destruct Hae_estep as (k' & ? & ? & HR2).
subst.
edestruct (skip_fun'_hits_all e Hae) as (kchoice & ?); eauto.
∃ kchoice. unfold f.
rewrite tr2fun_fun2tr. rewrite plus_0_l.
split; [|subst; auto].
cut (k ≤ kchoice); auto.
eapply (skip_fun'_order_embedding e Hae). omega.
Qed.
End erasure.
Section block.
From iris.prelude Require Export set.
Context (flatten: A → B × (nat → set nat)).
Context (flatten_spec_step:
∀ i a a', R1 i a a' →
(∃ l, isteps R2 l ((flatten a).1) ((flatten a').1)
∧ ∀ j, j ∈ (flatten a).2 i →
j ∈ l ∨ ¬ enabled R2 ((flatten a').1) j)).
Context (flatten_spec_cover:
∀ a i, enabled R2 ((flatten a).1) i →
∃ j, i ∈ (flatten a).2 j).
Context (flatten_spec_enabled_reflect:
∀ a i j, enabled R2 ((flatten a).1) i ∧ i ∈ (flatten a).2 j →
enabled R1 a j).
Context (flatten_spec_enabled_some:
∀ a i, enabled R1 a i → ∃ j, j ∈ (flatten a).2 i ∧ enabled R2 ((flatten a).1) j).
Context (flatten_spec_nonstep_mono:
∀ a a' i, R1 i a a' →
(∀ j, j ≠ i → ((flatten a).2) j ⊆ ((flatten a').2) j)).
Lemma isteps_lookup: ∀ l b1 b2 n, isteps R2 l b1 b2 → n < length l →
∃ bi l1 l2, l = l1 ++ (bi.2) :: l2 ∧
isteps R2 l1 b1 (bi.1) ∧
isteps R2 (bi.2 :: l2) (bi.1) b2 ∧
length l1 = n.
Proof.
intros l b1 b2 n Hsteps. revert n. induction Hsteps.
- simpl. intros; omega.
- simpl. intros.
destruct n.
× ∃ (x, i).
∃ [], l. split_and!; rewrite ?app_nil_l; eauto; try econstructor; eauto.
× edestruct (IHHsteps n) as ((b&i')&l1&l2&?&?&?&?).
** omega.
** ∃ (b, i'), (i :: l1), l2; subst.
split_and!; eauto.
econstructor; eauto.
Qed.
Definition glue (a: A) (e: trace R1 a) (n: nat) : list (B × nat).
Proof.
revert a e.
induction n; intros.
- exact [].
- destruct e as [i x y HS e'].
destruct (constructive_indefinite_description _ (flatten_spec_step _ _ _ HS)) as (l&Histeps&?).
destruct (constructive_indefinite_description _ (isteps_augment _ _ _ _ Histeps)) as (l'&?&?).
eapply (l' ++ IHn _ e').
Defined.
Lemma glue_length: ∀ a e n, length (glue a e n) ≥ n.
Proof.
intros a e n. revert a e; induction n; intros; [omega|].
simpl. destruct e as [i x y HS e']. destruct constructive_indefinite_description
as (l & Histeps & Hdisj).
destruct constructive_indefinite_description as (l' &?&?).
rewrite app_length.
destruct l.
- exfalso. edestruct (flatten_spec_enabled_some x i) as (j&?&?).
{ econstructor; eauto. }
destruct (Hdisj j) as [?|Hne]; eauto.
** set_solver.
** eapply Hne. inversion Histeps. subst. eauto.
- simpl in ×. specialize (IHn _ e').
destruct l'; [simpl in *; congruence|].
simpl. omega.
Qed.
Lemma glue_length_S: ∀ a e n, n < length (glue a e (S n)).
Proof.
intros.
eapply (lt_le_trans n (S n)); auto.
apply glue_length.
Qed.
Lemma glue_prefix_S: ∀ a e n, prefix_of (glue a e n) (glue a e (S n)).
Proof.
intros a e n. revert a e; induction n; intros.
- simpl; eexists; eauto.
- destruct e as [i x y HS e'].
specialize (IHn _ e').
simpl in ×. destruct constructive_indefinite_description
as (l & Histeps & Hdisj).
destruct constructive_indefinite_description as (l'&?&?).
eapply prefix_of_app; eauto.
Qed.
Lemma glue_prefix_le: ∀ a e n n', n ≤ n' → prefix_of (glue a e n) (glue a e n').
Proof.
intros a e n n' Hle. revert a e; induction Hle; intros; auto.
etransitivity. eauto. eapply glue_prefix_S.
Qed.
Lemma glue_cons: ∀ i x y HS e n, glue _ (trace_step i x y HS e) (S n) =
glue _ (trace_step i x y HS e) 1 ++
glue _ e n.
Proof.
intros i x y HS e n. revert i x y HS e.
simpl.
destruct e.
destruct constructive_indefinite_description as (l & Histeps & Hdisj).
destruct constructive_indefinite_description as (l' & ? & ?).
rewrite ?app_nil_r. auto.
Qed.
Lemma glue_isteps:
∀ a e n, isteps_aux' R2 (glue a e n) ((flatten a).1) (flatten ((tr2fun e n).1).1).
Proof.
intros a e n. revert a e; induction n; intros.
- simpl. destruct e. simpl. econstructor.
- destruct e as [i x y HS e'].
specialize (IHn _ e').
simpl in ×. destruct constructive_indefinite_description
as (l & Histeps & Hdisj).
destruct constructive_indefinite_description as (l'&?&?).
eapply isteps_aux'_app; eauto.
Qed.
Definition glue_lookup a e (n: nat) : { bi: B × nat | ∃ l1 l2, glue a e (S n) = l1 ++ bi :: l2
∧ length l1 = n }.
Proof.
specialize (nth_error_None (glue a e (S n)) n). intros Herr.
specialize (nth_error_split (glue a e (S n)) n). intros Hsplit.
destruct nth_error as [|p].
- ∃ p.
eapply Hsplit; eauto.
- exfalso. destruct Herr as (Hfalse&?). specialize (Hfalse eq_refl).
specialize (glue_length_S a e n). intros. omega.
Qed.
Definition flatten_trace_fun (a: A) (e: trace R1 a) (n: nat) : B × nat :=
proj1_sig (glue_lookup a e n).
Lemma flatten_trace_tfun: ∀ a (e: trace R1 a), tfun R2 (flatten_trace_fun a e).
Proof.
intros a e n.
unfold flatten_trace_fun.
destruct glue_lookup as ((b&i)&l1&l2&Heq&Hlen).
destruct glue_lookup as ((b'&i')&l1'&l2'&Heq'&Hlen').
simpl.
destruct (glue_prefix_S a e (S n)) as (gext&Hext).
specialize (glue_isteps a e (S (S n))). intros Histeps.
assert (Heq'': l1 ++ [(b, i)] = l1').
{
rewrite Hext in Heq'.
rewrite Heq in Heq'.
replace (l1 ++ (b, i) :: l2) with ((l1 ++ [(b, i)]) ++ l2) in Heq'
by (simpl; rewrite <-app_assoc; auto).
rewrite <-app_assoc in Heq'.
apply app_inj_1 in Heq' as (?&?); auto.
rewrite app_length. simpl; omega.
}
rewrite <-Heq'' in Heq'.
rewrite Heq' in Histeps.
replace (((l1 ++ [(b, i)]) ++ (b', i') :: l2')) with
(l1 ++ (b, i) :: (b', i') :: l2') in Histeps
by (rewrite <-?app_assoc; simpl; auto).
eapply isteps_aux'_cons; eauto.
Qed.
Lemma al_ev_classical P:
¬ (∃ k, ∀ k', k' ≥ k → ¬ P k') → (∀ k, ∃ k', k' ≥ k ∧ P k').
Proof.
intros Hneg k. eapply not_all_not_ex. intros Hf.
eapply Hneg. ∃ k. intros k' Hge.
specialize (Hf k'). apply not_and_or in Hf.
destruct Hf; [omega|].
auto.
Qed.
Lemma flatten_trace_fun_cons_offset:
∀ i x y HS e, ∃ k', k' > 0 ∧ ∀ k,
flatten_trace_fun _ (trace_step i x y HS e) (k + k') =
flatten_trace_fun _ e k.
Proof.
intros. unfold flatten_trace_fun.
simpl.
∃ (length (glue _ (trace_step i x y HS e) 1)).
split.
- specialize (glue_length x (trace_step i x y HS e) 1).
omega.
- intros k.
destruct glue_lookup as ((b'&i')&l1&l2&Heq&Hlen).
destruct glue_lookup as ((b''&i'')&l1'&l2'&Heq'&Hlen').
simpl.
rewrite glue_cons in Heq.
assert (S k ≤ k + length (glue x (trace_step i x y HS e) 1)) as Hle.
{
specialize (glue_length _ (trace_step i x y HS e) 1).
omega.
}
edestruct (glue_prefix_le _ e _ _ Hle) as (lext&Hext).
rewrite Hext in Heq. rewrite Heq' in Heq.
rewrite <-(app_assoc _ _ lext) in Heq.
rewrite (app_assoc _ l1') in Heq.
apply app_inj_1 in Heq as (_&Heq); auto.
× rewrite <-app_comm_cons in Heq. inversion Heq. auto.
× rewrite ?app_length.
omega.
Qed.
Lemma flatten_trace_match:
∀ a e k, ∃ k', k ≤ k' ∧ (flatten ((tr2fun e k).1)).1 = (flatten_trace_fun a e k').1
∧ ∃ l, isteps_aux' R2 l ((flatten ((tr2fun e k).1)).1)
((flatten ((tr2fun e (S k)).1)).1)
∧ (∀ j, j ∈ (flatten ((tr2fun e k).1)).2 ((tr2fun e k).2) →
j ∈ (map snd l) ∨ ¬ enabled R2 ((flatten ((tr2fun e (S k)).1)).1) j)
∧ (∀ idx, idx < length l →
nth_error l idx = Some (flatten_trace_fun a e (k' + idx))).
Proof.
intros a e k. revert a e.
induction k.
- ∃ 0. split; auto.
unfold flatten_trace_fun at 1.
destruct glue_lookup as ((b&i)&l1&l2&Heq&Hlen). simpl. destruct e as [i' x y HS e].
destruct l1; [| simpl in *; omega].
simpl.
assert (flatten x.1 = b) as →.
{
simpl in ×. destruct constructive_indefinite_description as (?&Histep&?).
destruct constructive_indefinite_description as (?&?&Histep').
rewrite ?app_nil_l, ?app_nil_r in Heq.
subst. inversion Histep'; subst. auto.
}
split; auto.
∃ ((b, i) :: l2).
destruct e as [i'' x' y' HS' e]. simpl.
split_and!; auto.
** simpl in ×. destruct constructive_indefinite_description as (?&Histep&?).
destruct constructive_indefinite_description as (?&?&Histep').
rewrite ?app_nil_l, ?app_nil_r in Heq.
subst. inversion Histep'; subst. auto.
** simpl in ×. destruct constructive_indefinite_description as (?&Histep&?).
destruct constructive_indefinite_description as (?&?&Histep').
rewrite ?app_nil_l, ?app_nil_r in Heq.
subst. inversion Histep'; subst. auto.
** intros idx Hlt.
unfold flatten_trace_fun.
destruct glue_lookup as ((b2&i2)&l1'&l2'&Heq'&Hlen'). simpl.
edestruct (glue_prefix_le _ (trace_step i' x x' HS (trace_step i'' x' y' HS' e))
1 (S idx)) as (gext & Hext); [omega|].
rewrite Hext in Heq'.
rewrite Heq in Heq'.
rewrite ?app_nil_l, ?app_nil_r in Heq'.
rewrite <-(nth_error_app1 _ gext); [| simpl; omega].
rewrite Heq'.
rewrite nth_error_app2; [| simpl; omega].
replace (idx - length l1') with 0 by omega.
auto.
- intros.
destruct e as [i x y HS e]. destruct (IHk _ e) as (k' & ? & Hk' & ? & ? & ? & ?).
destruct (flatten_trace_fun_cons_offset _ _ _ HS e) as (k''&?&Hk'').
∃ (k' + k''). split; [omega|].
split.
× simpl. rewrite Hk'. symmetry; f_equal; eauto.
× eexists; split_and!; eauto.
intros. replace (k' + k'' + idx) with ((k' + idx) + k'') by omega.
erewrite Hk''; eauto.
Qed.
Lemma flatten_fair_pres (a: A) (e: trace R1 a):
∃ (e': trace R2 ((flatten a).1)), fair_pres e e'.
Proof.
pose (f := fun2tr R2 O (flatten_trace_fun a e) (flatten_trace_tfun _ _)).
assert (Hhd: flatten_trace_fun a e 0.1 = flatten a.1).
{
unfold flatten_trace_fun. destruct glue_lookup as (?&l1&l2&Heq&?); simpl.
specialize (glue_isteps a e 1); intros Histeps.
destruct l1; [| simpl in *; omega].
rewrite Heq in Histeps. rewrite app_nil_l in Histeps. inversion Histeps.
auto.
}
destruct Hhd.
∃ f.
unfold fair_pres, weak_fair.
intros Hfair i Hea_f.
eapply ae_taken_equiv.
unfold ae_taken', ev_taken'.
rewrite (tr2fun_al_ev _ _ _ (λ p, i = snd p)).
eapply al_ev_classical. intros (k1&Hk1).
eapply ea_enabled_equiv in Hea_f.
unfold ea_enabled', al_enabled' in Hea_f.
eapply (tr2fun_ev_al _ _ _ (λ p, enabled R2 (fst p) i)) in Hea_f.
destruct Hea_f as (k2&Hk2).
destruct (flatten_trace_match a e (k1 + k2)) as (kb&Hlt&Hmatch&l&?&Hinblock&Hoffset).
edestruct (flatten_spec_cover (tr2fun e (k1 + k2).1) i) as (j&Hin).
{ rewrite Hmatch.
specialize (Hk2 kb).
unfold f in Hk2. rewrite tr2fun_fun2tr in Hk2.
simpl in Hk2. eauto.
eapply Hk2. omega.
}
assert (enabled R1 (tr2fun e (k1 + k2).1) j) as Henj.
{
eapply flatten_spec_enabled_reflect.
rewrite Hmatch.
specialize (Hk2 kb).
unfold f in Hk2. rewrite tr2fun_fun2tr in Hk2.
simpl in Hk2. split; [eapply Hk2; omega|].
eauto.
}
assert (∀ ka', (k1 + k2) ≤ ka' → i ∈ ((flatten ((tr2fun e ka').1)).2) j →
(tr2fun e ka').2 ≠ j) as Hin_ns.
{
intros ka' Hle Hin' Heq.
subst.
destruct (flatten_trace_match a e ka') as (kb'&Hlt'&Hmatch'&l'&?&Hinblock'&Hoffset').
specialize (Hinblock' i Hin'). destruct Hinblock' as [Hi_step | Hi_ne].
× assert (In i (map snd l')) as Hi_step'.
{
clear -Hi_step. induction l'.
- simpl in ×. inversion Hi_step.
- inversion Hi_step; subst; auto.
× left; auto.
× right. auto.
}
eapply in_map_iff in Hi_step'.
destruct Hi_step' as ((b&i')&Heqi&Hin'').
simpl in Heqi; subst i'.
eapply In_nth_error in Hin'' as (n&Hnth_some).
assert (flatten_trace_fun a e (kb' + n) = (b, i)) as Heqkbn.
{
specialize (Hoffset' n).
rewrite Hnth_some in Hoffset'.
assert (n < length l') as Hlt''.
{ eapply nth_error_Some. congruence. }
specialize (Hoffset' Hlt''). inversion Hoffset'. auto.
}
eapply (Hk1 (kb' + n)); [omega|].
unfold f. rewrite tr2fun_fun2tr. simpl. rewrite Heqkbn. auto.
× destruct (flatten_trace_match a e (S ka')) as (kb''&Hl''&Hmatch''&_).
eapply Hi_ne. rewrite Hmatch''. unfold f in Hk2.
specialize (Hk2 kb'').
rewrite tr2fun_fun2tr in Hk2. eapply Hk2. omega.
}
assert (∀ ka', (k1 + k2) ≤ ka' → enabled R1 ((tr2fun e ka').1) j ∧
i ∈ ((flatten ((tr2fun e ka').1)).2) j) as Hen_in.
{
induction 1 as [| m Hle (IHen&IHin)].
- split_and!; auto.
- destruct (flatten_trace_match a e (S m)) as (kb'&Hlt'&Hmatch'&l'&?&Hinblock'&Hoffset').
specialize (tr2fun_succ _ _ e m). intros Hsucc_step.
assert (j ≠ (tr2fun e m).2) as IHns'.
{
intros Heq. subst. eapply (Hin_ns m); auto.
}
generalize (flatten_spec_nonstep_mono _ _ _ Hsucc_step j IHns'); intros Hmono.
split_and!.
× eapply flatten_spec_enabled_reflect. split.
** rewrite Hmatch'. specialize (Hk2 kb'). unfold f in Hk2. rewrite tr2fun_fun2tr in Hk2.
simpl in Hk2. eapply Hk2.
omega.
** set_solver.
× set_solver.
}
assert (ea_enabled e j) as Hea.
{
eapply ea_enabled_equiv.
unfold ea_enabled', al_enabled'.
eapply (tr2fun_ev_al _ _ _ (λ p, enabled R1 (fst p) j)).
∃ (k1+k2). intros k' Hgt.
edestruct Hen_in; eauto.
}
specialize (Hfair j Hea).
eapply ae_taken_equiv in Hfair.
unfold ae_taken', ev_taken' in Hfair.
rewrite (tr2fun_al_ev _ _ _ (λ p, j = snd p)) in Hfair.
destruct (Hfair (k1 + k2)) as (kstep&Hgt&Hstep).
eapply (Hin_ns kstep).
- omega.
- eapply Hen_in. omega.
- auto.
Qed.
End block.
End cofair.