Commit 2d209fea authored by Joseph Tassarotti's avatar Joseph Tassarotti

More stylistic fixes.

parent 472e32c9
......@@ -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 done.
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.
......@@ -217,10 +217,9 @@ Lemma tac_wand_intro Δ i P Q R :
end
envs_entails Δ R.
Proof.
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.
destruct (envs_app _ _ _) as [Δ'|] eqn:Hrep; last done.
rewrite /FromWand envs_entails_eq => <- HQ.
rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
Qed.
Lemma tac_wand_intro_intuitionistic Δ i P P' Q R :
......@@ -512,11 +511,10 @@ Lemma tac_and_destruct Δ i p j1 j2 P P1 P2 Q :
end
envs_entails Δ Q.
Proof.
destruct (envs_simple_replace) as [Δ'|] eqn:Hrep.
- rewrite envs_entails_eq. intros. rewrite envs_simple_replace_sound //=. destruct p.
* by rewrite (into_and _ P) /= right_id -(comm _ P1) wand_elim_r.
* by rewrite /= (into_sep P) right_id -(comm _ P1) wand_elim_r.
- intros; by exfalso.
destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
rewrite envs_entails_eq. intros. rewrite envs_simple_replace_sound //=. destruct p.
- by rewrite (into_and _ P) /= right_id -(comm _ P1) wand_elim_r.
- by rewrite /= (into_sep P) right_id -(comm _ P1) wand_elim_r.
Qed.
(* Using this tactic, one can destruct a (non-separating) conjunction in the
......@@ -587,8 +585,8 @@ Lemma tac_or_destruct Δ i p j1 j2 P P1 P2 Q :
end
envs_entails Δ Q.
Proof.
destruct (envs_simple_replace i p (Esnoc Enil j1 P1)) as [Δ1|] eqn:?; [| by intros; exfalso].
destruct (envs_simple_replace i p (Esnoc Enil j2 P2)) as [Δ2|] eqn:?; [| by intros; exfalso].
destruct (envs_simple_replace i p (Esnoc Enil j1 P1)) as [Δ1|] eqn:?; last done.
destruct (envs_simple_replace i p (Esnoc Enil j2 P2)) as [Δ2|] eqn:?; last done.
rewrite envs_entails_eq. intros ?? (HP1&HP2). rewrite envs_lookup_sound //.
rewrite (into_or P) intuitionistically_if_or sep_or_r; apply or_elim.
- rewrite (envs_simple_replace_singleton_sound' _ Δ1) //.
......@@ -614,7 +612,7 @@ Lemma tac_forall_specialize {A} Δ i p P (Φ : A → PROP) Q :
envs_entails Δ Q.
Proof.
rewrite envs_entails_eq. intros ?? (x&?).
destruct (envs_simple_replace) as [Δ'|] eqn:?; [| by exfalso].
destruct (envs_simple_replace) as [Δ'|] eqn:?; last done.
rewrite envs_simple_replace_singleton_sound //; simpl.
by rewrite (into_forall P) (forall_elim x) wand_elim_r.
Qed.
......@@ -955,7 +953,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 done. 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.
......
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