Commit 75c165b2 authored by Robbert Krebbers's avatar Robbert Krebbers

Rename persistent → intuitionistic for proofmode internals/error messages.

parent ae327e1f
......@@ -601,7 +601,7 @@ with the exception of:
- [FromAssumption] used by [iAssumption]
- [Frame] and [MaybeFrame] used by [iFrame]
- [MaybeIntoLaterN] and [FromLaterN] used by [iNext]
- [IntoPersistent] used by [iPersistent]
- [IntoPersistent] used by [iIntuitionistic]
*)
Instance into_pure_tc_opaque {PROP : bi} (P : PROP) φ :
IntoPure P φ IntoPure (tc_opaque P) φ := id.
......
......@@ -135,8 +135,8 @@ Qed.
Lemma tac_pure_revert Δ φ Q : envs_entails Δ (⌜φ⌝ Q) (φ envs_entails Δ Q).
Proof. rewrite envs_entails_eq. intros HΔ ?. by rewrite HΔ pure_True // left_id. Qed.
(** * Persistence *)
Lemma tac_persistent Δ Δ' i p P P' Q :
(** * Intuitionistic *)
Lemma tac_intuitionistic Δ Δ' i p P P' Q :
envs_lookup i Δ = Some (p, P)
IntoPersistent p P P'
(if p then TCTrue else TCOr (Affine P) (Absorbing Q))
......@@ -170,7 +170,7 @@ Proof.
- apply impl_intro_l. rewrite envs_app_singleton_sound //; simpl.
by rewrite -(from_affinely P') persistent_and_affinely_sep_l_1 wand_elim_r.
Qed.
Lemma tac_impl_intro_persistent Δ Δ' i P P' Q R :
Lemma tac_impl_intro_intuitionistic Δ Δ' i P P' Q R :
FromImpl R P Q
IntoPersistent false P P'
envs_app true (Esnoc Enil i P') Δ = Some Δ'
......@@ -195,7 +195,7 @@ Proof.
rewrite /FromWand envs_entails_eq => <- ? HQ.
rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
Qed.
Lemma tac_wand_intro_persistent Δ Δ' i P P' Q R :
Lemma tac_wand_intro_intuitionistic Δ Δ' i P P' Q R :
FromWand R P Q
IntoPersistent false P P'
TCOr (Affine P) (Absorbing Q)
......@@ -234,7 +234,7 @@ Lemma tac_specialize Δ Δ' Δ'' i p j q P1 P2 R Q :
Proof.
rewrite envs_entails_eq. intros [? ->]%envs_lookup_delete_Some Hj ? Hj' <-.
rewrite (envs_lookup_sound' _ false) //; simpl. destruct p; simpl.
- move: Hj; rewrite envs_delete_persistent=> Hj.
- move: Hj; rewrite envs_delete_intuitionistic=> Hj.
rewrite envs_simple_replace_singleton_sound //; simpl.
rewrite -intuitionistically_if_idemp -intuitionistically_idemp into_wand /=.
rewrite assoc (intuitionistically_intuitionistically_if q).
......@@ -296,7 +296,7 @@ Proof.
by rewrite emp_wand wand_elim_r.
Qed.
Lemma tac_specialize_assert_persistent Δ Δ' Δ'' j q P1 P1' P2 R Q :
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
......@@ -315,7 +315,7 @@ Proof.
by rewrite intuitionistically_if_sep_2 into_wand wand_elim_l wand_elim_r.
Qed.
Lemma tac_specialize_persistent_helper Δ Δ'' j q P R R' Q :
Lemma tac_specialize_intuitionistic_helper Δ Δ'' j q P R R' Q :
envs_lookup j Δ = Some (q,P)
envs_entails Δ (<absorb> R)
IntoPersistent false R R'
......@@ -333,7 +333,7 @@ Qed.
(* A special version of [tac_assumption] that does not do any of the
[FromAssumption] magic. *)
Lemma tac_specialize_persistent_helper_done Δ i q P :
Lemma tac_specialize_intuitionistic_helper_done Δ i q P :
envs_lookup i Δ = Some (q,P)
envs_entails Δ (<absorb> P).
Proof.
......@@ -631,8 +631,8 @@ End bi_tactics.
(** The following _private_ classes are used internally by [tac_modal_intro] /
[iModIntro] to transform the proofmode environments when introducing a modality.
The class [TransformPersistentEnv M C Γin Γout] is used to transform the
persistent environment using a type class [C].
The class [TransformIntuitionisticEnv M C Γin Γout] is used to transform the
intuitionistic environment using a type class [C].
Inputs:
- [Γin] : the original environment.
......@@ -643,18 +643,18 @@ Inputs:
Outputs:
- [Γout] : the resulting environment. *)
Class TransformPersistentEnv {PROP1 PROP2} (M : modality PROP1 PROP2)
Class TransformIntuitionisticEnv {PROP1 PROP2} (M : modality PROP1 PROP2)
(C : PROP2 PROP1 Prop) (Γin : env PROP2) (Γout : env PROP1) := {
transform_persistent_env :
transform_intuitionistic_env :
( P Q, C P Q P M ( Q))
( P Q, M P M Q M (P Q))
([] Γin) M ( ([] Γout));
transform_persistent_env_wf : env_wf Γin env_wf Γout;
transform_persistent_env_dom i : Γin !! i = None Γout !! i = None;
transform_intuitionistic_env_wf : env_wf Γin env_wf Γout;
transform_intuitionistic_env_dom i : Γin !! i = None Γout !! i = None;
}.
(* The class [TransformPersistentEnv M C Γin Γout filtered] is used to transform
the persistent environment using a type class [C].
(* The class [TransformIntuitionisticEnv M C Γin Γout filtered] is used to transform
the intuitionistic environment using a type class [C].
Inputs:
- [Γin] : the original environment.
......@@ -676,8 +676,8 @@ Class TransformSpatialEnv {PROP1 PROP2} (M : modality PROP1 PROP2)
transform_spatial_env_dom i : Γin !! i = None Γout !! i = None;
}.
(* The class [IntoModalPersistentEnv M Γin Γout s] is used to transform the
persistent environment with respect to the behavior needed to introduce [M] as
(* The class [IntoModalIntuitionisticEnv M Γin Γout s] is used to transform the
intuitionistic environment with respect to the behavior needed to introduce [M] as
given by [s : modality_intro_spec PROP1 PROP2].
Inputs:
......@@ -688,24 +688,24 @@ Inputs:
Outputs:
- [Γout] : the resulting environment. *)
Inductive IntoModalPersistentEnv {PROP2} : {PROP1} (M : modality PROP1 PROP2)
Inductive IntoModalIntuitionisticEnv {PROP2} : {PROP1} (M : modality PROP1 PROP2)
(Γin : env PROP2) (Γout : env PROP1), modality_action PROP1 PROP2 Prop :=
| MIEnvIsEmpty_persistent {PROP1} (M : modality PROP1 PROP2) :
IntoModalPersistentEnv M Enil Enil MIEnvIsEmpty
| MIEnvForall_persistent (M : modality PROP2 PROP2) (C : PROP2 Prop) Γ :
| MIEnvIsEmpty_intuitionistic {PROP1} (M : modality PROP1 PROP2) :
IntoModalIntuitionisticEnv M Enil Enil MIEnvIsEmpty
| MIEnvForall_intuitionistic (M : modality PROP2 PROP2) (C : PROP2 Prop) Γ :
TCForall C (env_to_list Γ)
IntoModalPersistentEnv M Γ Γ (MIEnvForall C)
| MIEnvTransform_persistent {PROP1}
IntoModalIntuitionisticEnv M Γ Γ (MIEnvForall C)
| MIEnvTransform_intuitionistic {PROP1}
(M : modality PROP1 PROP2) (C : PROP2 PROP1 Prop) Γin Γout :
TransformPersistentEnv M C Γin Γout
IntoModalPersistentEnv M Γin Γout (MIEnvTransform C)
| MIEnvClear_persistent {PROP1 : bi} (M : modality PROP1 PROP2) Γ :
IntoModalPersistentEnv M Γ Enil MIEnvClear
| MIEnvId_persistent (M : modality PROP2 PROP2) Γ :
IntoModalPersistentEnv M Γ Γ MIEnvId.
Existing Class IntoModalPersistentEnv.
Existing Instances MIEnvIsEmpty_persistent MIEnvForall_persistent
MIEnvTransform_persistent MIEnvClear_persistent MIEnvId_persistent.
TransformIntuitionisticEnv M C Γin Γout
IntoModalIntuitionisticEnv M Γin Γout (MIEnvTransform C)
| MIEnvClear_intuitionistic {PROP1 : bi} (M : modality PROP1 PROP2) Γ :
IntoModalIntuitionisticEnv M Γ Enil MIEnvClear
| MIEnvId_intuitionistic (M : modality PROP2 PROP2) Γ :
IntoModalIntuitionisticEnv M Γ Γ MIEnvId.
Existing Class IntoModalIntuitionisticEnv.
Existing Instances MIEnvIsEmpty_intuitionistic MIEnvForall_intuitionistic
MIEnvTransform_intuitionistic MIEnvClear_intuitionistic MIEnvId_intuitionistic.
(* The class [IntoModalSpatialEnv M Γin Γout s] is used to transform the spatial
environment with respect to the behavior needed to introduce [M] as given by
......@@ -742,15 +742,15 @@ Existing Instances MIEnvIsEmpty_spatial MIEnvForall_spatial
Section tac_modal_intro.
Context {PROP1 PROP2 : bi} (M : modality PROP1 PROP2).
Global Instance transform_persistent_env_nil C : TransformPersistentEnv M C Enil Enil.
Global Instance transform_intuitionistic_env_nil C : TransformIntuitionisticEnv M C Enil Enil.
Proof.
split; [|eauto using Enil_wf|done]=> /= ??.
rewrite !intuitionistically_True_emp -modality_emp //.
Qed.
Global Instance transform_persistent_env_snoc (C : PROP2 PROP1 Prop) Γ Γ' i P Q :
Global Instance transform_intuitionistic_env_snoc (C : PROP2 PROP1 Prop) Γ Γ' i P Q :
C P Q
TransformPersistentEnv M C Γ Γ'
TransformPersistentEnv M C (Esnoc Γ i P) (Esnoc Γ' i Q).
TransformIntuitionisticEnv M C Γ Γ'
TransformIntuitionisticEnv M C (Esnoc Γ i P) (Esnoc Γ' i Q).
Proof.
intros ? [HΓ Hwf Hdom]; split; simpl.
- intros HC Hand. rewrite intuitionistically_and HC // HΓ //.
......@@ -758,9 +758,9 @@ Section tac_modal_intro.
- inversion 1; constructor; auto.
- intros j. destruct (ident_beq _ _); naive_solver.
Qed.
Global Instance transform_persistent_env_snoc_not (C : PROP2 PROP1 Prop) Γ Γ' i P :
TransformPersistentEnv M C Γ Γ'
TransformPersistentEnv M C (Esnoc Γ i P) Γ' | 100.
Global Instance transform_intuitionistic_env_snoc_not (C : PROP2 PROP1 Prop) Γ Γ' i P :
TransformIntuitionisticEnv M C Γ Γ'
TransformIntuitionisticEnv M C (Esnoc Γ i P) Γ' | 100.
Proof.
intros [HΓ Hwf Hdom]; split; simpl.
- intros HC Hand. by rewrite and_elim_r HΓ.
......@@ -804,7 +804,7 @@ Section tac_modal_intro.
(** The actual introduction tactic *)
Lemma tac_modal_intro {A} (sel : A) Γp Γs n Γp' Γs' Q Q' fi :
FromModal M sel Q' Q
IntoModalPersistentEnv M Γp Γp' (modality_intuitionistic_action M)
IntoModalIntuitionisticEnv M Γp Γp' (modality_intuitionistic_action M)
IntoModalSpatialEnv M Γs Γs' (modality_spatial_action M) fi
(if fi then Absorbing Q' else TCTrue)
envs_entails (Envs Γp' Γs' n) Q envs_entails (Envs Γp Γs n) Q'.
......@@ -897,8 +897,8 @@ Qed.
(** The class [MaybeIntoLaterNEnvs] is used by tactics that need to introduce
laters, e.g. the symbolic execution tactics. *)
Class MaybeIntoLaterNEnvs (n : nat) (Δ1 Δ2 : envs PROP) := {
into_later_persistent :
TransformPersistentEnv (modality_laterN n) (MaybeIntoLaterN false n)
into_later_intuitionistic :
TransformIntuitionisticEnv (modality_laterN n) (MaybeIntoLaterN false n)
(env_intuitionistic Δ1) (env_intuitionistic Δ2);
into_later_spatial :
TransformSpatialEnv (modality_laterN n)
......@@ -906,7 +906,7 @@ Class MaybeIntoLaterNEnvs (n : nat) (Δ1 Δ2 : envs PROP) := {
}.
Global Instance into_laterN_envs n Γp1 Γp2 Γs1 Γs2 m :
TransformPersistentEnv (modality_laterN n) (MaybeIntoLaterN false n) Γp1 Γp2
TransformIntuitionisticEnv (modality_laterN n) (MaybeIntoLaterN false n) Γp1 Γp2
TransformSpatialEnv (modality_laterN n) (MaybeIntoLaterN false n) Γs1 Γs2 false
MaybeIntoLaterNEnvs n (Envs Γp1 Γs1 m) (Envs Γp2 Γs2 m).
Proof. by split. Qed.
......
......@@ -255,29 +255,29 @@ Definition envs_lookup {PROP} (i : ident) (Δ : envs PROP) : option (bool * PROP
| None => P env_lookup i Γs; Some (false, P)
end.
Definition envs_delete {PROP} (remove_persistent : bool)
Definition envs_delete {PROP} (remove_intuitionistic : bool)
(i : ident) (p : bool) (Δ : envs PROP) : envs PROP :=
let (Γp,Γs,n) := Δ in
match p with
| true => Envs (if remove_persistent then env_delete i Γp else Γp) Γs n
| true => Envs (if remove_intuitionistic then env_delete i Γp else Γp) Γs n
| false => Envs Γp (env_delete i Γs) n
end.
Definition envs_lookup_delete {PROP} (remove_persistent : bool)
Definition envs_lookup_delete {PROP} (remove_intuitionistic : bool)
(i : ident) (Δ : envs PROP) : option (bool * PROP * envs PROP) :=
let (Γp,Γs,n) := Δ in
match env_lookup_delete i Γp with
| Some (P,Γp') => Some (true, P, Envs (if remove_persistent then Γp' else Γp) Γs n)
| Some (P,Γp') => Some (true, P, Envs (if remove_intuitionistic then Γp' else Γp) Γs n)
| None => ''(P,Γs') env_lookup_delete i Γs; Some (false, P, Envs Γp Γs' n)
end.
Fixpoint envs_lookup_delete_list {PROP} (remove_persistent : bool)
Fixpoint envs_lookup_delete_list {PROP} (remove_intuitionistic : bool)
(js : list ident) (Δ : envs PROP) : option (bool * list PROP * envs PROP) :=
match js with
| [] => Some (true, [], Δ)
| j :: js =>
''(p,P,Δ') envs_lookup_delete remove_persistent j Δ;
''(q,Ps,Δ'') envs_lookup_delete_list remove_persistent js Δ';
''(p,P,Δ') envs_lookup_delete remove_intuitionistic j Δ;
''(q,Ps,Δ'') envs_lookup_delete_list remove_intuitionistic js Δ';
Some ((p:bool) && q, P :: Ps, Δ'')
end.
......@@ -313,7 +313,7 @@ Definition env_spatial_is_nil {PROP} (Δ : envs PROP) : bool :=
Definition envs_clear_spatial {PROP} (Δ : envs PROP) : envs PROP :=
Envs (env_intuitionistic Δ) Enil (env_counter Δ).
Definition envs_clear_persistent {PROP} (Δ : envs PROP) : envs PROP :=
Definition envs_clear_intuitionistic {PROP} (Δ : envs PROP) : envs PROP :=
Envs Enil (env_spatial Δ) (env_counter Δ).
Definition envs_incr_counter {PROP} (Δ : envs PROP) : envs PROP :=
......@@ -396,7 +396,7 @@ Global Instance envs_entails_flip_mono :
Proper (envs_Forall2 () ==> flip () ==> flip impl) (@envs_entails PROP).
Proof. rewrite envs_entails_eq=> Δ1 Δ2 ? P1 P2 <- <-. by f_equiv. Qed.
Lemma envs_delete_persistent Δ i : envs_delete false i true Δ = Δ.
Lemma envs_delete_intuitionistic Δ i : envs_delete false i true Δ = Δ.
Proof. by destruct Δ. Qed.
Lemma envs_delete_spatial Δ i :
envs_delete false i false Δ = envs_delete true i false Δ.
......@@ -433,7 +433,7 @@ Lemma envs_lookup_sound Δ i p P :
envs_lookup i Δ = Some (p,P)
of_envs Δ ?p P of_envs (envs_delete true i p Δ).
Proof. apply envs_lookup_sound'. Qed.
Lemma envs_lookup_persistent_sound Δ i P :
Lemma envs_lookup_intuitionistic_sound Δ i P :
envs_lookup i Δ = Some (true,P) of_envs Δ P of_envs Δ.
Proof. intros ?%(envs_lookup_sound' _ false). by destruct Δ. Qed.
Lemma envs_lookup_sound_2 Δ i p P :
......
......@@ -100,11 +100,11 @@ with parse_clear (ts : list token) (k : stack) : option stack :=
match ts with
| TFrame :: TName s :: ts => parse_clear ts (StPat (IClearFrame (SelIdent s)) :: k)
| TFrame :: TPure :: ts => parse_clear ts (StPat (IClearFrame SelPure) :: k)
| TFrame :: TAlways :: ts => parse_clear ts (StPat (IClearFrame SelPersistent) :: k)
| TFrame :: TAlways :: ts => parse_clear ts (StPat (IClearFrame SelIntuitionistic) :: k)
| TFrame :: TSep :: ts => parse_clear ts (StPat (IClearFrame SelSpatial) :: k)
| TName s :: ts => parse_clear ts (StPat (IClear (SelIdent s)) :: k)
| TPure :: ts => parse_clear ts (StPat (IClear SelPure) :: k)
| TAlways :: ts => parse_clear ts (StPat (IClear SelPersistent) :: k)
| TAlways :: ts => parse_clear ts (StPat (IClear SelIntuitionistic) :: k)
| TSep :: ts => parse_clear ts (StPat (IClear SelSpatial) :: k)
| TBraceR :: ts => parse_go ts k
| _ => None
......@@ -148,25 +148,25 @@ Ltac parse_one s :=
end.
End intro_pat.
Fixpoint intro_pat_persistent (p : intro_pat) :=
Fixpoint intro_pat_intuitionistic (p : intro_pat) :=
match p with
| IPureElim => true
| IAlwaysElim _ => true
| IList pps => forallb (forallb intro_pat_persistent) pps
| IList pps => forallb (forallb intro_pat_intuitionistic) pps
| ISimpl => true
| IClear _ => true
| IClearFrame _ => true
| _ => false
end.
Ltac intro_pat_persistent p :=
Ltac intro_pat_intuitionistic p :=
lazymatch type of p with
| intro_pat => eval cbv in (intro_pat_persistent p)
| list intro_pat => eval cbv in (forallb intro_pat_persistent p)
| intro_pat => eval cbv in (intro_pat_intuitionistic p)
| list intro_pat => eval cbv in (forallb intro_pat_intuitionistic p)
| string =>
let pat := intro_pat.parse p in
eval cbv in (forallb intro_pat_persistent pat)
eval cbv in (forallb intro_pat_intuitionistic pat)
| ident => false
| bool => p
| ?X => fail "intro_pat_persistent:" p "has unexpected type" X
| ?X => fail "intro_pat_intuitionistic:" p "has unexpected type" X
end.
......@@ -148,9 +148,9 @@ Local Ltac iElaborateSelPat_go pat Δ Hs :=
lazymatch pat with
| [] => eval cbv in Hs
| SelPure :: ?pat => iElaborateSelPat_go pat Δ (ESelPure :: Hs)
| SelPersistent :: ?pat =>
| SelIntuitionistic :: ?pat =>
let Hs' := pm_eval (env_dom (env_intuitionistic Δ)) in
let Δ' := pm_eval (envs_clear_persistent Δ) in
let Δ' := pm_eval (envs_clear_intuitionistic Δ) in
iElaborateSelPat_go pat Δ' ((ESelIdent true <$> Hs') ++ Hs)
| SelSpatial :: ?pat =>
let Hs' := pm_eval (env_dom (env_spatial Δ)) in
......@@ -249,18 +249,18 @@ Tactic Notation "iAssumption" :=
(** * False *)
Tactic Notation "iExFalso" := apply tac_ex_falso.
(** * Making hypotheses persistent or pure *)
Local Tactic Notation "iPersistent" constr(H) :=
eapply tac_persistent with _ H _ _ _; (* (i:=H) *)
(** * Making hypotheses intuitionistic or pure *)
Local Tactic Notation "iIntuitionistic" constr(H) :=
eapply tac_intuitionistic with _ H _ _ _; (* (i:=H) *)
[pm_reflexivity ||
let H := pretty_ident H in
fail "iPersistent:" H "not found"
fail "iIntuitionistic:" H "not found"
|iSolveTC ||
let P := match goal with |- IntoPersistent _ ?P _ => P end in
fail "iPersistent:" P "not persistent"
fail "iIntuitionistic:" P "not persistent"
|pm_reduce; iSolveTC ||
let P := match goal with |- TCOr (Affine ?P) _ => P end in
fail "iPersistent:" P "not affine and the goal not absorbing"
fail "iIntuitionistic:" P "not affine and the goal not absorbing"
|pm_reflexivity|].
Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
......@@ -320,7 +320,7 @@ Local Ltac iFrameHyp H :=
Local Ltac iFrameAnyPure :=
repeat match goal with H : _ |- _ => iFramePure H end.
Local Ltac iFrameAnyPersistent :=
Local Ltac iFrameAnyIntuitionistic :=
iStartProof;
let rec go Hs :=
match Hs with [] => idtac | ?H :: ?Hs => repeat iFrameHyp H; go Hs end in
......@@ -365,7 +365,7 @@ Local Ltac iFrame_go Hs :=
lazymatch Hs with
| [] => idtac
| SelPure :: ?Hs => iFrameAnyPure; iFrame_go Hs
| SelPersistent :: ?Hs => iFrameAnyPersistent; iFrame_go Hs
| SelIntuitionistic :: ?Hs => iFrameAnyIntuitionistic; iFrame_go Hs
| SelSpatial :: ?Hs => iFrameAnySpatial; iFrame_go Hs
| SelIdent ?H :: ?Hs => iFrameHyp H; iFrame_go Hs
end.
......@@ -446,7 +446,7 @@ Local Tactic Notation "iIntro" "#" constr(H) :=
iStartProof;
first
[(* (?P → _) *)
eapply tac_impl_intro_persistent with _ H _ _ _; (* (i:=H) *)
eapply tac_impl_intro_intuitionistic with _ H _ _ _; (* (i:=H) *)
[iSolveTC
|iSolveTC ||
let P := match goal with |- IntoPersistent _ ?P _ => P end in
......@@ -456,11 +456,11 @@ Local Tactic Notation "iIntro" "#" constr(H) :=
fail 1 "iIntro:" H "not fresh"
|(* subgoal *)]
|(* (?P -∗ _) *)
eapply tac_wand_intro_persistent with _ H _ _ _; (* (i:=H) *)
eapply tac_wand_intro_intuitionistic with _ H _ _ _; (* (i:=H) *)
[iSolveTC
|iSolveTC ||
let P := match goal with |- IntoPersistent _ ?P _ => P end in
fail 1 "iIntro:" P "not persistent"
fail 1 "iIntro:" P "not intuitionistic"
|iSolveTC ||
let P := match goal with |- TCOr (Affine ?P) _ => P end in
fail 1 "iIntro:" P "not affine and the goal not absorbing"
......@@ -665,8 +665,8 @@ Ltac iSpecializePat_go H1 pats :=
|pm_reflexivity
|solve_done d (*goal*)
|iSpecializePat_go H1 pats]
| SGoal (SpecGoal GPersistent false ?Hs_frame [] ?d) :: ?pats =>
notypeclasses refine (tac_specialize_assert_persistent _ _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _ _);
| 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"
......@@ -678,8 +678,8 @@ Ltac iSpecializePat_go H1 pats :=
|pm_reflexivity
|iFrame Hs_frame; solve_done d (*goal*)
|iSpecializePat_go H1 pats]
| SGoal (SpecGoal GPersistent _ _ _ _) :: ?pats =>
fail "iSpecialize: cannot select hypotheses for persistent premise"
| 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' _ _ _ _ _ _ _ _ _ _ _);
......@@ -696,8 +696,8 @@ Ltac iSpecializePat_go H1 pats :=
fail "iSpecialize: hypotheses" Hs' "not found"
|iFrame Hs_frame; solve_done d (*goal*)
|iSpecializePat_go H1 pats]
| SAutoFrame GPersistent :: ?pats =>
notypeclasses refine (tac_specialize_assert_persistent _ _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _ _);
| SAutoFrame GIntuitionistic :: ?pats =>
notypeclasses refine (tac_specialize_assert_intuitionistic _ _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _ _);
[pm_reflexivity ||
let H1 := pretty_ident H1 in
fail "iSpecialize:" H1 "not found"
......@@ -730,7 +730,7 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
let pats := spec_pat.parse pat in iSpecializePat_go H pats.
(* The argument [p] denotes whether the conclusion of the specialized term is
persistent. If so, one can use all spatial hypotheses for both proving the
intuitionistic. If so, one can use all spatial hypotheses for both proving the
premises and the remaning goal. The argument [p] can either be a Boolean or an
introduction pattern, which will be coerced into [true] when it solely contains
`#` or `%` patterns at the top-level.
......@@ -740,7 +740,7 @@ should be kept for one of the premises (i.e. [>[H1 .. Hn]] is used) then [p]
defaults to [false] (i.e. spatial hypotheses are not preserved). *)
Tactic Notation "iSpecializeCore" open_constr(H)
"with" open_constr(xs) open_constr(pat) "as" constr(p) :=
let p := intro_pat_persistent p in
let p := intro_pat_intuitionistic p in
let pat := spec_pat.parse pat in
let H :=
lazymatch type of H with
......@@ -750,11 +750,11 @@ Tactic Notation "iSpecializeCore" open_constr(H)
iSpecializeArgs H xs; [..|
lazymatch type of H with
| ident =>
(* The lemma [tac_specialize_persistent_helper] allows one to use all
(* The lemma [tac_specialize_intuitionistic_helper] allows one to use all
spatial hypotheses for both proving the premises of the lemma we
specialize as well as those of the remaining goal. We can only use it when
the result of the specialization is persistent, and no modality is
eliminated. We do not use [tac_specialize_persistent_helper] in the case
the result of the specialization is intuitionistic, and no modality is
eliminated. We do not use [tac_specialize_intuitionistic_helper] in the case
only universal quantifiers and no implications or wands are instantiated
(i.e [pat = []]) because it is a.) not needed, and b.) more efficient. *)
let pat := spec_pat.parse pat in
......@@ -762,13 +762,13 @@ Tactic Notation "iSpecializeCore" open_constr(H)
(p && bool_decide (pat []) && negb (existsb spec_pat_modal pat)) with
| true =>
(* FIXME: do something reasonable when the BI is not affine *)
notypeclasses refine (tac_specialize_persistent_helper _ _ H _ _ _ _ _ _ _ _ _ _ _);
notypeclasses refine (tac_specialize_intuitionistic_helper _ _ H _ _ _ _ _ _ _ _ _ _ _);
[pm_reflexivity ||
let H := pretty_ident H in
fail "iSpecialize:" H "not found"
|iSpecializePat H pat;
[..
|notypeclasses refine (tac_specialize_persistent_helper_done _ H _ _ _);
|notypeclasses refine (tac_specialize_intuitionistic_helper_done _ H _ _ _);
pm_reflexivity]
|iSolveTC ||
let Q := match goal with |- IntoPersistent _ ?Q _ => Q end in
......@@ -1112,10 +1112,10 @@ Tactic Notation "iModIntro" uconstr(sel) :=
[iSolveTC ||
fail "iModIntro: the goal is not a modality"
|iSolveTC ||
let s := lazymatch goal with |- IntoModalPersistentEnv _ _ _ ?s => s end in
let s := lazymatch goal with |- IntoModalIntuitionisticEnv _ _ _ ?s => s end in
lazymatch eval hnf in s with
| MIEnvForall ?C => fail "iModIntro: persistent context does not satisfy" C
| MIEnvIsEmpty => fail "iModIntro: persistent context is non-empty"
| MIEnvForall ?C => fail "iModIntro: intuitionistic context does not satisfy" C
| MIEnvIsEmpty => fail "iModIntro: intuitionistic context is non-empty"
end
|iSolveTC ||
let s := lazymatch goal with |- IntoModalSpatialEnv _ _ _ ?s _ => s end in
......@@ -1166,7 +1166,7 @@ Local Ltac iDestructHypGo Hz pat :=
| IPureElim => iPure Hz as ?
| IRewrite Right => iPure Hz as ->
| IRewrite Left => iPure Hz as <-
| IAlwaysElim ?pat => iPersistent Hz; iDestructHypGo Hz pat
| IAlwaysElim ?pat => iIntuitionistic Hz; iDestructHypGo Hz pat
| IModalElim ?pat => iModCore Hz; iDestructHypGo Hz pat
| _ => fail "iDestruct:" pat "invalid"
end.
......@@ -1590,7 +1590,7 @@ Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) :=
| _ =>
(* Only copy the hypothesis in case there is a [CopyDestruct] instance.
Also, rule out cases in which it does not make sense to copy, namely when
destructing a lemma (instead of a hypothesis) or a spatial hyopthesis
destructing a lemma (instead of a hypothesis) or a spatial hypothesis
(which cannot be kept). *)
iStartProof;
lazymatch ident with
......@@ -1601,7 +1601,7 @@ Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) :=
let H := pretty_ident H in
fail "iDestruct:" H "not found"
| Some (true, ?P) =>
(* persistent hypothesis, check for a CopyDestruct instance *)
(* intuitionistic hypothesis, check for a CopyDestruct instance *)
tryif (let dummy := constr:(_ : CopyDestruct P) in idtac)
then (iPoseProofCore lem as p false tac)
else (iSpecializeCore lem as p; [..| tac H])
......@@ -1688,14 +1688,14 @@ Tactic Notation "iPoseProof" open_constr(lem) "as" "(" simple_intropattern(x1)
result in the following actions:
- Revert the proofmode hypotheses [Hs]
- Revert all remaining spatial hypotheses and the remaining persistent
- Revert all remaining spatial hypotheses and the remaining intuitionistic
hypotheses containing the induction variable [x]
- Revert the pure hypotheses [x1..xn]
- Actuall perform induction
- Introduce thee pure hypotheses [x1..xn]
- Introduce the spatial hypotheses and persistent hypotheses involving [x]
- Introduce the spatial hypotheses and intuitionistic hypotheses involving [x]
- Introduce the proofmode hypotheses [Hs]
*)
Tactic Notation "iInductionCore" tactic(tac) "as" constr(IH) :=
......@@ -1982,7 +1982,7 @@ Tactic Notation "iAssertCore" open_constr(Q)
|iSpecializeCore H with hnil pats as p; [..|tac H]].
Tactic Notation "iAssertCore" open_constr(Q) "as" constr(p) tactic(tac) :=
let p := intro_pat_persistent p in
let p := intro_pat_intuitionistic p in
lazymatch p with
| true => iAssertCore Q with "[#]" as p tac
| false => iAssertCore Q with "[]" as p tac
......