### 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`
parent cb9adddc
 ... ... @@ -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) ... ...
 ... ... @@ -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. ... ...
 ... ... @@ -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'). ... ...
 ... ... @@ -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 : ... ...
 ... ... @@ -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 off-diagonal 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. *) ... ...
 ... ... @@ -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.
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