Commit 8fd8da22 authored by Robbert Krebbers's avatar Robbert Krebbers

Rename pure_equiv -> pure_True.

The old name didn't make much sense. Also now we can have
pure_False too.
parent 863f30c0
......@@ -260,7 +260,7 @@ Section list.
revert Φ HΦ. induction l as [|x l IH]=> Φ HΦ.
{ rewrite big_sepL_nil; auto with I. }
rewrite big_sepL_cons. rewrite -always_and_sep_l; apply and_intro.
- by rewrite (forall_elim 0) (forall_elim x) pure_equiv // True_impl.
- by rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
- rewrite -IH. apply forall_intro=> k; by rewrite (forall_elim (S k)).
Qed.
......@@ -384,11 +384,11 @@ Section gmap.
induction m as [|i x m ? IH] using map_ind; [rewrite ?big_sepM_empty; auto|].
rewrite big_sepM_insert // -always_and_sep_l. apply and_intro.
- rewrite (forall_elim i) (forall_elim x) lookup_insert.
by rewrite pure_equiv // True_impl.
by rewrite pure_True // True_impl.
- rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
apply impl_intro_l, pure_elim_l=> ?.
rewrite lookup_insert_ne; last by intros ?; simplify_map_eq.
by rewrite pure_equiv // True_impl.
by rewrite pure_True // True_impl.
Qed.
Lemma big_sepM_impl Φ Ψ m :
......@@ -492,12 +492,12 @@ Section gset.
intros. apply (anti_symm _).
{ apply forall_intro=> x.
apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. }
induction X as [|x m ? IH] using collection_ind_L.
induction X as [|x X ? IH] using collection_ind_L.
{ rewrite big_sepS_empty; auto. }
rewrite big_sepS_insert // -always_and_sep_l. apply and_intro.
- by rewrite (forall_elim x) pure_equiv ?True_impl; last set_solver.
- by rewrite (forall_elim x) pure_True ?True_impl; last set_solver.
- rewrite -IH. apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
by rewrite pure_equiv ?True_impl; last set_solver.
by rewrite pure_True ?True_impl; last set_solver.
Qed.
Lemma big_sepS_impl Φ Ψ X :
......
......@@ -163,6 +163,11 @@ Proof.
- by rewrite -(left_id True%I uPred_and (_ _)%I) impl_elim_r.
- by apply impl_intro_l; rewrite left_id.
Qed.
Lemma False_impl P : (False P) True.
Proof.
apply (anti_symm ()); [by auto|].
apply impl_intro_l. rewrite left_absorb. auto.
Qed.
Lemma exists_impl_forall {A} P (Ψ : A uPred M) :
(( x : A, Ψ x) P) x : A, Ψ x P.
......@@ -223,8 +228,11 @@ Lemma pure_elim_l φ Q R : (φ → Q ⊢ R) → ■ φ ∧ Q ⊢ R.
Proof. intros; apply pure_elim with φ; eauto. Qed.
Lemma pure_elim_r φ Q R : (φ Q R) Q φ R.
Proof. intros; apply pure_elim with φ; eauto. Qed.
Lemma pure_equiv (φ : Prop) : φ φ True.
Lemma pure_True (φ : Prop) : φ φ True.
Proof. intros; apply (anti_symm _); auto. Qed.
Lemma pure_False (φ : Prop) : ¬φ φ False.
Proof. intros; apply (anti_symm _); eauto using pure_elim. Qed.
Lemma pure_and φ1 φ2 : (φ1 φ2) φ1 φ2.
Proof.
......@@ -243,7 +251,7 @@ Proof.
apply (anti_symm _).
- apply impl_intro_l. rewrite -pure_and. apply pure_mono. naive_solver.
- rewrite -pure_forall_2. apply forall_intro=> ?.
by rewrite -(left_id True uPred_and (_→_))%I (pure_equiv φ1) // impl_elim_r.
by rewrite -(left_id True uPred_and (_→_))%I (pure_True φ1) // impl_elim_r.
Qed.
Lemma pure_forall {A} (φ : A Prop) : ( x, φ x) x, φ x.
Proof.
......@@ -268,7 +276,7 @@ Proof. apply (internal_eq_rewrite a b (λ b, b ≡ a)%I); auto. solve_proper. Qe
Lemma pure_impl_forall φ P : ( φ P) ( _ : φ, P).
Proof.
apply (anti_symm _).
- apply forall_intro=> ?. by rewrite pure_equiv // left_id.
- apply forall_intro=> ?. by rewrite pure_True // left_id.
- apply impl_intro_l, pure_elim_l=> Hφ. by rewrite (forall_elim Hφ).
Qed.
Lemma pure_alt φ : φ _ : φ, True.
......
......@@ -95,7 +95,7 @@ Proof.
first (eapply alloc_updateP_strong', cmra_transport_valid, Ha);
naive_solver.
- apply exist_elim=>m; apply pure_elim_l=>-[γ [Hfresh ->]].
by rewrite !own_eq /own_def -(exist_intro γ) pure_equiv // left_id.
by rewrite !own_eq /own_def -(exist_intro γ) pure_True // left_id.
Qed.
Lemma own_alloc a : a True == γ, own γ a.
Proof.
......
......@@ -88,7 +88,7 @@ Section heap.
l {q1} v1 l {q2} v2 v1 = v2 l {q1+q2} v1.
Proof.
destruct (decide (v1 = v2)) as [->|].
{ by rewrite heap_mapsto_op_eq pure_equiv // left_id. }
{ by rewrite heap_mapsto_op_eq pure_True // left_id. }
apply (anti_symm ()); last by apply pure_elim_l.
rewrite heap_mapsto_eq -auth_own_op auth_own_valid discrete_valid.
eapply pure_elim; [done|] => /=.
......
......@@ -152,10 +152,10 @@ Proof.
rewrite /envs_lookup /of_envs=>?; apply pure_elim_sep_l=> Hwf.
destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
- rewrite (env_lookup_perm Γp) //= always_sep.
rewrite pure_equiv // left_id.
rewrite pure_True // left_id.
cancel [ P]%I. apply wand_intro_l. solve_sep_entails.
- destruct (Γs !! i) eqn:?; simplify_eq/=.
rewrite (env_lookup_perm Γs) //=. rewrite pure_equiv // left_id.
rewrite (env_lookup_perm Γs) //=. rewrite pure_True // left_id.
cancel [P]. apply wand_intro_l. solve_sep_entails.
Qed.
......@@ -398,7 +398,7 @@ Proof.
Qed.
Lemma tac_pure_revert Δ φ Q : (Δ φ Q) (φ Δ Q).
Proof. intros HΔ ?. by rewrite HΔ pure_equiv // left_id. Qed.
Proof. intros HΔ ?. by rewrite HΔ pure_True // left_id. Qed.
(** * Later *)
Class IntoLaterEnv (Γ1 Γ2 : env (uPred M)) :=
......@@ -548,7 +548,7 @@ Lemma tac_specialize_assert_pure Δ Δ' j q R P1 P2 φ Q :
φ (Δ' Q) Δ Q.
Proof.
intros. rewrite envs_simple_replace_sound //; simpl.
rewrite right_id (into_wand R) -(from_pure P1) pure_equiv //.
rewrite right_id (into_wand R) -(from_pure P1) pure_True //.
by rewrite wand_True wand_elim_r.
Qed.
......@@ -745,7 +745,7 @@ Qed.
(** * Framing *)
Lemma tac_frame_pure Δ (φ : Prop) P Q :
φ Frame ( φ) P Q (Δ Q) Δ P.
Proof. intros ?? ->. by rewrite -(frame ( φ) P) pure_equiv // left_id. Qed.
Proof. intros ?? ->. by rewrite -(frame ( φ) P) pure_True // left_id. Qed.
Lemma tac_frame Δ Δ' i p R P Q :
envs_lookup_delete i Δ = Some (p, R, Δ') Frame R P Q
......
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