From 77a15fea647d8d775556879ab6a8992529840aa7 Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Thu, 25 Feb 2016 10:47:51 +0100
Subject: [PATCH] write a tactic that can solve Proper goals, and use it in a
few places
This replaces f_equiv and solve_proper with our own, hopefully better, versions

algebra/cofe.v  2 
algebra/sts.v  2 +
algebra/upred.v  2 +
barrier/proof.v  14 ++++
prelude/tactics.v  68 ++++++++++++++++++++++++++++++++++++++
program_logic/saved_prop.v  2 +
6 files changed, 77 insertions(+), 13 deletions()
diff git a/algebra/cofe.v b/algebra/cofe.v
index 3428d3c2..ce23c17d 100644
 a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ 40,8 +40,6 @@ Tactic Notation "cofe_subst" :=
 H:@dist ?A ?d ?n _ ?x  _ => symmetry in H;setoid_subst_aux (@dist A d n) x
end.
Tactic Notation "solve_ne" := intros; solve_proper.

Record chain (A : Type) `{Dist A} := {
chain_car :> nat → A;
chain_cauchy n i : n < i → chain_car i ≡{n}≡ chain_car (S n)
diff git a/algebra/sts.v b/algebra/sts.v
index 68a0590d..668dd8ee 100644
 a/algebra/sts.v
+++ b/algebra/sts.v
@@ 77,7 +77,7 @@ Proof. by intros ??? ?? [??]; split; apply up_preserving. Qed.
Global Instance up_set_preserving : Proper ((⊆) ==> flip (⊆) ==> (⊆)) up_set.
Proof.
intros S1 S2 HS T1 T2 HT. rewrite /up_set.
 f_equiv; last done. move =>s1 s2 Hs. simpl in HT. by apply up_preserving.
+ f_equiv. move =>s1 s2 Hs. simpl in HT. by apply up_preserving.
Qed.
Global Instance up_set_proper : Proper ((≡) ==> (≡) ==> (≡)) up_set.
Proof. by intros S1 S2 [??] T1 T2 [??]; split; apply up_set_preserving. Qed.
diff git a/algebra/upred.v b/algebra/upred.v
index 94b8bbc7..4a31b059 100644
 a/algebra/upred.v
+++ b/algebra/upred.v
@@ 648,7 +648,7 @@ Proof. intros; apply (anti_symm _); auto using const_intro. Qed.
Lemma equiv_eq {A : cofeT} P (a b : A) : a ≡ b → P ⊑ (a ≡ b).
Proof. intros >; apply eq_refl. Qed.
Lemma eq_sym {A : cofeT} (a b : A) : (a ≡ b) ⊑ (b ≡ a).
Proof. apply (eq_rewrite a b (λ b, b ≡ a)%I); auto using eq_refl. solve_ne. Qed.
+Proof. apply (eq_rewrite a b (λ b, b ≡ a)%I); auto using eq_refl. solve_proper. Qed.
(* BI connectives *)
Lemma sep_mono P P' Q Q' : P ⊑ Q → P' ⊑ Q' → (P ★ P') ⊑ (Q ★ Q').
diff git a/barrier/proof.v b/barrier/proof.v
index 4cbeeb32..41959838 100644
 a/barrier/proof.v
+++ b/barrier/proof.v
@@ 52,19 +52,17 @@ Definition recv (l : loc) (R : iProp) : iProp :=
saved_prop_own i Q ★ ▷ (Q ★ R))%I.
(** Setoids *)
(* TODO: These lemmas really ought to be doable by just calling a tactic.
 It is just application of already registered congruence lemmas. *)
Global Instance waiting_ne n : Proper (dist n ==> (=) ==> dist n) waiting.
Proof. intros P P' HP I ? <. rewrite /waiting. by setoid_rewrite HP. Qed.
+Proof. solve_proper. Qed.
Global Instance barrier_inv_ne n l :
 Proper (dist n ==> pointwise_relation _ (dist n)) (barrier_inv l).
Proof. intros P P' HP [[]]; rewrite /barrier_inv //=. by setoid_rewrite HP. Qed.
+ Proper (dist n ==> eq ==> dist n) (barrier_inv l).
+Proof. solve_proper. Qed.
Global Instance barrier_ctx_ne n γ l : Proper (dist n ==> dist n) (barrier_ctx γ l).
Proof. intros P P' HP. rewrite /barrier_ctx. by setoid_rewrite HP. Qed.
+Proof. solve_proper. Qed.
Global Instance send_ne n l : Proper (dist n ==> dist n) (send l).
Proof. intros P P' HP. rewrite /send. by setoid_rewrite HP. Qed.
+Proof. solve_proper. Qed.
Global Instance recv_ne n l : Proper (dist n ==> dist n) (recv l).
Proof. intros R R' HR. rewrite /recv. by setoid_rewrite HR. Qed.
+Proof. solve_proper. Qed.
(** Helper lemmas *)
Lemma waiting_split i i1 i2 Q R1 R2 P I :
diff git a/prelude/tactics.v b/prelude/tactics.v
index 9843baa6..a5aea2cc 100644
 a/prelude/tactics.v
+++ b/prelude/tactics.v
@@ 228,6 +228,74 @@ Ltac setoid_subst :=
 H : @equiv ?A ?e _ ?x  _ => symmetry in H; setoid_subst_aux (@equiv A e) x
end.
+
+(** f_equiv solves goals of the form "f _ = f _", for any relation and any
+ number of arguments, by looking for appropriate "Proper" instances.
+ If it cannot solve an equality, it will leave that to the user. *)
+Ltac f_equiv :=
+ (* Deal with "pointwise_relation" *)
+ try lazymatch goal with
+   pointwise_relation _ _ _ _ => intros ?
+ end;
+ (* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *)
+ first [ reflexivity  assumption  symmetry; assumption 
+ match goal with
+ (* We support matches on both sides, *if* they concern the same
+ or provably equal variables.
+ TODO: We should support different variables, provided that we can
+ derive contradictions for the offdiagonal cases. *)
+   ?R (match ?x with _ => _ end) (match ?x with _ => _ end) =>
+ destruct x; f_equiv
+   ?R (match ?x with _ => _ end) (match ?y with _ => _ end) =>
+ subst y; f_equiv
+ (* First assume that the arguments need the same relation as the result *)
+   ?R (?f ?x) (?f _) =>
+ let H := fresh "Proper" in
+ assert (Proper (R ==> R) f) as H by (eapply _);
+ apply H; clear H; f_equiv
+   ?R (?f ?x ?y) (?f _ _) =>
+ let H := fresh "Proper" in
+ assert (Proper (R ==> R ==> R) f) as H by (eapply _);
+ apply H; clear H; f_equiv
+ (* Next, try to infer the relation *)
+ (* TODO: If some of the arguments are the same, we could also
+ query for "pointwise_relation"'s. But that leads to a combinatorial
+ explosion about which arguments are and which are not the same. *)
+   ?R (?f ?x) (?f _) =>
+ let R1 := fresh "R" in let H := fresh "Proper" in
+ let T := type of x in evar (R1: relation T);
+ assert (Proper (R1 ==> R) f) as H by (subst R1; eapply _);
+ subst R1; apply H; clear H; f_equiv
+   ?R (?f ?x ?y) (?f _ _) =>
+ let R1 := fresh "R" in let R2 := fresh "R" in
+ let H := fresh "Proper" in
+ let T1 := type of x in evar (R1: relation T1);
+ let T2 := type of y in evar (R2: relation T2);
+ assert (Proper (R1 ==> R2 ==> R) f) as H by (subst R1 R2; eapply _);
+ subst R1 R2; apply H; clear H; f_equiv
+ end  idtac (* Let the user solve this goal *)
+ ].
+
+(** solve_proper solves goals of the form "Proper (R1 ==> R2)", for any
+ number of relations. All the actual work is done by f_equiv;
+ solve_proper just introduces the assumptions and unfolds the first
+ head symbol. *)
+Ltac solve_proper :=
+ (* Introduce everything *)
+ intros;
+ repeat lazymatch goal with
+   Proper _ _ => intros ???
+   (_ ==> _)%signature _ _ => intros ???
+ end;
+ (* Unfold the head symbol, which is the one we are proving a new property about *)
+ lazymatch goal with
+   ?R (?f _ _ _ _) (?f _ _ _ _) => unfold f
+   ?R (?f _ _ _) (?f _ _ _) => unfold f
+   ?R (?f _ _) (?f _ _) => unfold f
+   ?R (?f _) (?f _) => unfold f
+ end;
+ solve [ f_equiv ].
+
(** Given a tactic [tac2] generating a list of terms, [iter tac1 tac2]
runs [tac x] for each element [x] until [tac x] succeeds. If it does not
suceed for any element of the generated list, the whole tactic wil fail. *)
diff git a/program_logic/saved_prop.v b/program_logic/saved_prop.v
index b7254b59..59e20923 100644
 a/program_logic/saved_prop.v
+++ b/program_logic/saved_prop.v
@@ 43,6 +43,6 @@ Section saved_prop.
rewrite agree_equivI later_equivI /=; apply later_mono.
rewrite {2}(iProp_fold_unfold P) {2}(iProp_fold_unfold Q).
apply (eq_rewrite (iProp_unfold P) (iProp_unfold Q) (λ Q' : iPreProp Λ _,
 iProp_fold (iProp_unfold P) ≡ iProp_fold Q')%I); solve_ne  auto with I.
+ iProp_fold (iProp_unfold P) ≡ iProp_fold Q')%I); solve_proper  auto with I.
Qed.
End saved_prop.

GitLab