Commit 6ae844ab by Paolo G. Giarrusso

### Allow swapping later^n and forall

`For half of #231.`
parent d04c9f7e
 ... @@ -380,6 +380,11 @@ Proof. ... @@ -380,6 +380,11 @@ Proof. iSpecialize ("Hφ" with "[% //] HP"). done. iSpecialize ("Hφ" with "[% //] HP"). done. Qed. Qed. Lemma demo_laterN_forall {A} (Φ Ψ: A → PROP) n: (∀ x, ▷^n Φ x) -∗ ▷^n (∀ x, Φ x). Proof. iIntros "H" (w). iApply ("H" \$! w). Qed. Lemma test_iNext_laterN_later P n : ▷ ▷^n P -∗ ▷^n ▷ P. Lemma test_iNext_laterN_later P n : ▷ ▷^n P -∗ ▷^n ▷ P. Proof. iIntros "H". iNext. by iNext. Qed. Proof. iIntros "H". iNext. by iNext. Qed. Lemma test_iNext_later_laterN P n : ▷^n ▷ P -∗ ▷ ▷^n P. Lemma test_iNext_later_laterN P n : ▷^n ▷ P -∗ ▷ ▷^n P. ... ...
 ... @@ -301,6 +301,11 @@ Proof. rewrite /IntoExist=> HP. by rewrite HP plainly_exist. Qed. ... @@ -301,6 +301,11 @@ Proof. rewrite /IntoExist=> HP. by rewrite HP plainly_exist. Qed. Global Instance into_forall_later {A} P (Φ : A → PROP) : Global Instance into_forall_later {A} P (Φ : A → PROP) : IntoForall P Φ → IntoForall (▷ P) (λ a, ▷ (Φ a))%I. IntoForall P Φ → IntoForall (▷ P) (λ a, ▷ (Φ a))%I. Proof. rewrite /IntoForall=> HP. by rewrite HP later_forall. Qed. Proof. rewrite /IntoForall=> HP. by rewrite HP later_forall. Qed. Global Instance into_forall_laterN {A} P (Φ : A → PROP) n : IntoForall P Φ → IntoForall (▷^n P) (λ a, ▷^n (Φ a))%I. Proof. rewrite /IntoForall=> HP. by rewrite HP laterN_forall. Qed. Global Instance into_forall_except_0 {A} P (Φ : A → PROP) : Global Instance into_forall_except_0 {A} P (Φ : A → PROP) : IntoForall P Φ → IntoForall (◇ P) (λ a, ◇ (Φ a))%I. IntoForall P Φ → IntoForall (◇ P) (λ a, ◇ (Φ a))%I. Proof. rewrite /IntoForall=> HP. by rewrite HP except_0_forall. Qed. Proof. rewrite /IntoForall=> HP. by rewrite HP except_0_forall. Qed. ... @@ -313,6 +318,11 @@ Proof. rewrite /IntoForall=> HP. by rewrite HP plainly_forall. Qed. ... @@ -313,6 +318,11 @@ Proof. rewrite /IntoForall=> HP. by rewrite HP plainly_forall. Qed. Global Instance from_forall_later {A} P (Φ : A → PROP) : Global Instance from_forall_later {A} P (Φ : A → PROP) : FromForall P Φ → FromForall (▷ P)%I (λ a, ▷ (Φ a))%I. FromForall P Φ → FromForall (▷ P)%I (λ a, ▷ (Φ a))%I. Proof. rewrite /FromForall=> <-. by rewrite later_forall. Qed. Proof. rewrite /FromForall=> <-. by rewrite later_forall. Qed. Global Instance from_forall_laterN {A} P (Φ : A → PROP) n : FromForall P Φ → FromForall (▷^n P)%I (λ a, ▷^n (Φ a))%I. Proof. rewrite /FromForall => <-. by rewrite laterN_forall. Qed. Global Instance from_forall_except_0 {A} P (Φ : A → PROP) : Global Instance from_forall_except_0 {A} P (Φ : A → PROP) : FromForall P Φ → FromForall (◇ P)%I (λ a, ◇ (Φ a))%I. FromForall P Φ → FromForall (◇ P)%I (λ a, ◇ (Φ a))%I. Proof. rewrite /FromForall=> <-. by rewrite except_0_forall. Qed. Proof. rewrite /FromForall=> <-. by rewrite except_0_forall. Qed. ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!