diff --git a/iris/logic.v b/iris/logic.v index c2d6c8b57608a513b268caa52ccfa6862fc48363..02bdc0f44126ce3d803f1e4aadf0afc904d670bf 100644 --- a/iris/logic.v +++ b/iris/logic.v @@ -92,7 +92,7 @@ Solve Obligations with naive_solver eauto 2 using (dist_le (A:=B)). Program Definition iprop_sep {A} (P Q : iProp A) : iProp A := {| iprop_holds n x := ∃ x1 x2, x ={n}= x1 ⋅ x2 ∧ P n x1 ∧ Q n x2 |}. Next Obligation. - by intros A P Q x y n (x1&x2&?&?&?) Hxy; exists x1 x2; rewrite <-Hxy. + by intros A P Q x y n (x1&x2&?&?&?) Hxy; exists x1, x2; rewrite <-Hxy. Qed. Next Obligation. intros A P Q x y n1 n2 Hxy ?? (x1&x2&Hx&?&?). @@ -100,7 +100,7 @@ Next Obligation. { rewrite ra_included_spec in Hxy; destruct Hxy as [z Hy]. exists (x2 ⋅ z); split; eauto using ra_included_l. apply dist_le with n1; auto. by rewrite (associative op), <-Hx, Hy. } - exists x1 x2'; split_ands; auto. + exists x1, x2'; split_ands; auto. * apply iprop_weaken with x1 n1; auto. by apply cmra_valid_op_l with x2'; rewrite <-Hy. * apply iprop_weaken with x2 n1; auto. @@ -194,7 +194,7 @@ Global Instance iprop_sep_ne n : Proper (dist n ==> dist n ==> dist n) (@iprop_sep A). Proof. intros P P' HP Q Q' HQ x n' ? Hx'; split; intros (x1&x2&Hx&?&?); - exists x1 x2; rewrite Hx in Hx'; split_ands; try apply HP; try apply HQ; + exists x1, x2; rewrite Hx in Hx'; split_ands; try apply HP; try apply HQ; eauto using cmra_valid_op_l, cmra_valid_op_r. Qed. Global Instance iprop_wand_ne n : @@ -262,27 +262,27 @@ Proof. intros P x n Hvalid; split. * intros (x1&x2&Hx&_&?); rewrite Hx in Hvalid |- *. apply iprop_weaken with x2 n; auto using ra_included_r. - * by intros ?; exists (unit x) x; rewrite ra_unit_l. + * by intros ?; exists (unit x), x; rewrite ra_unit_l. Qed. Global Instance iprop_sep_commutative : Commutative (≡) (@iprop_sep A). Proof. by intros P Q x n ?; split; - intros (x1&x2&?&?&?); exists x2 x1; rewrite (commutative op). + intros (x1&x2&?&?&?); exists x2, x1; rewrite (commutative op). Qed. Global Instance iprop_sep_associative : Associative (≡) (@iprop_sep A). Proof. intros P Q R x n ?; split. - * intros (x1&x2&Hx&?&y1&y2&Hy&?&?); exists (x1 ⋅ y1) y2; split_ands; auto. + * intros (x1&x2&Hx&?&y1&y2&Hy&?&?); exists (x1 ⋅ y1), y2; split_ands; auto. + by rewrite <-(associative op), <-Hy, <-Hx. - + by exists x1 y1. - * intros (x1&x2&Hx&(y1&y2&Hy&?&?)&?); exists y1 (y2 ⋅ x2); split_ands; auto. + + by exists x1, y1. + * intros (x1&x2&Hx&(y1&y2&Hy&?&?)&?); exists y1, (y2 ⋅ x2); split_ands; auto. + by rewrite (associative op), <-Hy, <-Hx. - + by exists y2 x2. + + by exists y2, x2. Qed. Lemma iprop_wand_intro P Q R : (R ★ P)%I ⊆ Q → R ⊆ (P -★ Q)%I. Proof. intros HPQ x n ?? x' n' ???; apply HPQ; auto. - exists x x'; split_ands; auto. + exists x, x'; split_ands; auto. eapply iprop_weaken with x n; eauto using cmra_valid_op_l. Qed. Lemma iprop_wand_elim P Q : ((P -★ Q) ★ P)%I ⊆ Q. @@ -291,21 +291,21 @@ Proof. Qed. Lemma iprop_sep_or P Q R : ((P ∨ Q) ★ R)%I ≡ ((P ★ R) ∨ (Q ★ R))%I. Proof. - split; [by intros (x1&x2&Hx&[?|?]&?); [left|right]; exists x1 x2|]. - intros [(x1&x2&Hx&?&?)|(x1&x2&Hx&?&?)]; exists x1 x2; split_ands; + split; [by intros (x1&x2&Hx&[?|?]&?); [left|right]; exists x1, x2|]. + intros [(x1&x2&Hx&?&?)|(x1&x2&Hx&?&?)]; exists x1, x2; split_ands; first [by left | by right | done]. Qed. Lemma iprop_sep_and P Q R : ((P ∧ Q) ★ R)%I ⊆ ((P ★ R) ∧ (Q ★ R))%I. -Proof. by intros x n ? (x1&x2&Hx&[??]&?); split; exists x1 x2. Qed. +Proof. by intros x n ? (x1&x2&Hx&[??]&?); split; exists x1, x2. Qed. Lemma iprop_sep_exist {B} (P : B → iProp A) Q : ((∃ b, P b) ★ Q)%I ≡ (∃ b, P b ★ Q)%I. Proof. - split; [by intros (x1&x2&Hx&[b ?]&?); exists b x1 x2|]. - intros [b (x1&x2&Hx&?&?)]; exists x1 x2; split_ands; by try exists b. + split; [by intros (x1&x2&Hx&[b ?]&?); exists b, x1, x2|]. + intros [b (x1&x2&Hx&?&?)]; exists x1, x2; split_ands; by try exists b. Qed. Lemma iprop_sep_forall `(P : B → iProp A) Q : ((∀ b, P b) ★ Q)%I ⊆ (∀ b, P b ★ Q)%I. -Proof. by intros x n ? (x1&x2&Hx&?&?); intros b; exists x1 x2. Qed. +Proof. by intros x n ? (x1&x2&Hx&?&?); intros b; exists x1, x2. Qed. (* Later *) Global Instance iprop_later_contractive : Contractive (@iprop_later A). @@ -345,12 +345,12 @@ Qed. Lemma iprop_later_sep P Q : (▷ (P ★ Q))%I ≡ (▷ P ★ ▷ Q)%I. Proof. intros x n ?; split. - * destruct n as [|n]; simpl; [by exists x x|intros (x1&x2&Hx&?&?)]. + * destruct n as [|n]; simpl; [by exists x, x|intros (x1&x2&Hx&?&?)]. destruct (cmra_extend_op x x1 x2 n) as ([y1 y2]&Hx'&Hy1&Hy2); auto using cmra_valid_S; simpl in *. - exists y1 y2; split; [by rewrite Hx'|by rewrite Hy1, Hy2]. + exists y1, y2; split; [by rewrite Hx'|by rewrite Hy1, Hy2]. * destruct n as [|n]; simpl; [done|intros (x1&x2&Hx&?&?)]. - exists x1 x2; eauto using (dist_S (A:=A)). + exists x1, x2; eauto using (dist_S (A:=A)). Qed. (* Always *) @@ -378,7 +378,7 @@ Lemma iprop_always_exist `(P : B → iProp A) : (□ ∃ b, P b)%I ≡ (∃ b, Proof. done. Qed. Lemma iprop_always_and_always_box P Q : (□ P ∧ Q)%I ⊆ (□ P ★ Q)%I. Proof. - intros x n ? [??]; exists (unit x) x; simpl in *. + intros x n ? [??]; exists (unit x), x; simpl in *. by rewrite ra_unit_l, ra_unit_idempotent. Qed. diff --git a/prelude/fin_maps.v b/prelude/fin_maps.v index a8a46783b024c78041b85dea55d7701dbe979f4d..b77edcd478d8e9eb4b1c6ec55cd71dfbbe524ec1 100644 --- a/prelude/fin_maps.v +++ b/prelude/fin_maps.v @@ -656,7 +656,7 @@ Lemma map_choose {A} (m : M A) : m ≠ ∅ → ∃ i x, m !! i = Some x. Proof. intros Hemp. destruct (map_to_list m) as [|[i x] l] eqn:Hm. { destruct Hemp; eauto using map_to_list_empty_inv. } - exists i x. rewrite <-elem_of_map_to_list, Hm. by left. + exists i, x. rewrite <-elem_of_map_to_list, Hm. by left. Qed. (** Properties of the imap function *) @@ -777,7 +777,7 @@ Proof. split; [|intros (i&x&?&?) Hm; specialize (Hm i x); tauto]. rewrite map_Forall_to_list. intros Hm. apply (not_Forall_Exists _), Exists_exists in Hm. - destruct Hm as ([i x]&?&?). exists i x. by rewrite <-elem_of_map_to_list. + destruct Hm as ([i x]&?&?). exists i, x. by rewrite <-elem_of_map_to_list. Qed. End map_Forall. diff --git a/prelude/hashset.v b/prelude/hashset.v index 0e34d90f8d8a686b0d7b6c6fcee51a22124ef9fb..345ba837ae1c8a26a6024d87679384cb05260abf 100644 --- a/prelude/hashset.v +++ b/prelude/hashset.v @@ -85,7 +85,7 @@ Proof. rewrite elem_of_list_intersection in Hx; naive_solver. } intros [(l&?&?) (k&?&?)]. assert (x ∈ list_intersection l k) by (by rewrite elem_of_list_intersection). - exists (list_intersection l k); split; [exists l k|]; split_ands; auto. + exists (list_intersection l k); split; [exists l, k|]; split_ands; auto. by rewrite option_guard_True by eauto using elem_of_not_nil. * unfold elem_of, hashset_elem_of, intersection, hashset_intersection. intros [m1 ?] [m2 ?] x; simpl. @@ -95,7 +95,7 @@ Proof. intros [(l&?&?) Hm2]; destruct (m2 !! hash x) as [k|] eqn:?; eauto. destruct (decide (x ∈ k)); [destruct Hm2; eauto|]. assert (x ∈ list_difference l k) by (by rewrite elem_of_list_difference). - exists (list_difference l k); split; [right; exists l k|]; split_ands; auto. + exists (list_difference l k); split; [right; exists l,k|]; split_ands; auto. by rewrite option_guard_True by eauto using elem_of_not_nil. * unfold elem_of at 2, hashset_elem_of, elements, hashset_elems. intros [m Hm] x; simpl. setoid_rewrite elem_of_list_bind. split. diff --git a/prelude/list.v b/prelude/list.v index 89f7a0a9a2ca4123081a9d35fcc99bf5d08ce2aa..25fe629b709e003cf0389e400427f548d33bd597 100644 --- a/prelude/list.v +++ b/prelude/list.v @@ -487,8 +487,8 @@ Lemma list_lookup_other l i x : length l ≠ 1 → l !! i = Some x → ∃ j y, j ≠ i ∧ l !! j = Some y. Proof. intros. destruct i, l as [|x0 [|x1 l]]; simplify_equality'. - * by exists 1 x1. - * by exists 0 x0. + * by exists 1, x1. + * by exists 0, x0. Qed. Lemma alter_app_l f l1 l2 i : i < length l1 → alter f i (l1 ++ l2) = alter f i l1 ++ l2. @@ -604,7 +604,7 @@ Proof. induction 1; rewrite ?elem_of_nil, ?elem_of_cons; intuition. Qed. Lemma elem_of_list_split l x : x ∈ l → ∃ l1 l2, l = l1 ++ x :: l2. Proof. induction 1 as [x l|x y l ? [l1 [l2 ->]]]; [by eexists [], l|]. - by exists (y :: l1) l2. + by exists (y :: l1), l2. Qed. Lemma elem_of_list_lookup_1 l x : x ∈ l → ∃ i, l !! i = Some x. Proof. @@ -1621,7 +1621,7 @@ Proof. split. * intros Hlk. induction k as [|y k IH]; inversion Hlk. + eexists [], k. by repeat constructor. - + destruct IH as (k1&k2&->&?); auto. by exists (y :: k1) k2. + + destruct IH as (k1&k2&->&?); auto. by exists (y :: k1), k2. * intros (k1&k2&->&?). by apply sublist_inserts_l, sublist_skip. Qed. Lemma sublist_app_r l k1 k2 : @@ -1633,9 +1633,9 @@ Proof. { eexists [], l. by repeat constructor. } rewrite sublist_cons_r. intros [?|(l' & ? &?)]; subst. + destruct (IH l k2) as (l1&l2&?&?&?); trivial; subst. - exists l1 l2. auto using sublist_cons. + exists l1, l2. auto using sublist_cons. + destruct (IH l' k2) as (l1&l2&?&?&?); trivial; subst. - exists (y :: l1) l2. auto using sublist_skip. + exists (y :: l1), l2. auto using sublist_skip. * intros (?&?&?&?&?); subst. auto using sublist_app. Qed. Lemma sublist_app_l l1 l2 k : @@ -1647,7 +1647,7 @@ Proof. { eexists [], k. by repeat constructor. } rewrite sublist_cons_l. intros (k1 & k2 &?&?); subst. destruct (IH l2 k2) as (h1 & h2 &?&?&?); trivial; subst. - exists (k1 ++ x :: h1) h2. rewrite <-(associative_L (++)). + exists (k1 ++ x :: h1), h2. rewrite <-(associative_L (++)). auto using sublist_inserts_l, sublist_skip. * intros (?&?&?&?&?); subst. auto using sublist_app. Qed. @@ -1865,7 +1865,7 @@ Proof. split. * rewrite contains_sublist_r. intros (l'&E&Hl'). rewrite sublist_app_r in Hl'. destruct Hl' as (l1&l2&?&?&?); subst. - exists l1 l2. eauto using sublist_contains. + exists l1, l2. eauto using sublist_contains. * intros (?&?&E&?&?). rewrite E. eauto using contains_app. Qed. Lemma contains_app_l l1 l2 k : @@ -1875,7 +1875,7 @@ Proof. split. * rewrite contains_sublist_l. intros (l'&Hl'&E). rewrite sublist_app_l in Hl'. destruct Hl' as (k1&k2&?&?&?); subst. - exists k1 k2. split. done. eauto using sublist_contains. + exists k1, k2. split. done. eauto using sublist_contains. * intros (?&?&E&?&?). rewrite E. eauto using contains_app. Qed. Lemma contains_app_inv_l l1 l2 k : @@ -2578,7 +2578,7 @@ Section fmap. Proof. revert l. induction k1 as [|y k1 IH]; simpl; [intros l ?; by eexists [],l|]. intros [|x l] ?; simplify_equality'. - destruct (IH l) as (l1&l2&->&->&->); [done|]. by exists (x :: l1) l2. + destruct (IH l) as (l1&l2&->&->&->); [done|]. by exists (x :: l1), l2. Qed. Lemma fmap_length l : length (f <\$> l) = length l. Proof. by induction l; f_equal'. Qed. @@ -3006,7 +3006,7 @@ Section zip_with. { intros l k ?. by eexists [], [], l, k. } intros [|x l] [|y k] ?; simplify_equality'. destruct (IH l k) as (l1&k1&l2&k2&->&->&->&->&?); [done |]. - exists (x :: l1) (y :: k1) l2 k2; simpl; auto with congruence. + exists (x :: l1), (y :: k1), l2, k2; simpl; auto with congruence. Qed. Lemma zip_with_inj `{!Injective2 (=) (=) (=) f} l1 l2 k1 k2 : length l1 = length k1 → length l2 = length k2 → diff --git a/prelude/natmap.v b/prelude/natmap.v index 94296e391dcba0c398c5bca7315a3e7a7da8a412..320b2cb87c2c3dcad9de9912591f8c0f03164279 100644 --- a/prelude/natmap.v +++ b/prelude/natmap.v @@ -19,7 +19,7 @@ Lemma natmap_wf_lookup {A} (l : natmap_raw A) : Proof. intros Hwf Hl. induction l as [|[x|] l IH]; simpl; [done| |]. { exists 0. simpl. eauto. } - destruct IH as (i&x&?); eauto using natmap_wf_inv; [|by exists (S i) x]. + destruct IH as (i&x&?); eauto using natmap_wf_inv; [|by exists (S i), x]. intros ->. by destruct Hwf. Qed. diff --git a/prelude/pmap.v b/prelude/pmap.v index 13e3a177759b50de63706d7df32084e03f8bcc0c..3cf4f3aa959657c7c89943f1c904856616a16fca 100644 --- a/prelude/pmap.v +++ b/prelude/pmap.v @@ -114,9 +114,9 @@ Proof. by destruct i. Qed. Lemma Pmap_ne_lookup {A} (t : Pmap_raw A) : Pmap_ne t → ∃ i x, t !! i = Some x. Proof. induction 1 as [? x ?| l r ? IHl | l r ? IHr]. - * intros. by exists 1 x. - * destruct IHl as [i [x ?]]. by exists (i~0) x. - * destruct IHr as [i [x ?]]. by exists (i~1) x. + * intros. by exists 1, x. + * destruct IHl as [i [x ?]]. by exists (i~0), x. + * destruct IHr as [i [x ?]]. by exists (i~1), x. Qed. Lemma Pmap_wf_eq_get {A} (t1 t2 : Pmap_raw A) :