diff --git a/base_logic/base_logic.v b/base_logic/base_logic.v index 31e643b158b2007ef8fe1d75824ef7341660d365..2ea42a57a9fb5f9a38061ede335f4586cc885890 100644 --- a/base_logic/base_logic.v +++ b/base_logic/base_logic.v @@ -14,4 +14,4 @@ Hint Resolve and_intro and_elim_l' and_elim_r' : I. Hint Resolve always_mono : I. Hint Resolve sep_elim_l' sep_elim_r' sep_mono : I. Hint Immediate True_intro False_elim : I. -Hint Immediate iff_refl eq_refl' : I. +Hint Immediate iff_refl internal_eq_refl' : I. diff --git a/base_logic/derived.v b/base_logic/derived.v index 7f4efa6e25a760fc172de6ba5a00cb25374cf4d6..a485b335a8fc86af8a242fa4238b04b549e0be62 100644 --- a/base_logic/derived.v +++ b/base_logic/derived.v @@ -241,13 +241,13 @@ Proof. - apply exist_elim=> x. eauto using pure_mono. Qed. -Lemma eq_refl' {A : cofeT} (a : A) P : P ⊢ a ≡ a. -Proof. rewrite (True_intro P). apply eq_refl. Qed. -Hint Resolve eq_refl'. -Lemma equiv_eq {A : cofeT} P (a b : A) : a ≡ b → P ⊢ a ≡ b. +Lemma internal_eq_refl' {A : cofeT} (a : A) P : P ⊢ a ≡ a. +Proof. rewrite (True_intro P). apply internal_eq_refl. Qed. +Hint Resolve internal_eq_refl'. +Lemma equiv_internal_eq {A : cofeT} P (a b : A) : a ≡ b → P ⊢ a ≡ b. Proof. by intros ->. Qed. -Lemma eq_sym {A : cofeT} (a b : A) : a ≡ b ⊢ b ≡ a. -Proof. apply (eq_rewrite a b (λ b, b ≡ a)%I); auto. solve_proper. Qed. +Lemma internal_eq_sym {A : cofeT} (a b : A) : a ≡ b ⊢ b ≡ a. +Proof. apply (internal_eq_rewrite a b (λ b, b ≡ a)%I); auto. solve_proper. Qed. Lemma pure_alt φ : ■ φ ⊣⊢ ∃ _ : φ, True. Proof. @@ -280,9 +280,10 @@ Proof. Qed. Lemma equiv_iff P Q : (P ⊣⊢ Q) → True ⊢ P ↔ Q. Proof. intros ->; apply iff_refl. Qed. -Lemma eq_iff P Q : P ≡ Q ⊢ P ↔ Q. +Lemma internal_eq_iff P Q : P ≡ Q ⊢ P ↔ Q. Proof. - apply (eq_rewrite P Q (λ Q, P ↔ Q))%I; first solve_proper; auto using iff_refl. + apply (internal_eq_rewrite P Q (λ Q, P ↔ Q))%I; + first solve_proper; auto using iff_refl. Qed. (* Derived BI Stuff *) @@ -445,12 +446,12 @@ Proof. apply impl_intro_l; rewrite -always_and. apply always_mono, impl_elim with P; auto. Qed. -Lemma always_eq {A:cofeT} (a b : A) : □ (a ≡ b) ⊣⊢ a ≡ b. +Lemma always_internal_eq {A:cofeT} (a b : A) : □ (a ≡ b) ⊣⊢ a ≡ b. Proof. apply (anti_symm (⊢)); auto using always_elim. - apply (eq_rewrite a b (λ b, □ (a ≡ b))%I); auto. + apply (internal_eq_rewrite a b (λ b, □ (a ≡ b))%I); auto. { intros n; solve_proper. } - rewrite -(eq_refl a) always_pure; auto. + rewrite -(internal_eq_refl a) always_pure; auto. Qed. Lemma always_and_sep P Q : □ (P ∧ Q) ⊣⊢ □ (P ★ Q). @@ -692,8 +693,8 @@ Global Instance ownM_timeless (a : M) : Timeless a → TimelessP (uPred_ownM a). Proof. intros ?. rewrite /TimelessP later_ownM. apply exist_elim=> b. rewrite (timelessP (a≡b)) (except_0_intro (uPred_ownM b)) -except_0_and. - apply except_0_mono. rewrite eq_sym. - apply (eq_rewrite b a (uPred_ownM)); first apply _; auto. + apply except_0_mono. rewrite internal_eq_sym. + apply (internal_eq_rewrite b a (uPred_ownM)); first apply _; auto. Qed. (* Persistence *) @@ -716,9 +717,9 @@ Proof. by intros; rewrite /PersistentP always_forall; apply forall_mono. Qed. Global Instance exist_persistent {A} (Ψ : A → uPred M) : (∀ x, PersistentP (Ψ x)) → PersistentP (∃ x, Ψ x). Proof. by intros; rewrite /PersistentP always_exist; apply exist_mono. Qed. -Global Instance eq_persistent {A : cofeT} (a b : A) : +Global Instance internal_eq_persistent {A : cofeT} (a b : A) : PersistentP (a ≡ b : uPred M)%I. -Proof. by intros; rewrite /PersistentP always_eq. Qed. +Proof. by intros; rewrite /PersistentP always_internal_eq. Qed. Global Instance cmra_valid_persistent {A : cmraT} (a : A) : PersistentP (✓ a : uPred M)%I. Proof. by intros; rewrite /PersistentP always_cmra_valid. Qed. diff --git a/base_logic/primitive.v b/base_logic/primitive.v index 5c8f15f1a70e24d36c2d0156a5310c68b6f85b93..7bcce8d77346757af140bb40b9f79321fcf881c8 100644 --- a/base_logic/primitive.v +++ b/base_logic/primitive.v @@ -58,12 +58,13 @@ Definition uPred_exist_aux : { x | x = @uPred_exist_def }. by eexists. Qed. Definition uPred_exist {M A} := proj1_sig uPred_exist_aux M A. Definition uPred_exist_eq: @uPred_exist = @uPred_exist_def := proj2_sig uPred_exist_aux. -Program Definition uPred_eq_def {M} {A : cofeT} (a1 a2 : A) : uPred M := +Program Definition uPred_internal_eq_def {M} {A : cofeT} (a1 a2 : A) : uPred M := {| uPred_holds n x := a1 ≡{n}≡ a2 |}. Solve Obligations with naive_solver eauto 2 using (dist_le (A:=A)). -Definition uPred_eq_aux : { x | x = @uPred_eq_def }. by eexists. Qed. -Definition uPred_eq {M A} := proj1_sig uPred_eq_aux M A. -Definition uPred_eq_eq: @uPred_eq = @uPred_eq_def := proj2_sig uPred_eq_aux. +Definition uPred_internal_eq_aux : { x | x = @uPred_internal_eq_def }. by eexists. Qed. +Definition uPred_internal_eq {M A} := proj1_sig uPred_internal_eq_aux M A. +Definition uPred_internal_eq_eq: + @uPred_internal_eq = @uPred_internal_eq_def := proj2_sig uPred_internal_eq_aux. Program Definition uPred_sep_def {M} (P Q : uPred M) : uPred M := {| uPred_holds n x := ∃ x1 x2, x ≡{n}≡ x1 ⋅ x2 ∧ P n x1 ∧ Q n x2 |}. @@ -177,7 +178,7 @@ Notation "□ P" := (uPred_always P) (at level 20, right associativity) : uPred_scope. Notation "▷ P" := (uPred_later P) (at level 20, right associativity) : uPred_scope. -Infix "≡" := uPred_eq : uPred_scope. +Infix "≡" := uPred_internal_eq : uPred_scope. Notation "✓ x" := (uPred_cmra_valid x) (at level 20) : uPred_scope. Notation "|==> Q" := (uPred_bupd Q) (at level 99, Q at level 200, format "|==> Q") : uPred_scope. @@ -189,7 +190,7 @@ Notation "P ==★ Q" := (P -★ |==> Q)%I Module uPred_primitive. Definition unseal := (uPred_pure_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq, - uPred_exist_eq, uPred_eq_eq, uPred_sep_eq, uPred_wand_eq, uPred_always_eq, + uPred_exist_eq, uPred_internal_eq_eq, uPred_sep_eq, uPred_wand_eq, uPred_always_eq, uPred_later_eq, uPred_ownM_eq, uPred_cmra_valid_eq, uPred_bupd_eq). Ltac unseal := rewrite !unseal /=. @@ -245,15 +246,15 @@ Proof. Qed. Global Instance wand_proper : Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@uPred_wand M) := ne_proper_2 _. -Global Instance eq_ne (A : cofeT) n : - Proper (dist n ==> dist n ==> dist n) (@uPred_eq M A). +Global Instance internal_eq_ne (A : cofeT) n : + Proper (dist n ==> dist n ==> dist n) (@uPred_internal_eq M A). Proof. intros x x' Hx y y' Hy; split=> n' z; unseal; split; intros; simpl in *. - by rewrite -(dist_le _ _ _ _ Hx) -?(dist_le _ _ _ _ Hy); auto. - by rewrite (dist_le _ _ _ _ Hx) ?(dist_le _ _ _ _ Hy); auto. Qed. -Global Instance eq_proper (A : cofeT) : - Proper ((≡) ==> (≡) ==> (⊣⊢)) (@uPred_eq M A) := ne_proper_2 _. +Global Instance internal_eq_proper (A : cofeT) : + Proper ((≡) ==> (≡) ==> (⊣⊢)) (@uPred_internal_eq M A) := ne_proper_2 _. Global Instance forall_ne A n : Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_forall M A). Proof. @@ -355,21 +356,16 @@ Proof. unseal; split=> n x ??; by exists a. Qed. Lemma exist_elim {A} (Φ : A → uPred M) Q : (∀ a, Φ a ⊢ Q) → (∃ a, Φ a) ⊢ Q. Proof. unseal; intros HΦΨ; split=> n x ? [a ?]; by apply HΦΨ with a. Qed. -Lemma eq_refl {A : cofeT} (a : A) : True ⊢ a ≡ a. +Lemma internal_eq_refl {A : cofeT} (a : A) : True ⊢ a ≡ a. Proof. unseal; by split=> n x ??; simpl. Qed. -Lemma eq_rewrite {A : cofeT} a b (Ψ : A → uPred M) P +Lemma internal_eq_rewrite {A : cofeT} a b (Ψ : A → uPred M) P {HΨ : ∀ n, Proper (dist n ==> dist n) Ψ} : (P ⊢ a ≡ b) → (P ⊢ Ψ a) → P ⊢ Ψ b. Proof. unseal; intros Hab Ha; split=> n x ??. apply HΨ with n a; auto. - by symmetry; apply Hab with x. - by apply Ha. Qed. -Lemma eq_equiv {A : cofeT} (a b : A) : (True ⊢ a ≡ b) → a ≡ b. -Proof. - unseal=> Hab; apply equiv_dist; intros n; apply Hab with ∅; last done. - apply cmra_valid_validN, ucmra_unit_valid. -Qed. -Lemma eq_rewrite_contractive {A : cofeT} a b (Ψ : A → uPred M) P +Lemma internal_eq_rewrite_contractive {A : cofeT} a b (Ψ : A → uPred M) P {HΨ : Contractive Ψ} : (P ⊢ ▷ (a ≡ b)) → (P ⊢ Ψ a) → P ⊢ Ψ b. Proof. unseal; intros Hab Ha; split=> n x ??. apply HΨ with n a; auto. diff --git a/program_logic/boxes.v b/program_logic/boxes.v index e2abbd055e972bc9eac6e223cee3db8e47acdaa8..03db8da2a658997873cdabedc3d0d495db509d17 100644 --- a/program_logic/boxes.v +++ b/program_logic/boxes.v @@ -165,7 +165,8 @@ Lemma box_fill_all f P Q : box N f P ★ ▷ P ={N}=★ box N (const true <\$> f) Proof. iIntros "[H HP]"; iDestruct "H" as (Φ) "[#HeqP Hf]". iExists Φ; iSplitR; first by rewrite big_sepM_fmap. - rewrite eq_iff later_iff big_sepM_later; iDestruct ("HeqP" with "HP") as "HP". + rewrite internal_eq_iff later_iff big_sepM_later. + iDestruct ("HeqP" with "HP") as "HP". iCombine "Hf" "HP" as "Hf". rewrite big_sepM_fmap; iApply (fupd_big_sepM _ _ f). iApply (big_sepM_impl _ _ f); iFrame "Hf". @@ -192,7 +193,7 @@ Proof. iMod ("Hclose" with "[Hγ]"); first (iNext; iExists false; iFrame; eauto). by iApply "HΦ". } iModIntro; iSplitL "HΦ". - - rewrite eq_iff later_iff big_sepM_later. by iApply "HeqP". + - rewrite internal_eq_iff later_iff big_sepM_later. by iApply "HeqP". - iExists Φ; iSplit; by rewrite big_sepM_fmap. Qed. End box. diff --git a/program_logic/iprop.v b/program_logic/iprop.v index 62c7ceb0586ba274a53641efd0ef6c0b626c9c77..96b7ea91164df204b244040023f4037e12f5bcc5 100644 --- a/program_logic/iprop.v +++ b/program_logic/iprop.v @@ -151,6 +151,6 @@ Lemma iProp_unfold_equivI {Σ} (P Q : iProp Σ) : iProp_unfold P ≡ iProp_unfold Q ⊢ (P ≡ Q : iProp Σ). Proof. rewrite -{2}(iProp_fold_unfold P) -{2}(iProp_fold_unfold Q). - eapply (uPred.eq_rewrite _ _ (λ z, + eapply (uPred.internal_eq_rewrite _ _ (λ z, iProp_fold (iProp_unfold P) ≡ iProp_fold z))%I; auto with I; solve_proper. Qed. diff --git a/program_logic/saved_prop.v b/program_logic/saved_prop.v index 5a804a2a1f6f4e72c77576db631043ac921308a8..22cfc001432763165dd80748d444718a09e4dc2c 100644 --- a/program_logic/saved_prop.v +++ b/program_logic/saved_prop.v @@ -42,7 +42,7 @@ Section saved_prop. { intros z. rewrite /G1 /G2 -cFunctor_compose -{2}[z]cFunctor_id. apply (ne_proper (cFunctor_map F)); split=>?; apply iProp_fold_unfold. } rewrite -{2}[x]help -{2}[y]help. apply later_mono. - apply (eq_rewrite (G1 x) (G1 y) (λ z, G2 (G1 x) ≡ G2 z))%I; + apply (internal_eq_rewrite (G1 x) (G1 y) (λ z, G2 (G1 x) ≡ G2 z))%I; first solve_proper; auto with I. Qed. End saved_prop. diff --git a/proofmode/class_instances.v b/proofmode/class_instances.v index 06cbcc6d01319ddbd86b9428eea5089f9889fb7c..f03509b43dfe354077708e44c46fa00b66982042 100644 --- a/proofmode/class_instances.v +++ b/proofmode/class_instances.v @@ -33,8 +33,11 @@ Proof. by rewrite /IntoPure discrete_valid. Qed. (* FromPure *) Global Instance from_pure_pure φ : @FromPure M (■ φ) φ. Proof. done. Qed. -Global Instance from_pure_eq {A : cofeT} (a b : A) : @FromPure M (a ≡ b) (a ≡ b). -Proof. rewrite /FromPure. eapply pure_elim; [done|]=> ->. apply eq_refl'. Qed. +Global Instance from_pure_internal_eq {A : cofeT} (a b : A) : + @FromPure M (a ≡ b) (a ≡ b). +Proof. + rewrite /FromPure. eapply pure_elim; [done|]=> ->. apply internal_eq_refl'. +Qed. Global Instance from_pure_cmra_valid {A : cmraT} (a : A) : @FromPure M (✓ a) (✓ a). Proof. diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v index f55b0e46e997ae55f057540078c33ed6261b2f7a..d520cf9a830bb706ac991aac02b0e4ff0adfc528 100644 --- a/proofmode/coq_tactics.v +++ b/proofmode/coq_tactics.v @@ -653,9 +653,9 @@ Lemma tac_rewrite Δ i p Pxy (lr : bool) Q : (∀ n, Proper (dist n ==> dist n) Φ) → (Δ ⊢ Φ (if lr then x else y)) → Δ ⊢ Q. Proof. - intros ? A x y ? HPxy -> ?; apply eq_rewrite; auto. + intros ? A x y ? HPxy -> ?; apply internal_eq_rewrite; auto. rewrite {1}envs_lookup_sound' //; rewrite sep_elim_l HPxy. - destruct lr; auto using eq_sym. + destruct lr; auto using internal_eq_sym. Qed. Lemma tac_rewrite_in Δ i p Pxy j q P (lr : bool) Q : @@ -673,8 +673,10 @@ Proof. rewrite sep_elim_l HPxy always_and_sep_r. rewrite (envs_simple_replace_sound _ _ j) //; simpl. rewrite HP right_id -assoc; apply wand_elim_r'. destruct lr. - - apply (eq_rewrite x y (λ y, □?q Φ y -★ Δ')%I); eauto with I. solve_proper. - - apply (eq_rewrite y x (λ y, □?q Φ y -★ Δ')%I); eauto using eq_sym with I. + - apply (internal_eq_rewrite x y (λ y, □?q Φ y -★ Δ')%I); + eauto with I. solve_proper. + - apply (internal_eq_rewrite y x (λ y, □?q Φ y -★ Δ')%I); + eauto using internal_eq_sym with I. solve_proper. Qed. diff --git a/proofmode/tactics.v b/proofmode/tactics.v index 1f449b36ab698c6e6ff65dde25d9188ec635e860..23848b1b8fb4c313707da9ddb3693049cc797ad0 100644 --- a/proofmode/tactics.v +++ b/proofmode/tactics.v @@ -1200,7 +1200,7 @@ Tactic Notation "iMod" open_constr(lem) "as" "%" simple_intropattern(pat) := Hint Extern 0 (of_envs _ ⊢ _) => by iPureIntro. Hint Extern 0 (of_envs _ ⊢ _) => iAssumption. Hint Extern 0 (of_envs _ ⊢ _) => progress iIntros. -Hint Resolve uPred.eq_refl'. (* Maybe make an [iReflexivity] tactic *) +Hint Resolve uPred.internal_eq_refl'. (* Maybe make an [iReflexivity] tactic *) (* We should be able to write [Hint Extern 1 (of_envs _ ⊢ (_ ★ _)%I) => ...], but then [eauto] mysteriously fails. See bug 4762 *) diff --git a/tests/proofmode.v b/tests/proofmode.v index f3c087059015d0818d47b17f80c6c5b05d28e114..7466cef64c69b80d2876b5500d58224d0db54815 100644 --- a/tests/proofmode.v +++ b/tests/proofmode.v @@ -67,7 +67,7 @@ Lemma demo_5 (M : ucmraT) (x y : M) (P : uPred M) : (∀ z, P → z ≡ y) ⊢ (P -★ (x,x) ≡ (y,x)). Proof. iIntros "H1 H2". - iRewrite (uPred.eq_sym x x with "[#]"); first done. + iRewrite (uPred.internal_eq_sym x x with "[#]"); first done. iRewrite -("H1" \$! _ with "[-]"); first done. done. Qed.