Commit 7f12ce11 authored by Joseph Tassarotti's avatar Joseph Tassarotti

Fix style issues in compact IPM changes.

parent 1d8edc89
......@@ -37,7 +37,7 @@ Lemma tac_eval_in Δ i p P P' Q :
end
envs_entails Δ Q.
Proof.
destruct (envs_simple_replace) as [Δ'|] eqn:Hrep; last (intros; by exfalso).
destruct (envs_simple_replace _ _ _) as [Δ'|] eqn:Hrep; last done.
rewrite envs_entails_eq /=. intros ? HP ?.
rewrite envs_simple_replace_singleton_sound //; simpl.
by rewrite HP wand_elim_r.
......@@ -83,10 +83,9 @@ Lemma tac_rename Δ i j p P Q :
end
envs_entails Δ Q.
Proof.
destruct (envs_simple_replace) as [Δ'|] eqn:Hrep.
- rewrite envs_entails_eq=> ??. rewrite envs_simple_replace_singleton_sound //.
by rewrite wand_elim_r.
- intros; by exfalso.
destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
rewrite envs_entails_eq=> ??. rewrite envs_simple_replace_singleton_sound //.
by rewrite wand_elim_r.
Qed.
(* TODO: convert to not take Δ' *)
......@@ -157,7 +156,7 @@ Lemma tac_intuitionistic Δ i p P P' Q :
end
envs_entails Δ Q.
Proof.
destruct (envs_replace) as [Δ'|] eqn:Hrep; last by (intros; exfalso).
destruct (envs_replace _ _ _ _ _) as [Δ'|] eqn:Hrep; last done.
rewrite envs_entails_eq=>?? HPQ HQ. rewrite envs_replace_singleton_sound //=.
destruct p; simpl; rewrite /bi_intuitionistically.
- by rewrite -(into_persistent true P) /= wand_elim_r.
......@@ -180,7 +179,7 @@ Lemma tac_impl_intro Δ i P P' Q R :
end
envs_entails Δ R.
Proof.
destruct (envs_app) eqn:?; last by (intros; exfalso).
destruct (envs_app _ _ _) eqn:?; last done.
rewrite /FromImpl envs_entails_eq => <- ???. destruct (env_spatial_is_nil Δ) eqn:?.
- rewrite (env_spatial_is_nil_intuitionistically Δ) //; simpl. apply impl_intro_l.
rewrite envs_app_singleton_sound //; simpl.
......@@ -198,7 +197,7 @@ Lemma tac_impl_intro_intuitionistic Δ i P P' Q R :
end
envs_entails Δ R.
Proof.
destruct (envs_app) eqn:?; last by (intros; exfalso).
destruct (envs_app _ _ _) eqn:?; last done.
rewrite /FromImpl envs_entails_eq => <- ??.
rewrite envs_app_singleton_sound //=. apply impl_intro_l.
rewrite (_ : P = <pers>?false P)%I // (into_persistent false P).
......@@ -212,13 +211,13 @@ Qed.
Lemma tac_wand_intro Δ i P Q R :
FromWand R P Q
(match envs_app false (Esnoc Enil i P) Δ with
match envs_app false (Esnoc Enil i P) Δ with
| None => False
| Some Δ' => envs_entails Δ' Q
end)
| Some Δ' => envs_entails Δ' Q
end
envs_entails Δ R.
Proof.
destruct (envs_app) as [Δ'|] eqn:Hrep.
destruct (envs_app _ _ _) as [Δ'|] eqn:Hrep.
- rewrite /FromWand envs_entails_eq => <- HQ.
rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
- intros; by exfalso.
......@@ -234,7 +233,7 @@ Lemma tac_wand_intro_intuitionistic Δ i P P' Q R :
end
envs_entails Δ R.
Proof.
destruct (envs_app) as [Δ'|] eqn:Hrep; last by (intros; exfalso).
destruct (envs_app _ _ _) as [Δ'|] eqn:Hrep; last done.
rewrite /FromWand envs_entails_eq => <- ? HPQ HQ.
rewrite envs_app_singleton_sound //=. apply wand_intro_l. destruct HPQ.
- rewrite -(affine_affinely P) (_ : P = <pers>?false P)%I //
......@@ -321,7 +320,7 @@ Lemma tac_specialize_assert_pure Δ j q a R P1 P2 φ Q :
end
envs_entails Δ Q.
Proof.
destruct envs_simple_replace as [Δ'|] eqn:?; last by (intros; exfalso).
destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:?; last done.
rewrite envs_entails_eq=> ?????. rewrite envs_simple_replace_singleton_sound //=.
rewrite -intuitionistically_if_idemp (into_wand q true) /=.
rewrite -(from_pure a P1) pure_True //.
......@@ -414,7 +413,7 @@ Lemma tac_assert Δ j P Q :
| Some Δ' => envs_entails Δ' Q
end envs_entails Δ Q.
Proof.
destruct (envs_app) as [Δ'|] eqn:?; last by (intros; exfalso).
destruct (envs_app _ _ _) as [Δ'|] eqn:?; last done.
rewrite envs_entails_eq=> ?. rewrite (envs_app_singleton_sound Δ) //; simpl.
by rewrite -(entails_wand P) // intuitionistically_emp emp_wand.
Qed.
......@@ -427,7 +426,7 @@ Lemma tac_pose_proof Δ j P Q :
end
envs_entails Δ Q.
Proof.
destruct (envs_app) as [Δ'|] eqn:?; last by (intros; exfalso).
destruct (envs_app _ _ _) as [Δ'|] eqn:?; last done.
rewrite envs_entails_eq => HP ?. rewrite envs_app_singleton_sound //=.
by rewrite -HP /= intuitionistically_emp emp_wand.
Qed.
......@@ -443,8 +442,8 @@ Lemma tac_pose_proof_hyp Δ i j Q :
end
envs_entails Δ Q.
Proof.
destruct envs_lookup_delete as [((p&P)&Δ')|] eqn:Hlookup; last by (intros; exfalso).
destruct (envs_app) as [Δ''|] eqn:?; last by (intros; exfalso).
destruct (envs_lookup_delete _ _ _) as [((p&P)&Δ')|] eqn:Hlookup; last done.
destruct (envs_app _ _ _) as [Δ''|] eqn:?; last done.
rewrite envs_entails_eq. rewrite envs_lookup_delete_Some in Hlookup *.
intros [? ->] <-.
rewrite envs_lookup_sound' // envs_app_singleton_sound //=.
......@@ -473,7 +472,7 @@ Lemma tac_sep_split Δ d js P Q1 Q2 :
| Some (Δ1,Δ2) => envs_entails Δ1 Q1 envs_entails Δ2 Q2
end envs_entails Δ P.
Proof.
destruct (envs_split) as [(Δ1&Δ2)|] eqn:?; last by (intros; exfalso).
destruct (envs_split _ _ _) as [(Δ1&Δ2)|] eqn:?; last done.
rewrite envs_entails_eq=>? [HQ1 HQ2].
rewrite envs_split_sound //. by rewrite HQ1 HQ2.
Qed.
......@@ -534,7 +533,7 @@ Lemma tac_and_destruct_choice Δ i p d j P P1 P2 Q :
| Some Δ' => envs_entails Δ' Q
end envs_entails Δ Q.
Proof.
destruct (envs_simple_replace) as [Δ'|] eqn:Hrep; last by (intros; exfalso).
destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
rewrite envs_entails_eq => ? HP HQ.
rewrite envs_simple_replace_singleton_sound //=. destruct p.
{ rewrite (into_and _ P) HQ. destruct d; simpl.
......@@ -656,7 +655,7 @@ Lemma tac_modal_elim Δ i p p' φ P' P Q Q' :
end
envs_entails Δ Q.
Proof.
destruct (envs_replace) as [Δ'|] eqn:?; last by (intros; exfalso).
destruct (envs_replace _ _ _ _ _) as [Δ'|] eqn:?; last done.
rewrite envs_entails_eq => ??? HΔ. rewrite envs_replace_singleton_sound //=.
rewrite HΔ. by eapply elim_modal.
Qed.
......@@ -956,7 +955,7 @@ Lemma tac_rewrite_in Δ i p Pxy j q P d Q :
envs_entails Δ Q.
Proof.
rewrite envs_entails_eq /IntoInternalEq => ?? A x y Φ HPxy HP ? Hentails.
destruct (envs_simple_replace) as [Δ'|] eqn:?; last by exfalso. rewrite -Hentails.
destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:?; last by exfalso. rewrite -Hentails.
rewrite -(idemp bi_and (of_envs Δ)) {2}(envs_lookup_sound _ i) //.
rewrite (envs_simple_replace_singleton_sound _ _ j) //=.
rewrite HP HPxy (intuitionistically_if_elim _ (_ _)%I) sep_elim_l.
......@@ -1005,7 +1004,7 @@ Lemma tac_löb Δ i Q :
end
envs_entails Δ Q.
Proof.
destruct (envs_app) eqn:?; last by (intros; exfalso).
destruct (envs_app _ _ _) eqn:?; last done.
rewrite envs_entails_eq => ? HQ.
rewrite (env_spatial_is_nil_intuitionistically Δ) //.
rewrite -(persistently_and_emp_elim Q). apply and_intro; first apply: affine.
......
......@@ -133,7 +133,7 @@ Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
| |- False =>
let H2 := pretty_ident H2 in
fail "iRename:" H2 "not fresh"
| _ => idtac (* subogal *)
| _ => idtac (* subgoal *)
end].
(** Elaborated selection patterns, unlike the type [sel_pat], contains
......@@ -717,7 +717,7 @@ Tactic Notation "iPoseProofCoreHyp" constr(H) "as" constr(Hnew) :=
pm_reduce;
lazymatch goal with
| |- False =>
let Htmp := pretty_ident Hnew in
let Hnew := pretty_ident Hnew in
fail "iPoseProof:" Hnew "not fresh"
| _ => idtac
end
......@@ -729,7 +729,7 @@ Tactic Notation "iPoseProofCoreLem"
[iIntoEmpValid lem
|pm_reduce;
lazymatch goal with
|- False =>
| |- False =>
let Htmp := pretty_ident Hnew in
fail "iPoseProof:" Hnew "not fresh"
| _ => tac
......@@ -1104,13 +1104,13 @@ Local Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
fail "iOrDestruct: cannot destruct" P
| pm_reduce; split;
[ lazymatch goal with
|- False =>
| |- False =>
let H1 := pretty_ident H1 in
fail "iOrDestruct:" H1 "not fresh"
| _ => idtac (* subgoal 1 *)
end
| lazymatch goal with
|- False =>
| |- False =>
let H1 := pretty_ident H1 in
fail "iOrDestruct:" H1 "not fresh"
| _ => idtac (* subgoal 2 *)
......@@ -1137,7 +1137,7 @@ Tactic Notation "iSplitL" constr(Hs) :=
fail "iSplitL:" P "not a separating conjunction"
|pm_reduce;
lazymatch goal with
|- False => let Hs := iMissingHypsCore Δ Hs in
| |- False => let Hs := iMissingHypsCore Δ Hs in
fail "iSplitL: hypotheses" Hs "not found"
| _ => split; [(* subgoal 1 *)|(* subgoal 2 *)]
end].
......@@ -1153,7 +1153,7 @@ Tactic Notation "iSplitR" constr(Hs) :=
fail "iSplitR:" P "not a separating conjunction"
|pm_reduce;
lazymatch goal with
|- False => let Hs := iMissingHypsCore Δ Hs in
| |- False => let Hs := iMissingHypsCore Δ Hs in
fail "iSplitR: hypotheses" Hs "not found"
| _ => split; [(* subgoal 1 *)|(* subgoal 2 *)]
end].
......
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