Commit e875cb29 by Robbert Krebbers

### Get rid of `later_proper'`, see discussion in !81.

parent 9539a84c
 ... @@ -672,9 +672,7 @@ Proof. ... @@ -672,9 +672,7 @@ Proof. Qed. Qed. (* Later derived *) (* Later derived *) Lemma later_proper' P Q : (P ⊣⊢ Q) → ▷ P ⊣⊢ ▷ Q. Hint Resolve later_mono. Proof. by intros ->. Qed. Hint Resolve later_mono later_proper'. Global Instance later_mono' : Proper ((⊢) ==> (⊢)) (@uPred_later M). Global Instance later_mono' : Proper ((⊢) ==> (⊢)) (@uPred_later M). Proof. intros P Q; apply later_mono. Qed. Proof. intros P Q; apply later_mono. Qed. Global Instance later_flip_mono' : Global Instance later_flip_mono' : ... @@ -725,9 +723,9 @@ Proof. done. Qed. ... @@ -725,9 +723,9 @@ Proof. done. Qed. Lemma later_laterN n P : ▷^(S n) P ⊣⊢ ▷ ▷^n P. Lemma later_laterN n P : ▷^(S n) P ⊣⊢ ▷ ▷^n P. Proof. done. Qed. Proof. done. Qed. Lemma laterN_later n P : ▷^(S n) P ⊣⊢ ▷^n ▷ P. Lemma laterN_later n P : ▷^(S n) P ⊣⊢ ▷^n ▷ P. Proof. induction n; simpl; auto. Qed. Proof. induction n; f_equiv/=; auto. Qed. Lemma laterN_plus n1 n2 P : ▷^(n1 + n2) P ⊣⊢ ▷^n1 ▷^n2 P. Lemma laterN_plus n1 n2 P : ▷^(n1 + n2) P ⊣⊢ ▷^n1 ▷^n2 P. Proof. induction n1; simpl; auto. Qed. Proof. induction n1; f_equiv/=; auto. Qed. Lemma laterN_le n1 n2 P : n1 ≤ n2 → ▷^n1 P ⊢ ▷^n2 P. Lemma laterN_le n1 n2 P : n1 ≤ n2 → ▷^n1 P ⊢ ▷^n2 P. Proof. induction 1; simpl; by rewrite -?later_intro. Qed. Proof. induction 1; simpl; by rewrite -?later_intro. Qed. ... @@ -745,22 +743,22 @@ Proof. induction n as [|n IH]; simpl; by rewrite -?later_intro. Qed. ... @@ -745,22 +743,22 @@ Proof. induction n as [|n IH]; simpl; by rewrite -?later_intro. Qed. Lemma laterN_True n : ▷^n True ⊣⊢ True. Lemma laterN_True n : ▷^n True ⊣⊢ True. Proof. apply (anti_symm (⊢)); auto using laterN_intro. Qed. Proof. apply (anti_symm (⊢)); auto using laterN_intro. Qed. Lemma laterN_forall {A} n (Φ : A → uPred M) : (▷^n ∀ a, Φ a) ⊣⊢ (∀ a, ▷^n Φ a). Lemma laterN_forall {A} n (Φ : A → uPred M) : (▷^n ∀ a, Φ a) ⊣⊢ (∀ a, ▷^n Φ a). Proof. induction n as [|n IH]; simpl; rewrite -?later_forall; auto. Qed. Proof. induction n as [|n IH]; simpl; rewrite -?later_forall ?IH; auto. Qed. Lemma laterN_exist_2 {A} n (Φ : A → uPred M) : (∃ a, ▷^n Φ a) ⊢ ▷^n (∃ a, Φ a). Lemma laterN_exist_2 {A} n (Φ : A → uPred M) : (∃ a, ▷^n Φ a) ⊢ ▷^n (∃ a, Φ a). Proof. apply exist_elim; eauto using exist_intro, laterN_mono. Qed. Proof. apply exist_elim; eauto using exist_intro, laterN_mono. Qed. Lemma laterN_exist `{Inhabited A} n (Φ : A → uPred M) : Lemma laterN_exist `{Inhabited A} n (Φ : A → uPred M) : (▷^n ∃ a, Φ a) ⊣⊢ ∃ a, ▷^n Φ a. (▷^n ∃ a, Φ a) ⊣⊢ ∃ a, ▷^n Φ a. Proof. induction n as [|n IH]; simpl; rewrite -?later_exist; auto. Qed. Proof. induction n as [|n IH]; simpl; rewrite -?later_exist ?IH; auto. Qed. Lemma laterN_and n P Q : ▷^n (P ∧ Q) ⊣⊢ ▷^n P ∧ ▷^n Q. Lemma laterN_and n P Q : ▷^n (P ∧ Q) ⊣⊢ ▷^n P ∧ ▷^n Q. Proof. induction n as [|n IH]; simpl; rewrite -?later_and; auto. Qed. Proof. induction n as [|n IH]; simpl; rewrite -?later_and ?IH; auto. Qed. Lemma laterN_or n P Q : ▷^n (P ∨ Q) ⊣⊢ ▷^n P ∨ ▷^n Q. Lemma laterN_or n P Q : ▷^n (P ∨ Q) ⊣⊢ ▷^n P ∨ ▷^n Q. Proof. induction n as [|n IH]; simpl; rewrite -?later_or; auto. Qed. Proof. induction n as [|n IH]; simpl; rewrite -?later_or ?IH; auto. Qed. Lemma laterN_impl n P Q : ▷^n (P → Q) ⊢ ▷^n P → ▷^n Q. Lemma laterN_impl n P Q : ▷^n (P → Q) ⊢ ▷^n P → ▷^n Q. Proof. Proof. apply impl_intro_l; rewrite -laterN_and; eauto using impl_elim, laterN_mono. apply impl_intro_l; rewrite -laterN_and; eauto using impl_elim, laterN_mono. Qed. Qed. Lemma laterN_sep n P Q : ▷^n (P ∗ Q) ⊣⊢ ▷^n P ∗ ▷^n Q. Lemma laterN_sep n P Q : ▷^n (P ∗ Q) ⊣⊢ ▷^n P ∗ ▷^n Q. Proof. induction n as [|n IH]; simpl; rewrite -?later_sep; auto. Qed. Proof. induction n as [|n IH]; simpl; rewrite -?later_sep ?IH; auto. Qed. Lemma laterN_wand n P Q : ▷^n (P -∗ Q) ⊢ ▷^n P -∗ ▷^n Q. Lemma laterN_wand n P Q : ▷^n (P -∗ Q) ⊢ ▷^n P -∗ ▷^n Q. Proof. Proof. apply wand_intro_r; rewrite -laterN_sep; eauto using wand_elim_l,laterN_mono. apply wand_intro_r; rewrite -laterN_sep; eauto using wand_elim_l,laterN_mono. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!