diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index df2cc9712695a348b65241118b0cc74435b34347..88de82408c9ba9da6900c291d95b6e563354db03 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -494,9 +494,24 @@ In nested Ltac calls to "iSpecialize (open_constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
-"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
-failed.
-Tactic failure: iSpecialize: "H" not found.
+"iSpecializePat (open_constr) (constr)", "iSpecializePat_go" and
+"notypeclasses refine (uconstr)", last call failed.
+Illegal application (Non-functional construction):
+The expression
+ "coq_tactics.tac_specialize false
+ {|
+ environments.env_intuitionistic := ;
+ environments.env_spatial := "HW" : P -∗ Q
+ "HP" : P
+ ;
+ environments.env_counter := 1%positive |} "H" "HW"
+ ?q ?P2 ?R ?Q ?f" of type
+ ""HW" : P -∗ Q
+ "HP" : P
+ --------------------------------------∗
+ ?Q
+ " cannot be applied to the term
+ "?y" : "?T"
"iExact_fail"
: string
The command has indeed failed with message:
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 91a7a384b9ef81c8dab55044c22194aa459595fc..88d3c9f5c0d70ead7410abbe7f6d0f3626b4946a 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -61,15 +61,18 @@ Proof. intros H. induction H; simpl; apply _. Qed.
Lemma tac_emp_intro Δ : AffineEnv (env_spatial Δ) → envs_entails Δ emp.
Proof. intros. by rewrite envs_entails_eq (affine (of_envs Δ)). Qed.
-(* TODO: convert to not take Δ' *)
-Lemma tac_assumption Δ Δ' i p P Q :
- envs_lookup_delete true i Δ = Some (p,P,Δ') →
- FromAssumption p P Q →
- (if env_spatial_is_nil Δ' then TCTrue
- else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ'))) →
+Lemma tac_assumption Δ i Q :
+ match envs_lookup_delete true i Δ with
+ | None => False
+ | Some (p,P,Δ') =>
+ FromAssumption p P Q ∧
+ (if env_spatial_is_nil Δ' then TCTrue
+ else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ')))
+ end →
envs_entails Δ Q.
Proof.
- intros ?? H. rewrite envs_entails_eq envs_lookup_delete_sound //.
+ destruct envs_lookup_delete as [((p&P)&Δ')|] eqn:Hlookup; last by (intros; exfalso).
+ intros (?&H). rewrite envs_entails_eq envs_lookup_delete_sound //.
destruct (env_spatial_is_nil Δ') eqn:?.
- by rewrite (env_spatial_is_nil_intuitionistically Δ') // sep_elim_l.
- rewrite from_assumption. destruct H; by rewrite sep_elim_l.
@@ -88,14 +91,17 @@ Proof.
by rewrite wand_elim_r.
Qed.
-(* TODO: convert to not take Δ' *)
-Lemma tac_clear Δ Δ' i p P Q :
- envs_lookup_delete true i Δ = Some (p,P,Δ') →
- (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) →
- envs_entails Δ' Q →
+Lemma tac_clear Δ i Q :
+ match envs_lookup_delete true i Δ with
+ | None => False
+ | Some (p,P,Δ') =>
+ (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) ∧
+ envs_entails Δ' Q
+ end →
envs_entails Δ Q.
Proof.
- rewrite envs_entails_eq=> ?? HQ. rewrite envs_lookup_delete_sound //.
+ destruct envs_lookup_delete as [((p&P)&Δ')|] eqn:Hlookup; last by (intros; exfalso).
+ rewrite envs_entails_eq. intros(?&HQ). rewrite envs_lookup_delete_sound //.
by destruct p; rewrite /= HQ sep_elim_r.
Qed.
@@ -124,14 +130,18 @@ Proof.
- by apply pure_intro.
Qed.
-(* TODO: convert to not take Δ' *)
-Lemma tac_pure Δ Δ' i p P φ Q :
- envs_lookup_delete true i Δ = Some (p, P, Δ') →
- IntoPure P φ →
- (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) →
- (φ → envs_entails Δ' Q) → envs_entails Δ Q.
+Lemma tac_pure Δ i φ Q :
+ match envs_lookup_delete true i Δ with
+ | None => False
+ | Some (p, P, Δ') =>
+ IntoPure P φ ∧
+ (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) ∧
+ (φ → envs_entails Δ' Q)
+ end →
+ envs_entails Δ Q.
Proof.
- rewrite envs_entails_eq=> ?? HPQ HQ.
+ destruct envs_lookup_delete as [((p&P)&Δ')|] eqn:Hlookup; last by (intros; exfalso).
+ rewrite envs_entails_eq. intros (?&HPQ&HQ).
rewrite envs_lookup_delete_sound //; simpl. destruct p; simpl.
- rewrite (into_pure P) -persistently_and_intuitionistically_sep_l persistently_pure.
by apply pure_elim_l.
@@ -253,18 +263,23 @@ Qed.
(* This is pretty much [tac_specialize_assert] with [js:=[j]] and [tac_exact],
but it is doing some work to keep the order of hypotheses preserved. *)
(* TODO: convert to not take Δ' *)
-Lemma tac_specialize remove_intuitionistic Δ Δ' i p j q P1 P2 R Q :
- envs_lookup_delete remove_intuitionistic i Δ = Some (p, P1, Δ') →
- envs_lookup j Δ' = Some (q, R) →
- IntoWand q p R P1 P2 →
- match envs_replace j q (p && q) (Esnoc Enil j P2) Δ' with
- | Some Δ'' => envs_entails Δ'' Q
- | None => False
- end → envs_entails Δ Q.
+Lemma tac_specialize remove_intuitionistic Δ i j q P2 R Q :
+ match envs_lookup_delete remove_intuitionistic i Δ with
+ | None => False → envs_entails Δ Q
+ | Some (p, P1, Δ') =>
+ envs_lookup j Δ' = Some (q, R) →
+ IntoWand q p R P1 P2 →
+ match envs_replace j q (p && q) (Esnoc Enil j P2) Δ' with
+ | None => False
+ | Some Δ'' => envs_entails Δ'' Q
+ end → envs_entails Δ Q
+ end.
Proof.
+ destruct envs_lookup_delete as [((p&P)&Δ')|] eqn:Hlookup; last by (intros; exfalso).
rewrite envs_entails_eq /IntoWand.
- intros [? ->]%envs_lookup_delete_Some ? HR ?.
- destruct (envs_replace _ _ _ _ _) as [Δ''|] eqn:?; last done.
+ apply envs_lookup_delete_Some in Hlookup as (?&->).
+ destruct (envs_replace) as [Δ''|] eqn:Hrep; last by (intros; exfalso; intuition).
+ intros ? HR <-.
rewrite (envs_lookup_sound' _ remove_intuitionistic) //.
rewrite envs_replace_singleton_sound //. destruct p; simpl in *.
- rewrite -{1}intuitionistically_idemp -{1}intuitionistically_if_idemp.
@@ -273,17 +288,29 @@ Proof.
- by rewrite HR assoc !wand_elim_r.
Qed.
-Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q neg js R P1 P2 P1' Q :
- envs_lookup_delete true j Δ = Some (q, R, Δ') →
- IntoWand q false R P1 P2 → AddModal P1' P1 Q →
- (''(Δ1,Δ2) ← envs_split (if neg is true then Right else Left) js Δ';
- Δ2' ← envs_app false (Esnoc Enil j P2) Δ2;
- Some (Δ1,Δ2')) = Some (Δ1,Δ2') → (* does not preserve position of [j] *)
- envs_entails Δ1 P1' → envs_entails Δ2' Q → envs_entails Δ Q.
+Lemma tac_specialize_assert Δ j neg js P1 P2 P1' Q :
+ match envs_lookup_delete true j Δ with
+ | None => False → envs_entails Δ Q
+ | Some (q, R, Δ') =>
+ IntoWand q false R P1 P2 →
+ AddModal P1' P1 Q →
+ match
+ (''(Δ1,Δ2) ← envs_split (if neg is true then Right else Left) js Δ';
+ Δ2' ← envs_app false (Esnoc Enil j P2) Δ2;
+ Some (Δ1,Δ2')) (* does not preserve position of [j] *)
+ with
+ | None => False → envs_entails Δ Q
+ | Some (Δ1,Δ2') =>
+ envs_entails Δ1 P1' → envs_entails Δ2' Q → envs_entails Δ Q
+ end
+ end.
Proof.
- rewrite envs_entails_eq. intros [? ->]%envs_lookup_delete_Some ??? HP1 HQ.
- destruct (envs_split _ _ _) as [[? Δ2]|] eqn:?; simplify_eq/=;
- destruct (envs_app _ _ _) eqn:?; simplify_eq/=.
+ destruct envs_lookup_delete as [((q&R)&Δ')|] eqn:Hlookup; last by (intros; exfalso).
+ rewrite envs_entails_eq. apply envs_lookup_delete_Some in Hlookup as (?&->).
+ intros ? ?.
+ destruct (envs_split _ _ _) as [[? Δ2]|] eqn:Heq_split; simplify_eq/=; last by (intros; exfalso).
+ destruct (envs_app _ _ _) eqn:Heq_app; simplify_eq/=; last by (intros; exfalso).
+ intros HP1 HQ.
rewrite envs_lookup_sound // envs_split_sound //.
rewrite (envs_app_singleton_sound Δ2) //; simpl.
rewrite HP1 (into_wand q false) /= -(add_modal P1' P1 Q). cancel [P1'].
@@ -297,15 +324,21 @@ Proof. rewrite envs_entails_eq=> ->. by rewrite -lock -True_sep_2. Qed.
Lemma tac_unlock Δ Q : envs_entails Δ Q → envs_entails Δ (locked Q).
Proof. by unlock. Qed.
-Lemma tac_specialize_frame Δ Δ' j q R P1 P2 P1' Q Q' :
- envs_lookup_delete true j Δ = Some (q, R, Δ') →
- IntoWand q false R P1 P2 →
- AddModal P1' P1 Q →
- envs_entails Δ' (P1' ∗ locked Q') →
- Q' = (P2 -∗ Q)%I →
- envs_entails Δ Q.
+Lemma tac_specialize_frame Δ j P1 P2 P1' Q Q' :
+ match envs_lookup_delete true j Δ with
+ | None => False → envs_entails Δ Q
+ | Some (q, R, Δ') =>
+ IntoWand q false R P1 P2 →
+ AddModal P1' P1 Q →
+ envs_entails Δ' (P1' ∗ locked Q') →
+ Q' = (P2 -∗ Q)%I →
+ envs_entails Δ Q
+ end.
Proof.
- rewrite envs_entails_eq. intros [? ->]%envs_lookup_delete_Some ?? HPQ ->.
+ destruct envs_lookup_delete as [((q&R)&Δ')|] eqn:Hlookup; last by (intros; exfalso).
+ rewrite envs_entails_eq.
+ apply envs_lookup_delete_Some in Hlookup as (?&->).
+ intros ? ? HPQ ->.
rewrite envs_lookup_sound //. rewrite HPQ -lock.
rewrite (into_wand q false) -{2}(add_modal P1' P1 Q). cancel [P1'].
apply wand_intro_l. by rewrite assoc !wand_elim_r.
@@ -330,20 +363,27 @@ Proof.
by rewrite intuitionistically_emp left_id wand_elim_r.
Qed.
-Lemma tac_specialize_assert_intuitionistic Δ Δ' j q P1 P1' P2 R Q :
- envs_lookup_delete true j Δ = Some (q, R, Δ') →
- IntoWand q true R P1 P2 →
- Persistent P1 →
- IntoAbsorbingly P1' P1 →
- envs_entails Δ' P1' →
- match envs_simple_replace j q (Esnoc Enil j P2) Δ with
- | Some Δ'' => envs_entails Δ'' Q
- | None => False
- end → envs_entails Δ Q.
+Lemma tac_specialize_assert_intuitionistic Δ j P1 P1' P2 Q :
+ match envs_lookup_delete true j Δ with
+ | None => False → envs_entails Δ Q
+ | Some (q, R, Δ') =>
+ IntoWand q true R P1 P2 →
+ Persistent P1 →
+ IntoAbsorbingly P1' P1 →
+ envs_entails Δ' P1' →
+ match envs_simple_replace j q (Esnoc Enil j P2) Δ with
+ | None => False → envs_entails Δ Q
+ | Some Δ'' =>
+ envs_entails Δ'' Q → envs_entails Δ Q
+ end
+ end.
Proof.
- rewrite envs_entails_eq => /envs_lookup_delete_Some [? ->] ??? HP1 HQ.
- destruct (envs_simple_replace _ _ _ _) as [Δ''|] eqn:?; last done.
- rewrite -HQ envs_lookup_sound //.
+ destruct envs_lookup_delete as [((q&R)&Δ')|] eqn:Hlookup; last by (intros; exfalso).
+ apply envs_lookup_delete_Some in Hlookup as (?&->).
+ rewrite envs_entails_eq.
+ destruct (envs_simple_replace) as [Δ''|] eqn:Hrep; last by (intros; exfalso; intuition).
+ intros ? ? ? HP1 <- .
+ rewrite envs_lookup_sound //.
rewrite -(idemp bi_and (of_envs (envs_delete _ _ _ _))).
rewrite {2}envs_simple_replace_singleton_sound' //; simpl.
rewrite {1}HP1 (into_absorbingly P1' P1) (persistent_persistently_2 P1).
@@ -464,12 +504,17 @@ Proof.
by rewrite wand_elim_r.
Qed.
-Lemma tac_apply Δ Δ' i p R P1 P2 :
- envs_lookup_delete true i Δ = Some (p, R, Δ') →
- IntoWand p false R P1 P2 →
- envs_entails Δ' P1 → envs_entails Δ P2.
+Lemma tac_apply Δ i P1 P2 :
+ match envs_lookup_delete true i Δ with
+ | None => False
+ | Some (p, R, Δ') =>
+ IntoWand p false R P1 P2 ∧
+ envs_entails Δ' P1
+ end →
+ envs_entails Δ P2.
Proof.
- rewrite envs_entails_eq => ?? HP1. rewrite envs_lookup_delete_sound //.
+ destruct envs_lookup_delete as [((p&R)&Δ')|] eqn:Hlookup; last by (intros; exfalso).
+ rewrite envs_entails_eq. intros (?&HP1). rewrite envs_lookup_delete_sound //.
by rewrite (into_wand p false) /= HP1 wand_elim_l.
Qed.
@@ -570,13 +615,19 @@ Proof.
auto using and_intro, pure_intro.
Qed.
-Lemma tac_frame Δ Δ' i p R P Q :
- envs_lookup_delete false i Δ = Some (p, R, Δ') →
- Frame p R P Q →
- envs_entails Δ' Q → envs_entails Δ P.
+Lemma tac_frame Δ i P Q :
+ match envs_lookup_delete false i Δ with
+ | None => False
+ | Some (p, R, Δ') =>
+ Frame p R P Q ∧
+ envs_entails Δ' Q
+ end →
+ envs_entails Δ P.
Proof.
- rewrite envs_entails_eq. intros [? ->]%envs_lookup_delete_Some Hframe HQ.
- rewrite (envs_lookup_sound' _ false) //. by rewrite -Hframe HQ.
+ destruct envs_lookup_delete as [((p&R)&Δ')|] eqn:Hlookup; last by (intros; exfalso).
+ rewrite envs_entails_eq. intros (Hframe&Heq).
+ apply envs_lookup_delete_Some in Hlookup as (?&->).
+ rewrite (envs_lookup_sound' _ false) //. by rewrite -Hframe Heq.
Qed.
(** * Disjunction *)
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 39c63598d2cc805916750b8af847624049512e65..efc3245d742d62a6f4a122efdc4f09f1a9e53ade 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -172,15 +172,20 @@ Ltac iElaborateSelPat pat :=
end.
Local Ltac iClearHyp H :=
- eapply tac_clear with _ H _ _; (* (i:=H) *)
- [pm_reflexivity ||
- let H := pretty_ident H in
- fail "iClear:" H "not found"
- |pm_reduce; iSolveTC ||
- let H := pretty_ident H in
- let P := match goal with |- TCOr (Affine ?P) _ => P end in
- fail "iClear:" H ":" P "not affine and the goal not absorbing"
- |].
+ eapply tac_clear with H; (* (i:=H) *)
+ pm_reduce;
+ lazymatch goal with
+ | |- False =>
+ let H := pretty_ident H in
+ fail "iClear:" H "not found"
+ | _ =>
+ esplit;
+ [pm_reduce; iSolveTC ||
+ let H := pretty_ident H in
+ let P := match goal with |- TCOr (Affine ?P) _ => P end in
+ fail "iClear:" H ":" P "not affine and the goal not absorbing"
+ |]
+ end.
Local Ltac iClear_go Hs :=
lazymatch Hs with
@@ -228,17 +233,22 @@ Ltac, but it may be possible in Ltac2. *)
(** * Assumptions *)
Tactic Notation "iExact" constr(H) :=
- eapply tac_assumption with _ H _ _; (* (i:=H) *)
- [pm_reflexivity ||
- let H := pretty_ident H in
- fail "iExact:" H "not found"
- |iSolveTC ||
- let H := pretty_ident H in
- let P := match goal with |- FromAssumption _ ?P _ => P end in
- fail "iExact:" H ":" P "does not match goal"
- |pm_reduce; iSolveTC ||
- let H := pretty_ident H in
- fail "iExact:" H "not absorbing and the remaining hypotheses not affine"].
+ eapply tac_assumption with H; (* (i:=H) *)
+ pm_reduce;
+ lazymatch goal with
+ |- False =>
+ let H := pretty_ident H in
+ fail "iExact:" H "not found"
+ | _ =>
+ split;
+ [iSolveTC ||
+ let H := pretty_ident H in
+ let P := match goal with |- FromAssumption _ ?P _ => P end in
+ fail "iExact:" H ":" P "does not match goal"
+ |pm_reduce; iSolveTC ||
+ let H := pretty_ident H in
+ fail "iExact:" H "not absorbing and the remaining hypotheses not affine"]
+ end.
Tactic Notation "iAssumptionCore" :=
let rec find Γ i P :=
@@ -262,11 +272,16 @@ Tactic Notation "iAssumption" :=
lazymatch Γ with
| Esnoc ?Γ ?j ?P => first
[pose proof (_ : FromAssumption p P Q) as Hass;
- eapply (tac_assumption _ _ j p P);
- [pm_reflexivity
- |apply Hass
- |pm_reduce; iSolveTC ||
- fail 1 "iAssumption:" j "not absorbing and the remaining hypotheses not affine"]
+ eapply (tac_assumption _ j);
+ pm_reduce;
+ lazymatch goal with
+ |- False => fail 1
+ | _ =>
+ split;
+ [apply Hass
+ |pm_reduce; iSolveTC ||
+ fail 1 "iAssumption:" j "not absorbing and the remaining hypotheses not affine"]
+ end
|assert (P = False%I) as Hass by reflexivity;
apply (tac_false_destruct _ j p P);
[pm_reflexivity
@@ -297,17 +312,22 @@ Local Tactic Notation "iIntuitionistic" constr(H) :=
|pm_reduce].
Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
- eapply tac_pure with _ H _ _ _; (* (i:=H1) *)
- [pm_reflexivity ||
- let H := pretty_ident H in
- fail "iPure:" H "not found"
- |iSolveTC ||
- let P := match goal with |- IntoPure ?P _ => P end in
- fail "iPure:" P "not pure"
- |pm_reduce; iSolveTC ||
- let P := match goal with |- TCOr (Affine ?P) _ => P end in
- fail "iPure:" P "not affine and the goal not absorbing"
- |intros pat].
+ eapply tac_pure with H _; (* (i:=H1) *)
+ pm_reduce;
+ lazymatch goal with
+ | |- False =>
+ let H := pretty_ident H in
+ fail "iPure:" H "not found"
+ | _ =>
+ split_and!;
+ [iSolveTC ||
+ let P := match goal with |- IntoPure ?P _ => P end in
+ fail "iPure:" P "not pure"
+ |pm_reduce; iSolveTC ||
+ let P := match goal with |- TCOr (Affine ?P) _ => P end in
+ fail "iPure:" P "not affine and the goal not absorbing"
+ |intros pat]
+ end.
Tactic Notation "iEmpIntro" :=
iStartProof;
@@ -342,14 +362,19 @@ Local Ltac iFramePure t :=
Local Ltac iFrameHyp H :=
iStartProof;
- eapply tac_frame with _ H _ _ _;
- [pm_reflexivity ||
- let H := pretty_ident H in
- fail "iFrame:" H "not found"
- |iSolveTC ||
- let R := match goal with |- Frame _ ?R _ _ => R end in
- fail "iFrame: cannot frame" R
- |iFrameFinish].
+ eapply tac_frame with H _;
+ [pm_reduce;
+ lazymatch goal with
+ |- False =>
+ let H := pretty_ident H in
+ fail "iFrame:" H "not found"
+ | _ =>
+ split;
+ [iSolveTC ||
+ let R := match goal with |- Frame _ ?R _ _ => R end in
+ fail "iFrame: cannot frame" R
+ |iFrameFinish]
+ end].
Local Ltac iFrameAnyPure :=
repeat match goal with H : _ |- _ => iFramePure H end.
@@ -784,18 +809,28 @@ Ltac iSpecializePat_go H1 pats :=
| SIdent ?H2 [] :: ?pats =>
(* If we not need to specialize [H2] we can avoid a lot of unncessary
context manipulation. *)
- notypeclasses refine (tac_specialize false _ _ H2 _ H1 _ _ _ _ _ _ _ _ _);
- [pm_reflexivity ||
- let H2 := pretty_ident H2 in
- fail "iSpecialize:" H2 "not found"
- |pm_reflexivity ||
+ match goal with
+ | |- envs_entails ?Δ _ =>
+ notypeclasses refine (tac_specialize false Δ H2 H1 _ _ _ _ _ _ _);
+ [ lazymatch goal with
+ | |- False =>
+ let H2 := pretty_ident H2 in
+ fail "iSpecialize:" H2 "not found"
+ | _ =>
+ pm_reflexivity ||
let H1 := pretty_ident H1 in
fail "iSpecialize:" H1 "not found"
+ end
|iSolveTC ||
let P := match goal with |- IntoWand _ _ ?P ?Q _ => P end in
let Q := match goal with |- IntoWand _ _ ?P ?Q _ => Q end in
fail "iSpecialize: cannot instantiate" P "with" Q
- |pm_reduce; iSpecializePat_go H1 pats]
+ |pm_reduce;
+ lazymatch goal with
+ | |- False => fail
+ | _ => iSpecializePat_go H1 pats
+ end]
+ end
| SIdent ?H2 ?pats1 :: ?pats =>
(* If [H2] is in the intuitionistic context, we copy it into a new
hypothesis [Htmp], so that it can be used multiple times. *)
@@ -811,18 +846,29 @@ Ltac iSpecializePat_go H1 pats :=
Ltac backtraces (which would otherwise include the whole closure). *)
[.. (* side-conditions of [iSpecialize] *)
|(* Use [remove_intuitionistic = true] to remove the copy [Htmp]. *)
- notypeclasses refine (tac_specialize true _ _ H2tmp _ H1 _ _ _ _ _ _ _ _ _);
- [pm_reflexivity ||
- let H2tmp := pretty_ident H2tmp in
- fail "iSpecialize:" H2tmp "not found"
- |pm_reflexivity ||
+ match goal with
+ | |- envs_entails ?Δ _ =>
+ (* TODO: the error handling here does not seem correct now *)
+ notypeclasses refine (tac_specialize true Δ H2tmp H1 _ _ _ _ _ _ _);
+ [ lazymatch goal with
+ | |- False =>
+ let H2tmp := pretty_ident H2tmp in
+ fail "iSpecialize:" H2tmp "not found"
+ | _ =>
+ pm_reflexivity ||
let H1 := pretty_ident H1 in
fail "iSpecialize:" H1 "not found"
+ end
|iSolveTC ||
let P := match goal with |- IntoWand _ _ ?P ?Q _ => P end in
let Q := match goal with |- IntoWand _ _ ?P ?Q _ => Q end in
fail "iSpecialize: cannot instantiate" P "with" Q
- |pm_reduce; iSpecializePat_go H1 pats]]
+ |pm_reduce;
+ lazymatch goal with
+ | |- False => fail
+ | _ => iSpecializePat_go H1 pats
+ end]
+ end]
| SPureGoal ?d :: ?pats =>
notypeclasses refine (tac_specialize_assert_pure _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
[pm_reflexivity ||
@@ -836,62 +882,92 @@ Ltac iSpecializePat_go H1 pats :=
|pm_reduce;
iSpecializePat_go H1 pats]
| SGoal (SpecGoal GIntuitionistic false ?Hs_frame [] ?d) :: ?pats =>
- notypeclasses refine (tac_specialize_assert_intuitionistic _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
- [pm_reflexivity ||
- let H1 := pretty_ident H1 in
- fail "iSpecialize:" H1 "not found"
- |solve_to_wand H1
- |iSolveTC ||
- let Q := match goal with |- Persistent ?Q => Q end in
- fail "iSpecialize:" Q "not persistent"
- |iSolveTC
- |iFrame Hs_frame; solve_done d (*goal*)
- |pm_reduce; iSpecializePat_go H1 pats]
+ match goal with
+ | |- envs_entails ?Δ _ =>
+ notypeclasses refine (tac_specialize_assert_intuitionistic Δ H1 _ _ _ _ _ _ _ _ _);
+ [ lazymatch goal with
+ | |- False =>
+ let H1 := pretty_ident H1 in
+ fail "iSpecialize:" H1 "not found"
+ | _ =>
+ solve_to_wand H1
+ end
+ |iSolveTC ||
+ let Q := match goal with |- Persistent ?Q => Q end in
+ fail "iSpecialize:" Q "not persistent"
+ |iSolveTC
+ |iFrame Hs_frame; solve_done d (*goal*)
+ | pm_reduce; iSpecializePat_go H1 pats]
+ end
| SGoal (SpecGoal GIntuitionistic _ _ _ _) :: ?pats =>
fail "iSpecialize: cannot select hypotheses for intuitionistic premise"
| SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs ?d) :: ?pats =>
let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in
- notypeclasses refine (tac_specialize_assert _ _ _ _ H1 _ lr Hs' _ _ _ _ _ _ _ _ _ _ _);
- [pm_reflexivity ||
- let H1 := pretty_ident H1 in
- fail "iSpecialize:" H1 "not found"
- |solve_to_wand H1
- |lazymatch m with
- | GSpatial => class_apply add_modal_id
- | GModal => iSolveTC || fail "iSpecialize: goal not a modality"
- end
- |pm_reflexivity ||
- let Hs' := iMissingHyps Hs' in
- fail "iSpecialize: hypotheses" Hs' "not found"
- |iFrame Hs_frame; solve_done d (*goal*)
- |iSpecializePat_go H1 pats]
+ match goal with
+ | |- envs_entails ?Δ _ =>
+ notypeclasses refine (tac_specialize_assert Δ H1 lr Hs' _ _ _ _ _ _ _ _);
+ [ lazymatch goal with
+ | |- False =>
+ let H1 := pretty_ident H1 in
+ fail "iSpecialize:" H1 "not found"
+ | |- ?H =>
+ solve_to_wand H1
+ end
+ |lazymatch m with
+ | GSpatial => class_apply add_modal_id
+ | GModal => iSolveTC || fail "iSpecialize: goal not a modality"
+ end
+ |pm_reduce;
+ match goal with
+ | |- False =>
+ let Hs' := iMissingHyps Hs' in
+ fail "iSpecialize: hypotheses" Hs' "not found"
+ | _ =>
+ iFrame Hs_frame; solve_done d (*goal*)
+ end
+ |iSpecializePat_go H1 pats
+ ]
+ end
| SAutoFrame GIntuitionistic :: ?pats =>
- notypeclasses refine (tac_specialize_assert_intuitionistic _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
- [pm_reflexivity ||
- let H1 := pretty_ident H1 in
- fail "iSpecialize:" H1 "not found"
- |solve_to_wand H1
+ match goal with
+ | |- envs_entails ?Δ _ =>
+ notypeclasses refine (tac_specialize_assert_intuitionistic Δ H1 _ _ _ _ _ _ _ _ _);
+ [ lazymatch goal with
+ | |- False =>
+ let H1 := pretty_ident H1 in
+ fail "iSpecialize:" H1 "not found"
+ | _ =>
+ solve_to_wand H1
+ end
|iSolveTC ||
let Q := match goal with |- Persistent ?Q => Q end in
fail "iSpecialize:" Q "not persistent"
+ |iSolveTC
|solve [iFrame "∗ #"]
- |pm_reduce; iSpecializePat_go H1 pats]
+ |iSpecializePat_go H1 pats]
+ end
| SAutoFrame ?m :: ?pats =>
- notypeclasses refine (tac_specialize_frame _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
- [pm_reflexivity ||
- let H1 := pretty_ident H1 in
- fail "iSpecialize:" H1 "not found"
- |solve_to_wand H1
- |lazymatch m with
- | GSpatial => class_apply add_modal_id
- | GModal => iSolveTC || fail "iSpecialize: goal not a modality"
- end
- |first
- [notypeclasses refine (tac_unlock_emp _ _ _)
- |notypeclasses refine (tac_unlock_True _ _ _)
- |iFrame "∗ #"; notypeclasses refine (tac_unlock _ _ _)
- |fail "iSpecialize: premise cannot be solved by framing"]
- |exact eq_refl]; iIntro H1; iSpecializePat_go H1 pats
+ match goal with
+ | |- envs_entails ?Δ _ =>
+ notypeclasses refine (tac_specialize_frame Δ H1 _ _ _ _ _ _ _ _ _);
+ [ lazymatch goal with
+ | |- False =>
+ let H1 := pretty_ident H1 in
+ fail "iSpecialize:" H1 "not found"
+ | _ =>
+ solve_to_wand H1
+ end
+ |lazymatch m with
+ | GSpatial => class_apply add_modal_id
+ | GModal => iSolveTC || fail "iSpecialize: goal not a modality"
+ end
+ |first
+ [notypeclasses refine (tac_unlock_emp _ _ _)
+ |notypeclasses refine (tac_unlock_True _ _ _)
+ |iFrame "∗ #"; notypeclasses refine (tac_unlock _ _ _)
+ |fail "iSpecialize: premise cannot be solved by framing"]
+ |exact eq_refl]; iIntro H1; iSpecializePat_go H1 pats
+ end
end.
Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
@@ -1050,20 +1126,30 @@ premises [n], the tactic will have the following behavior:
actual error. *)
Local Ltac iApplyHypExact H :=
first
- [eapply tac_assumption with _ H _ _; (* (i:=H) *)
- [pm_reflexivity || fail 1
- |iSolveTC || fail 1
- |pm_reduce; iSolveTC]
+ [eapply tac_assumption with H; (* (i:=H) *)
+ pm_reduce;
+ lazymatch goal with
+ | |- False => fail 1
+ | _ =>
+ esplit;
+ [iSolveTC || fail 1
+ |pm_reduce; iSolveTC]
+ end
|lazymatch iTypeOf H with
| Some (_,?Q) =>
fail 2 "iApply:" Q "not absorbing and the remaining hypotheses not affine"
end].
Local Ltac iApplyHypLoop H :=
first
- [eapply tac_apply with _ H _ _ _;
- [pm_reflexivity
- |iSolveTC
+ [eapply tac_apply with H _;
+ pm_reduce;
+ lazymatch goal with
+ | |- False => fail
+ | _ =>
+ esplit;
+ [iSolveTC
|pm_prettify (* reduce redexes created by instantiation *)]
+ end
|iSpecializePat H "[]"; last iApplyHypLoop H].
Tactic Notation "iApplyHyp" constr(H) :=