From 176a588ce2d4d75a015669f5c978b583d00d1009 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Sun, 4 Dec 2016 16:56:34 +0100 Subject: [PATCH] New definition of contractive. Using this new definition we can express being contractive using a Proper. This has the following advantages: - It makes it easier to state that a function with multiple arguments is contractive (in all or some arguments). - A solve_contractive tactic can be implemented by extending the solve_proper tactic. --- algebra/ofe.v | 61 ++++++++++++++++++++++++++----------- algebra/sts.v | 2 +- base_logic/lib/boxes.v | 12 ++++---- base_logic/lib/fractional.v | 4 +-- base_logic/lib/wsat.v | 7 ++--- base_logic/primitive.v | 11 +++---- base_logic/upred.v | 4 +-- prelude/gmultiset.v | 4 +-- prelude/tactics.v | 34 +++++++++------------ program_logic/weakestpre.v | 18 +++++------ 10 files changed, 84 insertions(+), 73 deletions(-) diff --git a/algebra/ofe.v b/algebra/ofe.v index 8812dc5f..9e0ed004 100644 --- a/algebra/ofe.v +++ b/algebra/ofe.v @@ -83,6 +83,11 @@ Record chain (A : ofeT) := { Arguments chain_car {_} _ _. Arguments chain_cauchy {_} _ _ _ _. +Program Definition chain_map {A B : ofeT} (f : A → B) + `{!∀ n, Proper (dist n ==> dist n) f} (c : chain A) : chain B := + {| chain_car n := f (c n) |}. +Next Obligation. by intros A B f Hf c n i ?; apply Hf, chain_cauchy. Qed. + Notation Compl A := (chain A%type → A). Class Cofe (A : ofeT) := { compl : Compl A; @@ -140,8 +145,14 @@ Section cofe. End cofe. (** Contractive functions *) -Class Contractive {A B : ofeT} (f : A → B) := - contractive n x y : (∀ i, i < n → x ≡{i}≡ y) → f x ≡{n}≡ f y. +Definition dist_later {A : ofeT} (n : nat) (x y : A) : Prop := + match n with 0 => True | S n => x ≡{n}≡ y end. +Arguments dist_later _ !_ _ _ /. + +Global Instance dist_later_equivalence A n : Equivalence (@dist_later A n). +Proof. destruct n as [|n]. by split. apply dist_equivalence. Qed. + +Notation Contractive f := (∀ n, Proper (dist_later n ==> dist n) f). Instance const_contractive {A B : ofeT} (x : A) : Contractive (@const A B x). Proof. by intros n y1 y2. Qed. @@ -151,9 +162,9 @@ Section contractive. Implicit Types x y : A. Lemma contractive_0 x y : f x ≡{0}≡ f y. - Proof. eauto using contractive with omega. Qed. + Proof. by apply (_ : Contractive f). Qed. Lemma contractive_S n x y : x ≡{n}≡ y → f x ≡{S n}≡ f y. - Proof. eauto using contractive, dist_le with omega. Qed. + Proof. intros. by apply (_ : Contractive f). Qed. Global Instance contractive_ne n : Proper (dist n ==> dist n) f | 100. Proof. by intros x y ?; apply dist_S, contractive_S. Qed. @@ -161,18 +172,27 @@ Section contractive. Proof. apply (ne_proper _). Qed. End contractive. -(** Mapping a chain *) -Program Definition chain_map {A B : ofeT} (f : A → B) - `{!∀ n, Proper (dist n ==> dist n) f} (c : chain A) : chain B := - {| chain_car n := f (c n) |}. -Next Obligation. by intros A B f Hf c n i ?; apply Hf, chain_cauchy. Qed. +Ltac f_contractive := + match goal with + | |- ?f _ ≡{_}≡ ?f _ => apply (_ : Proper (dist_later _ ==> _) f) + | |- ?f _ _ ≡{_}≡ ?f _ _ => apply (_ : Proper (dist_later _ ==> _ ==> _) f) + | |- ?f _ _ ≡{_}≡ ?f _ _ => apply (_ : Proper (_ ==> dist_later _ ==> _) f) + end; + try match goal with + | |- dist_later ?n ?x ?y => destruct n as [|n]; [done|change (x ≡{n}≡ y)] + end; + try reflexivity. + +Ltac solve_contractive := + preprocess_solve_proper; + solve [repeat (first [f_contractive|f_equiv]; try eassumption)]. (** Fixpoint *) Program Definition fixpoint_chain {A : ofeT} `{Inhabited A} (f : A → A) `{!Contractive f} : chain A := {| chain_car i := Nat.iter (S i) f inhabitant |}. Next Obligation. intros A ? f ? n. - induction n as [|n IH]; intros [|i] ?; simpl in *; try reflexivity || omega. + induction n as [|n IH]=> -[|i] //= ?; try omega. - apply (contractive_0 f). - apply (contractive_S f), IH; auto with omega. Qed. @@ -513,7 +533,7 @@ Instance ofe_morCF_contractive F1 F2 : cFunctorContractive (ofe_morCF F1 F2). Proof. intros ?? A1 A2 B1 B2 n [f g] [f' g'] Hfg; simpl in *. - apply ofe_morC_map_ne; apply cFunctor_contractive=>i ?; split; by apply Hfg. + apply ofe_morC_map_ne; apply cFunctor_contractive; destruct n, Hfg; by split. Qed. (** Sum *) @@ -606,6 +626,7 @@ Qed. (** Discrete cofe *) Section discrete_cofe. Context `{Equiv A, @Equivalence A (≡)}. + Instance discrete_dist : Dist A := λ n x y, x ≡ y. Definition discrete_ofe_mixin : OfeMixin A. Proof. @@ -614,7 +635,7 @@ Section discrete_cofe. - done. - done. Qed. - + Global Program Instance discrete_cofe : Cofe (OfeT A discrete_ofe_mixin) := { compl c := c 0 }. Next Obligation. @@ -743,17 +764,17 @@ Section later. Context {A : ofeT}. Instance later_equiv : Equiv (later A) := λ x y, later_car x ≡ later_car y. Instance later_dist : Dist (later A) := λ n x y, - match n with 0 => True | S n => later_car x ≡{n}≡ later_car y end. + dist_later n (later_car x) (later_car y). Definition later_ofe_mixin : OfeMixin (later A). Proof. split. - intros x y; unfold equiv, later_equiv; rewrite !equiv_dist. split. intros Hxy [|n]; [done|apply Hxy]. intros Hxy n; apply (Hxy (S n)). - - intros [|n]; [by split|split]; unfold dist, later_dist. + - split; rewrite /dist /later_dist. + by intros [x]. + by intros [x] [y]. + by intros [x] [y] [z] ??; trans y. - - intros [|n] [x] [y] ?; [done|]; unfold dist, later_dist; by apply dist_S. + - intros [|n] [x] [y] ?; [done|]; rewrite /dist /later_dist; by apply dist_S. Qed. Canonical Structure laterC : ofeT := OfeT (later A) later_ofe_mixin. @@ -767,9 +788,13 @@ Section later. Qed. Global Instance Next_contractive : Contractive (@Next A). - Proof. intros [|n] x y Hxy; [done|]; apply Hxy; lia. Qed. + Proof. by intros [|n] x y. Qed. Global Instance Later_inj n : Inj (dist n) (dist (S n)) (@Next A). Proof. by intros x y. Qed. + + Lemma contractive_alt {B : ofeT} (f : A → B) : + Contractive f ↔ (∀ n x y, Next x ≡{n}≡ Next y → f x ≡{n}≡ f y). + Proof. done. Qed. End later. Arguments laterC : clear implicits. @@ -812,8 +837,8 @@ Qed. Instance laterCF_contractive F : cFunctorContractive (laterCF F). Proof. - intros A1 A2 B1 B2 n fg fg' Hfg. - apply laterC_map_contractive => i ?. by apply cFunctor_ne, Hfg. + intros A1 A2 B1 B2 n fg fg' Hfg. apply laterC_map_contractive. + destruct n as [|n]; simpl in *; first done. apply cFunctor_ne, Hfg. Qed. (** Notation for writing functors *) diff --git a/algebra/sts.v b/algebra/sts.v index fd6046d1..d19e1974 100644 --- a/algebra/sts.v +++ b/algebra/sts.v @@ -78,7 +78,7 @@ 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=> // s1 s2 Hs. by apply up_preserving. Qed. Global Instance up_set_proper : Proper ((≡) ==> (≡) ==> (≡)) up_set. Proof. diff --git a/base_logic/lib/boxes.v b/base_logic/lib/boxes.v index 8e53d534..8c3bc73b 100644 --- a/base_logic/lib/boxes.v +++ b/base_logic/lib/boxes.v @@ -47,17 +47,17 @@ Global Instance box_own_prop_ne n γ : Proper (dist n ==> dist n) (box_own_prop Proof. solve_proper. Qed. Global Instance box_inv_ne n γ : Proper (dist n ==> dist n) (slice_inv γ). Proof. solve_proper. Qed. + Global Instance slice_ne n γ : Proper (dist n ==> dist n) (slice N γ). Proof. solve_proper. Qed. -Global Instance box_contractive f : Contractive (box N f). -Proof. - intros n P1 P2 HP1P2. apply exist_ne. intros Φ. f_equiv; last done. - apply contractive. intros n' ?. by rewrite HP1P2. -Qed. - Global Instance slice_persistent γ P : PersistentP (slice N γ P). Proof. apply _. Qed. +Global Instance box_contractive f : Contractive (box N f). +Proof. solve_contractive. Qed. +Global Instance box_ne n f : Proper (dist n ==> dist n) (box N f). +Proof. apply (contractive_ne _). Qed. + Lemma box_own_auth_agree γ b1 b2 : box_own_auth γ (● Excl' b1) ∗ box_own_auth γ (◯ Excl' b2) ⊢ ⌜b1 = b2⌝. Proof. diff --git a/base_logic/lib/fractional.v b/base_logic/lib/fractional.v index a2247bf4..15e11691 100644 --- a/base_logic/lib/fractional.v +++ b/base_logic/lib/fractional.v @@ -55,7 +55,6 @@ Section fractional. Proof. done. Qed. (** Proof mode instances *) - Global Instance from_sep_fractional_fwd P P1 P2 Φ q1 q2 : AsFractional P Φ (q1 + q2) → Fractional Φ → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 → @@ -97,12 +96,11 @@ Section fractional. AsFractional R Φ r → AsFractional PP' Φ (p + p') → Fractional Φ → Frame R (Φ p') Q → MakeSep (Φ p) Q PQ → Frame R PP' PQ. Proof. - rewrite /Frame=>->->-><-<-. rewrite !assoc. f_equiv. by rewrite comm. done. + rewrite /Frame=>->->-><-<-. rewrite !assoc. f_equiv. by rewrite comm. Qed. Global Instance frame_fractional_half P Q R Φ p: AsFractional R Φ (p/2) → AsFractional P Φ p → Fractional Φ → AsFractional Q Φ (p/2)%Qp → Frame R P Q. Proof. by rewrite /Frame -{2}(Qp_div_2 p)=>->->->->. Qed. - End fractional. diff --git a/base_logic/lib/wsat.v b/base_logic/lib/wsat.v index 4489034a..c456f19f 100644 --- a/base_logic/lib/wsat.v +++ b/base_logic/lib/wsat.v @@ -44,11 +44,10 @@ Context `{invG Σ}. Implicit Types P : iProp Σ. (* Invariants *) +Instance invariant_unfold_contractive : Contractive (@invariant_unfold Σ). +Proof. solve_contractive. Qed. Global Instance ownI_contractive i : Contractive (@ownI Σ _ i). -Proof. - intros n P Q HPQ. rewrite /ownI /invariant_unfold. do 4 f_equiv. - apply Next_contractive=> j ?; by rewrite (HPQ j). -Qed. +Proof. solve_contractive. Qed. Global Instance ownI_persistent i P : PersistentP (ownI i P). Proof. rewrite /ownI. apply _. Qed. diff --git a/base_logic/primitive.v b/base_logic/primitive.v index 510424fe..85dfdb49 100644 --- a/base_logic/primitive.v +++ b/base_logic/primitive.v @@ -284,8 +284,8 @@ Proof. Qed. Global Instance later_contractive : Contractive (@uPred_later M). Proof. - intros n P Q HPQ; unseal; split=> -[|n'] x ??; simpl; [done|]. - apply (HPQ n'); eauto using cmra_validN_S. + unseal; intros [|n] P Q HPQ; split=> -[|n'] x ?? //=; try omega. + apply HPQ; eauto using cmra_validN_S. Qed. Global Instance later_proper' : Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_later M) := ne_proper _. @@ -583,12 +583,11 @@ Proof. unseal. by destruct mx. Qed. (* Contractive functions *) Lemma contractiveI {A B : ofeT} (f : A → B) : - Contractive f ↔ (∀ x y, ▷ (x ≡ y) ⊢ f x ≡ f y). + Contractive f ↔ (∀ a b, ▷ (a ≡ b) ⊢ f a ≡ f b). Proof. split; unseal; intros Hf. - - intros x y; split=> -[|n] z _ /=; eauto using contractive_0, contractive_S. - - intros [|i] x y Hxy; apply (uPred_in_entails _ _ (Hf x y) _ ∅); - simpl; eauto using ucmra_unit_validN. + - intros a b; split=> n x _; apply Hf. + - intros i a b; eapply Hf, ucmra_unit_validN. Qed. (* Functions *) diff --git a/base_logic/upred.v b/base_logic/upred.v index f943c438..ac98bddd 100644 --- a/base_logic/upred.v +++ b/base_logic/upred.v @@ -118,8 +118,8 @@ Qed. Instance uPredCF_contractive F : urFunctorContractive F → cFunctorContractive (uPredCF F). Proof. - intros ? A1 A2 B1 B2 n P Q HPQ. - apply uPredC_map_ne, urFunctor_contractive=> i ?; split; by apply HPQ. + intros ? A1 A2 B1 B2 n P Q HPQ. apply uPredC_map_ne, urFunctor_contractive. + destruct n; split; by apply HPQ. Qed. (** logical entailement *) diff --git a/prelude/gmultiset.v b/prelude/gmultiset.v index 84c7be8e..52a77a7a 100644 --- a/prelude/gmultiset.v +++ b/prelude/gmultiset.v @@ -185,8 +185,8 @@ Proof. rewrite !map_to_list_insert, !bind_cons by (by rewrite ?lookup_union_with, ?lookup_delete, ?HX). rewrite (assoc_L _), <-(comm (++) (f (_,n'))), <-!(assoc_L _), <-IH. - rewrite (assoc_L _); f_equiv; [rewrite (comm _); simpl|done]. - by rewrite replicate_plus, Permutation_middle. + rewrite (assoc_L _). f_equiv. + rewrite (comm _); simpl. by rewrite replicate_plus, Permutation_middle. - rewrite <-insert_union_with_l, !map_to_list_insert, !bind_cons by (by rewrite ?lookup_union_with, ?HX, ?HY). by rewrite <-(assoc_L (++)), <-IH. diff --git a/prelude/tactics.v b/prelude/tactics.v index 38175757..7ca9b524 100644 --- a/prelude/tactics.v +++ b/prelude/tactics.v @@ -273,6 +273,7 @@ favor the second because the relation (dist) stays the same. *) Ltac f_equiv := match goal with | _ => reflexivity + | |- pointwise_relation _ _ _ _ => intros ? (* We support matches on both sides, *if* they concern the same variable, or variables in some relation. *) | |- ?R (match ?x with _ => _ end) (match ?x with _ => _ end) => @@ -301,26 +302,12 @@ Ltac f_equiv := (* In case the function symbol differs, but the arguments are the same, maybe we have a pointwise_relation in our context. *) | H : pointwise_relation _ ?R ?f ?g |- ?R (?f ?x) (?g ?x) => apply H - end. - -(** auto_proper solves goals of the form "f _ = f _", for any relation and any - number of arguments, by repeatedly applying f_equiv and handling trivial cases. - If it cannot solve an equality, it will leave that to the user. *) -Ltac auto_equiv := - (* Deal with "pointwise_relation" *) - repeat lazymatch goal with - | |- pointwise_relation _ _ _ _ => intros ? end; - (* Normalize away equalities. *) - simplify_eq; - (* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *) - try (f_equiv; fast_done || auto_equiv). - -(** solve_proper solves goals of the form "Proper (R1 ==> R2)", for any - number of relations. All the actual work is done by auto_equiv; - solve_proper just introduces the assumptions and unfolds the first - head symbol. *) -Ltac solve_proper := + try reflexivity. + +(* The tactic [preprocess_solve_proper] unfolds the first head symbol, so that +we proceed by repeatedly using [f_equiv]. *) +Ltac preprocess_solve_proper := (* Introduce everything *) intros; repeat lazymatch goal with @@ -340,7 +327,14 @@ Ltac solve_proper := | |- ?R (?f _ _) (?f _ _) => unfold f | |- ?R (?f _) (?f _) => unfold f end; - solve [ auto_equiv ]. + simplify_eq. + +(** The tactic [solve_proper] solves goals of the form "Proper (R1 ==> R2)", for +any number of relations. The actual work is done by repeatedly applying +[f_equiv]. *) +Ltac solve_proper := + preprocess_solve_proper; + solve [repeat (f_equiv; try eassumption)]. (** The tactic [intros_revert tac] introduces all foralls/arrows, performs tac, and then reverts them. *) diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v index 9c3070b3..6999d231 100644 --- a/program_logic/weakestpre.v +++ b/program_logic/weakestpre.v @@ -37,11 +37,7 @@ Definition wp_pre `{irisG Λ Σ} Local Instance wp_pre_contractive `{irisG Λ Σ} : Contractive wp_pre. Proof. rewrite /wp_pre=> n wp wp' Hwp E e1 Φ. - apply or_ne, and_ne, forall_ne; auto=> σ1; apply wand_ne; auto. - apply fupd_ne, sep_ne, later_contractive; auto=> i ?. - apply forall_ne=> e2; apply forall_ne=> σ2; apply forall_ne=> efs. - apply wand_ne, fupd_ne, sep_ne, sep_ne; auto; first by apply Hwp. - apply big_opL_ne=> ? ef. by apply Hwp. + repeat (f_contractive || f_equiv); apply Hwp. Qed. Definition wp_def `{irisG Λ Σ} : @@ -138,12 +134,12 @@ Global Instance wp_ne E e n : Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ _ E e). Proof. revert e. induction (lt_wf n) as [n _ IH]=> e Φ Ψ HΦ. - rewrite !wp_unfold /wp_pre. apply or_ne, and_ne; auto; first solve_proper. - apply forall_ne=> σ1. - apply wand_ne, fupd_ne, sep_ne, later_contractive; auto=> i ?. - apply forall_ne=> e2; apply forall_ne=> σ2; apply forall_ne=> ef. - apply wand_ne, fupd_ne, sep_ne, sep_ne; auto. - apply IH; [done|]=> v. eapply dist_le; eauto with omega. + rewrite !wp_unfold /wp_pre. + (* FIXME: figure out a way to properly automate this proof *) + (* FIXME: reflexivity, as being called many times by f_equiv and f_contractive + is very slow here *) + do 18 (f_contractive || f_equiv). apply IH; first lia. + intros v. eapply dist_le; eauto with omega. Qed. Global Instance wp_proper E e : Proper (pointwise_relation _ (≡) ==> (≡)) (@wp Λ Σ _ E e). -- GitLab