Skip to content

GitLab

Commit dff7eb3c authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents c05f2a06 978eec47
Expand all Hide whitespace changes
Inline Side-by-side
algebra/agree.v
View file @ dff7eb3c
......@@ -130,11 +130,11 @@ Lemma to_agree_car n (x : agree A) : ✓{n} x → to_agree (x n) ≡{n}≡ x.
Proof. intros [??]; split; naive_solver eauto using agree_valid_le. Qed.
(** Internalized properties *)
Lemma agree_equivI {M} a b : (to_agree a ≡ to_agree b)%I ≡ (a ≡ b : uPred M)%I.
Lemma agree_equivI {M} a b : (to_agree a ≡ to_agree b) ⊣⊢ (a ≡ b : uPred M).
Proof.
uPred.unseal. do 2 split. by intros [? Hv]; apply (Hv n). apply: to_agree_ne.
Qed.
Lemma agree_validI {M} x y : ✓ (x ⋅ y) ⊑ (x ≡ y : uPred M).
Lemma agree_validI {M} x y : ✓ (x ⋅ y) ⊢ (x ≡ y : uPred M).
Proof. uPred.unseal; split=> r n _ ?; by apply: agree_op_inv. Qed.
End agree.
......
algebra/auth.v
View file @ dff7eb3c
......@@ -138,14 +138,14 @@ Admitted.
(** Internalized properties *)
Lemma auth_equivI {M} (x y : auth A) :
(x ≡ y)%I ≡ (authoritative x ≡ authoritative y ∧ own x ≡ own y : uPred M)%I.
(x ≡ y) ⊣⊢ (authoritative x ≡ authoritative y ∧ own x ≡ own y : uPred M).
Proof. by uPred.unseal. Qed.
Lemma auth_validI {M} (x : auth A) :
(✓ x)%I ≡ (match authoritative x with
(✓ x) ⊣⊢ (match authoritative x with
| Excl a => (∃ b, a ≡ own x ⋅ b) ∧ ✓ a
| ExclUnit => ✓ own x
| ExclBot => False
end : uPred M)%I.
end : uPred M).
Proof. uPred.unseal. by destruct x as [[]]. Qed.
(** The notations ◯ and ● only work for CMRAs with an empty element. So, in
......
algebra/excl.v
View file @ dff7eb3c
......@@ -138,16 +138,16 @@ Qed.
(** Internalized properties *)
Lemma excl_equivI {M} (x y : excl A) :
(x ≡ y)%I ≡ (match x, y with
(x ≡ y) ⊣⊢ (match x, y with
| Excl a, Excl b => a ≡ b
| ExclUnit, ExclUnit | ExclBot, ExclBot => True
| _, _ => False
end : uPred M)%I.
end : uPred M).
Proof.
uPred.unseal. do 2 split. by destruct 1. by destruct x, y; try constructor.
Qed.
Lemma excl_validI {M} (x : excl A) :
(✓ x)%I ≡ (if x is ExclBot then False else True : uPred M)%I.
(✓ x) ⊣⊢ (if x is ExclBot then False else True : uPred M).
Proof. uPred.unseal. by destruct x. Qed.
(** ** Local updates *)
......
algebra/fin_maps.v
View file @ dff7eb3c
......@@ -164,9 +164,9 @@ Global Instance map_cmra_discrete : CMRADiscrete A → CMRADiscrete mapR.
Proof. split; [apply _|]. intros m ? i. by apply: cmra_discrete_valid. Qed.
(** Internalized properties *)
Lemma map_equivI {M} m1 m2 : (m1 ≡ m2)%I ≡ (∀ i, m1 !! i ≡ m2 !! i : uPred M)%I.
Lemma map_equivI {M} m1 m2 : (m1 ≡ m2) ⊣⊢ (∀ i, m1 !! i ≡ m2 !! i : uPred M).
Proof. by uPred.unseal. Qed.
Lemma map_validI {M} m : (✓ m)%I ≡ (∀ i, ✓ (m !! i) : uPred M)%I.
Lemma map_validI {M} m : (✓ m) ⊣⊢ (∀ i, ✓ (m !! i) : uPred M).
Proof. by uPred.unseal. Qed.
End cmra.
......
algebra/frac.v
View file @ dff7eb3c
......@@ -177,17 +177,17 @@ Proof. intros. by apply frac_validN_inv_l with 0 a, cmra_valid_validN. Qed.
(** Internalized properties *)
Lemma frac_equivI {M} (x y : frac A) :
(x ≡ y)%I ≡ (match x, y with
(x ≡ y) ⊣⊢ (match x, y with
| Frac q1 a, Frac q2 b => q1 = q2 ∧ a ≡ b
| FracUnit, FracUnit => True
| _, _ => False
end : uPred M)%I.
end : uPred M).
Proof.
uPred.unseal; do 2 split; first by destruct 1.
by destruct x, y; destruct 1; try constructor.
Qed.
Lemma frac_validI {M} (x : frac A) :
(✓ x)%I ≡ (if x is Frac q a then ■ (q ≤ 1)%Qc ∧ ✓ a else True : uPred M)%I.
(✓ x) ⊣⊢ (if x is Frac q a then ■ (q ≤ 1)%Qc ∧ ✓ a else True : uPred M).
Proof. uPred.unseal. by destruct x. Qed.
(** ** Local updates *)
......
algebra/iprod.v
View file @ dff7eb3c
......@@ -164,9 +164,9 @@ Section iprod_cmra.
Qed.
(** Internalized properties *)
Lemma iprod_equivI {M} g1 g2 : (g1 ≡ g2)%I ≡ (∀ i, g1 i ≡ g2 i : uPred M)%I.
Lemma iprod_equivI {M} g1 g2 : (g1 ≡ g2) ⊣⊢ (∀ i, g1 i ≡ g2 i : uPred M).
Proof. by uPred.unseal. Qed.
Lemma iprod_validI {M} g : (✓ g)%I ≡ (∀ i, ✓ g i : uPred M)%I.
Lemma iprod_validI {M} g : (✓ g) ⊣⊢ (∀ i, ✓ g i : uPred M).
Proof. by uPred.unseal. Qed.
(** Properties of iprod_insert. *)
......
algebra/option.v
View file @ dff7eb3c
......@@ -132,14 +132,14 @@ Proof. by destruct mx, my; inversion_clear 1. Qed.
(** Internalized properties *)
Lemma option_equivI {M} (x y : option A) :
(x ≡ y)%I ≡ (match x, y with
(x ≡ y) ⊣⊢ (match x, y with
| Some a, Some b => a ≡ b | None, None => True | _, _ => False
end : uPred M)%I.
end : uPred M).
Proof.
uPred.unseal. do 2 split. by destruct 1. by destruct x, y; try constructor.
Qed.
Lemma option_validI {M} (x : option A) :
(✓ x)%I ≡ (match x with Some a => ✓ a | None => True end : uPred M)%I.
(✓ x) ⊣⊢ (match x with Some a => ✓ a | None => True end : uPred M).
Proof. uPred.unseal. by destruct x. Qed.
(** Updates *)
......
algebra/upred.v
View file @ dff7eb3c
This diff is collapsed.
algebra/upred_big_op.v
View file @ dff7eb3c
......@@ -39,9 +39,9 @@ Implicit Types Ps Qs : list (uPred M).
Implicit Types A : Type.
(* Big ops *)
Global Instance big_and_proper : Proper ((≡) ==> (≡)) (@uPred_big_and M).
Global Instance big_and_proper : Proper ((≡) ==> (⊣⊢)) (@uPred_big_and M).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance big_sep_proper : Proper ((≡) ==> (≡)) (@uPred_big_sep M).
Global Instance big_sep_proper : Proper ((≡) ==> (⊣⊢)) (@uPred_big_sep M).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance big_and_ne n :
......@@ -51,19 +51,19 @@ Global Instance big_sep_ne n :
Proper (Forall2 (dist n) ==> dist n) (@uPred_big_sep M).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance big_and_mono' : Proper (Forall2 (⊑) ==> (⊑)) (@uPred_big_and M).
Global Instance big_and_mono' : Proper (Forall2 (⊢) ==> (⊢)) (@uPred_big_and M).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance big_sep_mono' : Proper (Forall2 (⊑) ==> (⊑)) (@uPred_big_sep M).
Global Instance big_sep_mono' : Proper (Forall2 (⊢) ==> (⊢)) (@uPred_big_sep M).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance big_and_perm : Proper ((≡ₚ) ==> (≡)) (@uPred_big_and M).
Global Instance big_and_perm : Proper ((≡ₚ) ==> (⊣⊢)) (@uPred_big_and M).
Proof.
induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
- by rewrite IH.
- by rewrite !assoc (comm _ P).
- etrans; eauto.
Qed.
Global Instance big_sep_perm : Proper ((≡ₚ) ==> (≡)) (@uPred_big_sep M).
Global Instance big_sep_perm : Proper ((≡ₚ) ==> (⊣⊢)) (@uPred_big_sep M).
Proof.
induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
- by rewrite IH.
......@@ -71,26 +71,26 @@ Proof.
- etrans; eauto.
Qed.
Lemma big_and_app Ps Qs : (Π∧ (Ps ++ Qs))%I ≡ (Π∧ Ps ∧ Π∧ Qs)%I.
Lemma big_and_app Ps Qs : (Π∧ (Ps ++ Qs)) ⊣⊢ (Π∧ Ps ∧ Π∧ Qs).
Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
Lemma big_sep_app Ps Qs : (Π★ (Ps ++ Qs))%I ≡ (Π★ Ps ★ Π★ Qs)%I.
Lemma big_sep_app Ps Qs : (Π★ (Ps ++ Qs)) ⊣⊢ (Π★ Ps ★ Π★ Qs).
Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
Lemma big_and_contains Ps Qs : Qs `contains` Ps → (Π∧ Ps)%I ⊑ (Π∧ Qs)%I.
Lemma big_and_contains Ps Qs : Qs `contains` Ps → (Π∧ Ps) ⊢ (Π∧ Qs).
Proof.
intros [Ps' ->]%contains_Permutation. by rewrite big_and_app and_elim_l.
Qed.
Lemma big_sep_contains Ps Qs : Qs `contains` Ps → (Π★ Ps)%I ⊑ (Π★ Qs)%I.
Lemma big_sep_contains Ps Qs : Qs `contains` Ps → (Π★ Ps) ⊢ (Π★ Qs).
Proof.
intros [Ps' ->]%contains_Permutation. by rewrite big_sep_app sep_elim_l.
Qed.
Lemma big_sep_and Ps : (Π★ Ps) ⊑ (Π∧ Ps).
Lemma big_sep_and Ps : (Π★ Ps) ⊢ (Π∧ Ps).
Proof. by induction Ps as [|P Ps IH]; simpl; auto with I. Qed.
Lemma big_and_elem_of Ps P : P ∈ Ps → (Π∧ Ps) ⊑ P.
Lemma big_and_elem_of Ps P : P ∈ Ps → (Π∧ Ps) ⊢ P.
Proof. induction 1; simpl; auto with I. Qed.
Lemma big_sep_elem_of Ps P : P ∈ Ps → (Π★ Ps) ⊑ P.
Lemma big_sep_elem_of Ps P : P ∈ Ps → (Π★ Ps) ⊢ P.
Proof. induction 1; simpl; auto with I. Qed.
(* Big ops over finite maps *)
......@@ -100,8 +100,8 @@ Section gmap.
Implicit Types Φ Ψ : K → A → uPred M.
Lemma big_sepM_mono Φ Ψ m1 m2 :
m2 ⊆ m1 → (∀ x k, m2 !! k = Some x → Φ k x ⊑ Ψ k x) →
(Π★{map m1} Φ) ⊑ (Π★{map m2} Ψ).
m2 ⊆ m1 → (∀ x k, m2 !! k = Some x → Φ k x ⊢ Ψ k x) →
(Π★{map m1} Φ) ⊢ (Π★{map m2} Ψ).
Proof.
intros HX HΦ. trans (Π★{map m2} Φ)%I.
- by apply big_sep_contains, fmap_contains, map_to_list_contains.
......@@ -117,36 +117,36 @@ Section gmap.
apply Forall2_Forall, Forall_true=> -[i x]; apply HΦ.
Qed.
Global Instance big_sepM_proper m :
Proper (pointwise_relation _ (pointwise_relation _ (≡)) ==> (≡))
Proper (pointwise_relation _ (pointwise_relation _ (⊣⊢)) ==> (⊣⊢))
(uPred_big_sepM (M:=M) m).
Proof.
intros Φ1 Φ2 HΦ; apply equiv_dist=> n.
apply big_sepM_ne=> k x; apply equiv_dist, HΦ.
Qed.
Global Instance big_sepM_mono' m :
Proper (pointwise_relation _ (pointwise_relation _ (⊑)) ==> (⊑))
Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (⊢))
(uPred_big_sepM (M:=M) m).
Proof. intros Φ1 Φ2 HΦ. apply big_sepM_mono; intros; [done|apply HΦ]. Qed.
Lemma big_sepM_empty Φ : (Π★{map ∅} Φ)%I ≡ True%I.
Lemma big_sepM_empty Φ : (Π★{map ∅} Φ) ⊣⊢ True.
Proof. by rewrite /uPred_big_sepM map_to_list_empty. Qed.
Lemma big_sepM_insert Φ (m : gmap K A) i x :
m !! i = None → (Π★{map <[i:=x]> m} Φ)%I ≡ (Φ i x ★ Π★{map m} Φ)%I.
m !! i = None → (Π★{map <[i:=x]> m} Φ) ⊣⊢ (Φ i x ★ Π★{map m} Φ).
Proof. intros ?; by rewrite /uPred_big_sepM map_to_list_insert. Qed.
Lemma big_sepM_singleton Φ i x : (Π★{map {[i := x]}} Φ)%I ≡ (Φ i x)%I.
Lemma big_sepM_singleton Φ i x : (Π★{map {[i := x]}} Φ) ⊣⊢ (Φ i x).
Proof.
rewrite -insert_empty big_sepM_insert/=; last auto using lookup_empty.
by rewrite big_sepM_empty right_id.
Qed.
Lemma big_sepM_sepM Φ Ψ m :
(Π★{map m} (λ i x, Φ i x ★ Ψ i x))%I ≡ (Π★{map m} Φ ★ Π★{map m} Ψ)%I.
(Π★{map m} (λ i x, Φ i x ★ Ψ i x)) ⊣⊢ (Π★{map m} Φ ★ Π★{map m} Ψ).
Proof.
rewrite /uPred_big_sepM.
induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?right_id //.
by rewrite IH -!assoc (assoc _ (Ψ _ _)) [(Ψ _ _ ★ _)%I]comm -!assoc.
Qed.
Lemma big_sepM_later Φ m : (▷ Π★{map m} Φ)%I ≡ (Π★{map m} (λ i x, ▷ Φ i x))%I.
Lemma big_sepM_later Φ m : (▷ Π★{map m} Φ) ⊣⊢ (Π★{map m} (λ i x, ▷ Φ i x)).
Proof.
rewrite /uPred_big_sepM.
induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?later_True //.
......@@ -161,7 +161,7 @@ Section gset.
Implicit Types Φ : A → uPred M.
Lemma big_sepS_mono Φ Ψ X Y :
Y ⊆ X → (∀ x, x ∈ Y → Φ x ⊑ Ψ x) → (Π★{set X} Φ) ⊑ (Π★{set Y} Ψ).
Y ⊆ X → (∀ x, x ∈ Y → Φ x ⊢ Ψ x) → (Π★{set X} Φ) ⊢ (Π★{set Y} Ψ).
Proof.
intros HX HΦ. trans (Π★{set Y} Φ)%I.
- by apply big_sep_contains, fmap_contains, elements_contains.
......@@ -176,38 +176,38 @@ Section gset.
apply Forall2_Forall, Forall_true=> x; apply HΦ.
Qed.
Lemma big_sepS_proper X :
Proper (pointwise_relation _ (≡) ==> (≡)) (uPred_big_sepS (M:=M) X).
Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (uPred_big_sepS (M:=M) X).
Proof.
intros Φ1 Φ2 HΦ; apply equiv_dist=> n.
apply big_sepS_ne=> x; apply equiv_dist, HΦ.
Qed.
Lemma big_sepS_mono' X :
Proper (pointwise_relation _ (⊑) ==> (⊑)) (uPred_big_sepS (M:=M) X).
Proper (pointwise_relation _ (⊢) ==> (⊢)) (uPred_big_sepS (M:=M) X).
Proof. intros Φ1 Φ2 HΦ. apply big_sepS_mono; naive_solver. Qed.
Lemma big_sepS_empty Φ : (Π★{set ∅} Φ)%I ≡ True%I.
Lemma big_sepS_empty Φ : (Π★{set ∅} Φ) ⊣⊢ True.
Proof. by rewrite /uPred_big_sepS elements_empty. Qed.
Lemma big_sepS_insert Φ X x :
x ∉ X → (Π★{set {[ x ]} ∪ X} Φ)%I ≡ (Φ x ★ Π★{set X} Φ)%I.
x ∉ X → (Π★{set {[ x ]} ∪ X} Φ) ⊣⊢ (Φ x ★ Π★{set X} Φ).
Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed.
Lemma big_sepS_delete Φ X x :
x ∈ X → (Π★{set X} Φ)%I ≡ (Φ x ★ Π★{set X ∖ {[ x ]}} Φ)%I.
x ∈ X → (Π★{set X} Φ) ⊣⊢ (Φ x ★ Π★{set X ∖ {[ x ]}} Φ).
Proof.
intros. rewrite -big_sepS_insert; last set_solver.
by rewrite -union_difference_L; last set_solver.
Qed.
Lemma big_sepS_singleton Φ x : (Π★{set {[ x ]}} Φ)%I ≡ (Φ x)%I.
Lemma big_sepS_singleton Φ x : (Π★{set {[ x ]}} Φ) ⊣⊢ (Φ x).
Proof. intros. by rewrite /uPred_big_sepS elements_singleton /= right_id. Qed.
Lemma big_sepS_sepS Φ Ψ X :
(Π★{set X} (λ x, Φ x ★ Ψ x))%I ≡ (Π★{set X} Φ ★ Π★{set X} Ψ)%I.
(Π★{set X} (λ x, Φ x ★ Ψ x)) ⊣⊢ (Π★{set X} Φ ★ Π★{set X} Ψ).
Proof.
rewrite /uPred_big_sepS.
induction (elements X) as [|x l IH]; csimpl; first by rewrite ?right_id.
by rewrite IH -!assoc (assoc _ (Ψ _)) [(Ψ _ ★ _)%I]comm -!assoc.
Qed.
Lemma big_sepS_later Φ X : (▷ Π★{set X} Φ)%I ≡ (Π★{set X} (λ x, ▷ Φ x))%I.
Lemma big_sepS_later Φ X : (▷ Π★{set X} Φ) ⊣⊢ (Π★{set X} (λ x, ▷ Φ x)).
Proof.
rewrite /uPred_big_sepS.
induction (elements X) as [|x l IH]; csimpl; first by rewrite ?later_True.
......
algebra/upred_tactics.v
View file @ dff7eb3c
......@@ -24,18 +24,18 @@ Module uPred_reflection. Section uPred_reflection.
Notation eval_list Σ l :=
(uPred_big_sep ((λ n, from_option True%I (Σ !! n)) <$> l)).
Lemma eval_flatten Σ e : eval Σ e ≡ eval_list Σ (flatten e).
Lemma eval_flatten Σ e : eval Σ e ⊣⊢ eval_list Σ (flatten e).
Proof.
induction e as [| |e1 IH1 e2 IH2];
rewrite /= ?right_id ?fmap_app ?big_sep_app ?IH1 ?IH2 //.
Qed.
Lemma flatten_entails Σ e1 e2 :
flatten e2 `contains` flatten e1 → eval Σ e1 ⊑ eval Σ e2.
flatten e2 `contains` flatten e1 → eval Σ e1 ⊢ eval Σ e2.
Proof.
intros. rewrite !eval_flatten. by apply big_sep_contains, fmap_contains.
Qed.
Lemma flatten_equiv Σ e1 e2 :
flatten e2 ≡ₚ flatten e1 → eval Σ e1 ≡ eval Σ e2.
flatten e2 ≡ₚ flatten e1 → eval Σ e1 ⊣⊢ eval Σ e2.
Proof. intros He. by rewrite !eval_flatten He. Qed.
Fixpoint prune (e : expr) : expr :=
......@@ -54,7 +54,7 @@ Module uPred_reflection. Section uPred_reflection.
induction e as [| |e1 IH1 e2 IH2]; simplify_eq/=; auto.
rewrite -IH1 -IH2. by repeat case_match; rewrite ?right_id_L.
Qed.
Lemma prune_correct Σ e : eval Σ (prune e) ≡ eval Σ e.
Lemma prune_correct Σ e : eval Σ (prune e) ⊣⊢ eval Σ e.
Proof. by rewrite !eval_flatten flatten_prune. Qed.
Fixpoint cancel_go (n : nat) (e : expr) : option expr :=
......@@ -86,7 +86,7 @@ Module uPred_reflection. Section uPred_reflection.
Qed.
Lemma cancel_entails Σ e1 e2 e1' e2' ns :
cancel ns e1 = Some e1' → cancel ns e2 = Some e2' →
eval Σ e1' ⊑ eval Σ e2' → eval Σ e1 ⊑ eval Σ e2.
eval Σ e1' ⊢ eval Σ e2' → eval Σ e1 ⊢ eval Σ e2.
Proof.
intros ??. rewrite !eval_flatten.
rewrite (flatten_cancel e1 e1' ns) // (flatten_cancel e2 e2' ns) //; csimpl.
......@@ -100,20 +100,20 @@ Module uPred_reflection. Section uPred_reflection.
| n :: l => ESep (EVar n) (to_expr l)
end.
Arguments to_expr !_ / : simpl nomatch.
Lemma eval_to_expr Σ l : eval Σ (to_expr l) ≡ eval_list Σ l.
Lemma eval_to_expr Σ l : eval Σ (to_expr l) ⊣⊢ eval_list Σ l.
Proof.
induction l as [|n1 [|n2 l] IH]; csimpl; rewrite ?right_id //.
by rewrite IH.
Qed.
Lemma split_l Σ e ns e' :
cancel ns e = Some e' → eval Σ e ≡ (eval Σ (to_expr ns) ★ eval Σ e')%I.
cancel ns e = Some e' → eval Σ e ⊣⊢ (eval Σ (to_expr ns) ★ eval Σ e').
Proof.
intros He%flatten_cancel.
by rewrite eval_flatten He fmap_app big_sep_app eval_to_expr eval_flatten.
Qed.
Lemma split_r Σ e ns e' :
cancel ns e = Some e' → eval Σ e ≡ (eval Σ e' ★ eval Σ (to_expr ns))%I.
cancel ns e = Some e' → eval Σ e ⊣⊢ (eval Σ e' ★ eval Σ (to_expr ns)).
Proof. intros. rewrite /= comm. by apply split_l. Qed.
Class Quote (Σ1 Σ2 : list (uPred M)) (P : uPred M) (e : expr) := {}.
......@@ -132,16 +132,16 @@ Module uPred_reflection. Section uPred_reflection.
Ltac quote :=
match goal with
| |- ?P1 ⊑ ?P2 =>
| |- ?P1 ⊢ ?P2 =>
lazymatch type of (_ : Quote [] _ P1 _) with Quote _ ?Σ2 _ ?e1 =>
lazymatch type of (_ : Quote Σ2 _ P2 _) with Quote _ ?Σ3 _ ?e2 =>
change (eval Σ3 e1 ⊑ eval Σ3 e2) end end
change (eval Σ3 e1 ⊢ eval Σ3 e2) end end
end.
Ltac quote_l :=
match goal with
| |- ?P1 ⊑ ?P2 =>
| |- ?P1 ⊢ ?P2 =>
lazymatch type of (_ : Quote [] _ P1 _) with Quote _ ?Σ2 _ ?e1 =>
change (eval Σ2 e1 ⊑ P2) end
change (eval Σ2 e1 ⊢ P2) end
end.
End uPred_reflection.
......@@ -162,7 +162,7 @@ Ltac close_uPreds Ps tac :=
Tactic Notation "cancel" constr(Ps) :=
uPred_reflection.quote;
let Σ := match goal with |- uPred_reflection.eval ?Σ _ ⊑ _ => Σ end in
let Σ := match goal with |- uPred_reflection.eval ?Σ _ ⊢ _ => Σ end in
let ns' := lazymatch type of (_ : uPred_reflection.QuoteArgs Σ Ps _) with
| uPred_reflection.QuoteArgs _ _ ?ns' => ns'
end in
......@@ -172,12 +172,12 @@ Tactic Notation "cancel" constr(Ps) :=
Tactic Notation "ecancel" open_constr(Ps) :=
close_uPreds Ps ltac:(fun Qs => cancel Qs).
(** [to_front [P1, P2, ..]] rewrites in the premise of ⊑ such that
(** [to_front [P1, P2, ..]] rewrites in the premise of ⊢ such that
the assumptions P1, P2, ... appear at the front, in that order. *)
Tactic Notation "to_front" open_constr(Ps) :=
close_uPreds Ps ltac:(fun Ps =>
uPred_reflection.quote_l;
let Σ := match goal with |- uPred_reflection.eval ?Σ _ ⊑ _ => Σ end in
let Σ := match goal with |- uPred_reflection.eval ?Σ _ ⊢ _ => Σ end in
let ns' := lazymatch type of (_ : uPred_reflection.QuoteArgs Σ Ps _) with
| uPred_reflection.QuoteArgs _ _ ?ns' => ns'
end in
......@@ -188,7 +188,7 @@ Tactic Notation "to_front" open_constr(Ps) :=
Tactic Notation "to_back" open_constr(Ps) :=
close_uPreds Ps ltac:(fun Ps =>
uPred_reflection.quote_l;
let Σ := match goal with |- uPred_reflection.eval ?Σ _ ⊑ _ => Σ end in
let Σ := match goal with |- uPred_reflection.eval ?Σ _ ⊢ _ => Σ end in
let ns' := lazymatch type of (_ : uPred_reflection.QuoteArgs Σ Ps _) with
| uPred_reflection.QuoteArgs _ _ ?ns' => ns'
end in
......@@ -205,46 +205,46 @@ Tactic Notation "sep_split" "right:" open_constr(Ps) :=
Tactic Notation "sep_split" "left:" open_constr(Ps) :=
to_front Ps; apply sep_mono.
(** Assumes a goal of the shape P ⊑ ▷ Q. Alterantively, if Q
(** Assumes a goal of the shape P ⊢ ▷ Q. Alterantively, if Q
is built of ★, ∧, ∨ with ▷ in all branches; that will work, too.
Will turn this goal into P ⊑ Q and strip ▷ in P below ★, ∧, ∨. *)
Will turn this goal into P ⊢ Q and strip ▷ in P below ★, ∧, ∨. *)
Ltac strip_later :=
let rec strip :=
lazymatch goal with
| |- (_ ★ _) ⊑ ▷ _ =>
| |- (_ ★ _) ⊢ ▷ _ =>
etrans; last (eapply equiv_entails_sym, later_sep);
apply sep_mono; strip
| |- (_ ∧ _) ⊑ ▷ _ =>
| |- (_ ∧ _) ⊢ ▷ _ =>
etrans; last (eapply equiv_entails_sym, later_and);
apply sep_mono; strip
| |- (_ ∨ _) ⊑ ▷ _ =>
| |- (_ ∨ _) ⊢ ▷ _ =>
etrans; last (eapply equiv_entails_sym, later_or);
apply sep_mono; strip
| |- ▷ _ ⊑ ▷ _ => apply later_mono; reflexivity
| |- _ ⊑ ▷ _ => apply later_intro; reflexivity
| |- ▷ _ ⊢ ▷ _ => apply later_mono; reflexivity
| |- _ ⊢ ▷ _ => apply later_intro; reflexivity
end
in let rec shape_Q :=
lazymatch goal with
| |- _ ⊑ (_ ★ _) =>
| |- _ ⊢ (_ ★ _) =>
(* Force the later on the LHS to be top-level, matching laters
below ★ on the RHS *)
etrans; first (apply equiv_entails, later_sep; reflexivity);
(* Match the arm recursively *)
apply sep_mono; shape_Q
| |- _ ⊑ (_ ∧ _) =>
| |- _ ⊢ (_ ∧ _) =>
etrans; first (apply equiv_entails, later_and; reflexivity);
apply sep_mono; shape_Q
| |- _ ⊑ (_ ∨ _) =>
| |- _ ⊢ (_ ∨ _) =>
etrans; first (apply equiv_entails, later_or; reflexivity);
apply sep_mono; shape_Q
| |- _ ⊑ ▷ _ => apply later_mono; reflexivity
| |- _ ⊢ ▷ _ => apply later_mono; reflexivity
(* We fail if we don't find laters in all branches. *)
end
in intros_revert ltac:(etrans; [|shape_Q];
etrans; last eapply later_mono; first solve [ strip ]).
(** Transforms a goal of the form ∀ ..., ?0... → ?1 ⊑ ?2
into True ⊑ ∀..., ■?0... → ?1 → ?2, applies tac, and
(** Transforms a goal of the form ∀ ..., ?0... → ?1 ⊢ ?2
into True ⊢ ∀..., ■?0... → ?1 → ?2, applies tac, and
the moves all the assumptions back. *)
(* TODO: this name may be a big too general *)
Ltac revert_all :=
......@@ -256,20 +256,20 @@ Ltac revert_all :=
on the sort of the argument, which is suboptimal. *)
first [ apply (const_intro_impl _ _ _ H); clear H
| revert H; apply forall_elim']
| |- _ ⊑ _ => apply impl_entails
| |- _ ⊢ _ => apply impl_entails
end.
(** This starts on a goal of the form ∀ ..., ?0... → ?1 ⊑ ?2.
(** This starts on a goal of the form ∀ ..., ?0... → ?1 ⊢ ?2.
It applies löb where all the Coq assumptions have been turned into logical
assumptions, then moves all the Coq assumptions back out to the context,
applies [tac] on the goal (now of the form _ ⊑ _), and then reverts the
applies [tac] on the goal (now of the form _ ⊢ _), and then reverts the
Coq assumption so that we end up with the same shape as where we started,
but with an additional assumption ★-ed to the context *)
Ltac löb tac :=
revert_all;
(* Add a box *)
etrans; last (eapply always_elim; reflexivity);
(* We now have a goal for the form True ⊑ P, with the "original" conclusion
(* We now have a goal for the form True ⊢ P, with the "original" conclusion
being locked. *)
apply löb_strong; etransitivity;
first (apply equiv_entails, left_id, _; reflexivity);
......@@ -278,13 +278,13 @@ Ltac löb tac :=
do the work *)
let rec go :=
lazymatch goal with
| |- _ ⊑ (∀ _, _) =>
| |- _ ⊢ (∀ _, _) =>
apply forall_intro; let H := fresh in intro H; go; revert H
| |- _ ⊑ (■ _ → _) =>
| |- _ ⊢ (■ _ → _) =>
apply impl_intro_l, const_elim_l; let H := fresh in intro H; go; revert H
(* This is the "bottom" of the goal, where we see the impl introduced
by uPred_revert_all as well as the ▷ from löb_strong and the □ we added. *)
| |- ▷ □ ?R ⊑ (?L → _) => apply impl_intro_l;
| |- ▷ □ ?R ⊢ (?L → _) => apply impl_intro_l;
trans (L ★ ▷ □ R)%I;
[eapply equiv_entails, always_and_sep_r, _; reflexivity | tac]<