Commit 5d8aef49 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix issue #127.

parent 09741a03
......@@ -327,6 +327,13 @@ Global Instance into_wand_iff_r p P P' Q Q' :
WandWeaken p Q P Q' P' IntoWand p (P Q) Q' P'.
Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_r', impl_wand_1. Qed.
Global Instance into_wand_forall_prop p (φ : Prop) P :
IntoWand p ( _ : φ, P) φ P.
Proof.
rewrite /FromAssumption /IntoWand persistently_if_pure -pure_impl_forall.
by apply impl_wand_1.
Qed.
Global Instance into_wand_forall {A} p (Φ : A uPred M) P Q x :
IntoWand p (Φ x) P Q IntoWand p ( x, Φ x) P Q.
Proof. rewrite /IntoWand=> <-. apply forall_elim. Qed.
......@@ -775,6 +782,18 @@ Proof. rewrite /IntoForall=> HP. by rewrite HP later_forall. Qed.
Global Instance into_forall_except_0 {A} P (Φ : A uPred M) :
IntoForall P Φ IntoForall ( P) (λ a, (Φ a))%I.
Proof. rewrite /IntoForall=> HP. by rewrite HP except_0_forall. Qed.
Global Instance into_forall_impl_pure φ P Q :
FromPureT P φ IntoForall (P Q) (λ _ : φ, Q).
Proof.
rewrite /FromPureT /FromPure /IntoForall=> -[φ' [-> <-]].
by rewrite pure_impl_forall.
Qed.
Global Instance into_forall_wand_pure φ P Q :
FromPureT P φ IntoForall (P - Q) (λ _ : φ, Q).
Proof.
rewrite /FromPureT /FromPure /IntoForall=> -[φ' [-> <-]].
by rewrite -pure_impl_forall -impl_wand.
Qed.
(* FromForall *)
Global Instance from_forall_forall {A} (Φ : A uPred M) :
......
......@@ -54,6 +54,13 @@ Class FromPure {M} (P : uPred M) (φ : Prop) := from_pure : ⌜φ⌝ ⊢ P.
Arguments from_pure {_} _ _ {_}.
Hint Mode FromPure + ! - : typeclass_instances.
Class FromPureT {M} (P : uPred M) (φ : Type) :=
from_pureT : ψ : Prop, φ = ψ FromPure P ψ.
Lemma from_pureT_hint {M} (P : uPred M) (φ : Prop) : FromPure P φ FromPureT P φ.
Proof. by exists φ. Qed.
Hint Extern 0 (FromPureT _ _) =>
notypeclasses refine (from_pureT_hint _ _ _) : typeclass_instances.
Class IntoInternalEq {M} {A : ofeT} (P : uPred M) (x y : A) :=
into_internal_eq : P x y.
Arguments into_internal_eq {_ _} _ _ _ {_}.
......
......@@ -396,8 +396,11 @@ Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
|typeclasses eauto ||
let P := match goal with |- IntoForall ?P _ => P end in
fail "iSpecialize: cannot instantiate" P "with" x
|lazymatch goal with (* Force [A] in [ex_intro] to deal with coercions. *)
| |- _ : ?A, _ => refine (@ex_intro A _ x (conj _ _))
|match goal with (* Force [A] in [ex_intro] to deal with coercions. *)
| |- _ : ?A, _ => refine (@ex_intro A _ x (conj _ _)); [|]
(* If the existentially quantified predicate is non-dependent and [x]
is a hole, [refine] will generate an additional goal it. *)
| |- _ : ?A, _ => refine (@ex_intro A _ x (conj _ _));[shelve| |]
end; [env_reflexivity|go xs]]
end in
go xs.
......
......@@ -234,6 +234,50 @@ Lemma test_iIntros_rewrite P (x1 x2 x3 x4 : nat) :
x1 = x2 ( x2 = x3 x3 x4 P) - x1 = x4 P.
Proof. iIntros (?) "(-> & -> & $)"; auto. Qed.
(* A bunch of test cases from #127 to establish that tactics behave the same on
`⌜ φ ⌝ → P` and `∀ _ : φ, P` *)
Lemma test_forall_nondep_1 (φ : Prop) :
φ ( _ : φ, False : uPred M) - False.
Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed.
Lemma test_forall_nondep_2 (φ : Prop) :
φ ( _ : φ, False : uPred M) - False.
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
Lemma test_forall_nondep_3 (φ : Prop) :
φ ( _ : φ, False : uPred M) - False.
Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _). done. done. Qed.
Lemma test_forall_nondep_4 (φ : Prop) :
φ ( _ : φ, False : uPred M) - False.
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ); done. Qed.
Lemma test_pure_impl_1 (φ : Prop) :
φ (⌜φ⌝ False : uPred M) - False.
Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed.
Lemma test_pure_impl_2 (φ : Prop) :
φ (⌜φ⌝ False : uPred M) - False.
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
Lemma test_pure_impl_3 (φ : Prop) :
φ (⌜φ⌝ False : uPred M) - False.
Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _). done. done. Qed.
Lemma test_pure_impl_4 (φ : Prop) :
φ (⌜φ⌝ False : uPred M) - False.
Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ). done. Qed.
Lemma test_forall_nondep_impl2 (φ : Prop) P :
φ P - ( _ : φ, P - False : uPred M) - False.
Proof.
iIntros (Hφ) "HP Hφ".
Fail iSpecialize ("Hφ" with "HP").
iSpecialize ("Hφ" with "[% //] HP"). done.
Qed.
Lemma test_pure_impl2 (φ : Prop) P :
φ P - (⌜φ⌝ P - False : uPred M) - False.
Proof.
iIntros (Hφ) "HP Hφ".
Fail iSpecialize ("Hφ" with "HP").
iSpecialize ("Hφ" with "[% //] HP"). done.
Qed.
(* TODO: This test is broken in Coq 8.6. Should be restored once we drop Coq
8.6 support. See also issue #108. *)
(*
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment