Commit 6bbc6b49 authored by Ralf Jung's avatar Ralf Jung

tune "Proof using" directives to minimize differences to previous types of all lemmas

parent 5213177f
Pipeline #3586 passed with stage
in 10 minutes and 31 seconds
From iris.algebra Require Export ofe.
(* FIXME: This file needs a 'Proof Using' hint, but the default we use
everywhere makes for lots of extra ssumptions. *)
Set Default Proof Using "Type".
Record solution (F : cFunctor) := Solution {
solution_car :> ofeT;
......@@ -22,7 +21,7 @@ Notation map := (cFunctor_map F).
Fixpoint A (k : nat) : ofeT :=
match k with 0 => unitC | S k => F (A k) end.
Local Instance: k, Cofe (A k).
Proof. induction 0; apply _. Defined.
Proof using Fcofe. induction 0; apply _. Defined.
Fixpoint f (k : nat) : A k -n> A (S k) :=
match k with 0 => CofeMor (λ _, inhabitant) | S k => map (g k,f k) end
with g (k : nat) : A (S k) -n> A k :=
......@@ -34,12 +33,12 @@ Arguments f : simpl never.
Arguments g : simpl never.
Lemma gf {k} (x : A k) : g k (f k x) x.
Proof.
Proof using Fcontr.
induction k as [|k IH]; simpl in *; [by destruct x|].
rewrite -cFunctor_compose -{2}[x]cFunctor_id. by apply (contractive_proper map).
Qed.
Lemma fg {k} (x : A (S (S k))) : f (S k) (g (S k) x) {k} x.
Proof.
Proof using Fcontr.
induction k as [|k IH]; simpl.
- rewrite f_S g_S -{2}[x]cFunctor_id -cFunctor_compose.
apply (contractive_0 map).
......@@ -88,11 +87,11 @@ Fixpoint ff {k} (i : nat) : A k -n> A (i + k) :=
Fixpoint gg {k} (i : nat) : A (i + k) -n> A k :=
match i with 0 => cid | S i => gg i g (i + k) end.
Lemma ggff {k i} (x : A k) : gg i (ff i x) x.
Proof. induction i as [|i IH]; simpl; [done|by rewrite (gf (ff i x)) IH]. Qed.
Proof using Fcontr. induction i as [|i IH]; simpl; [done|by rewrite (gf (ff i x)) IH]. Qed.
Lemma f_tower k (X : tower) : f (S k) (X (S k)) {k} X (S (S k)).
Proof. intros. by rewrite -(fg (X (S (S k)))) -(g_tower X). Qed.
Proof using Fcontr. intros. by rewrite -(fg (X (S (S k)))) -(g_tower X). Qed.
Lemma ff_tower k i (X : tower) : ff i (X (S k)) {k} X (i + S k).
Proof.
Proof using Fcontr.
intros; induction i as [|i IH]; simpl; [done|].
by rewrite IH Nat.add_succ_r (dist_le _ _ _ _ (f_tower _ X)); last omega.
Qed.
......@@ -138,7 +137,7 @@ Definition embed_coerce {k} (i : nat) : A k -n> A i :=
end.
Lemma g_embed_coerce {k i} (x : A k) :
g i (embed_coerce (S i) x) embed_coerce i x.
Proof.
Proof using Fcontr.
unfold embed_coerce; destruct (le_lt_dec (S i) k), (le_lt_dec i k); simpl.
- symmetry; by erewrite (@gg_gg _ _ 1 (k - S i)); simpl.
- exfalso; lia.
......@@ -206,7 +205,7 @@ Instance fold_ne : Proper (dist n ==> dist n) fold.
Proof. by intros n X Y HXY k; rewrite /fold /= HXY. Qed.
Theorem result : solution F.
Proof.
Proof using All.
apply (Solution F T _ (CofeMor unfold) (CofeMor fold)).
- move=> X /=. rewrite equiv_dist=> n k; rewrite /unfold /fold /=.
rewrite -g_tower -(gg_tower _ n); apply (_ : Proper (_ ==> _) (g _)).
......
......@@ -358,34 +358,34 @@ Section freshness.
Lemma alloc_updateP' m x :
x m ~~>: λ m', i, m' = <[i:=x]>m m !! i = None.
Proof. eauto using alloc_updateP. Qed.
Lemma alloc_unit_singleton_updateP (P : A Prop) (Q : gmap K A Prop) u i :
u LeftId () u ()
u ~~>: P ( y, P y Q {[ i := y ]}) ~~>: Q.
Proof.
intros ?? Hx HQ. apply cmra_total_updateP=> n gf Hg.
destruct (Hx n (gf !! i)) as (y&?&Hy).
{ move:(Hg i). rewrite !left_id.
case: (gf !! i)=>[x|]; rewrite /= ?left_id //.
intros; by apply cmra_valid_validN. }
exists {[ i := y ]}; split; first by auto.
intros i'; destruct (decide (i' = i)) as [->|].
- rewrite lookup_op lookup_singleton.
move:Hy; case: (gf !! i)=>[x|]; rewrite /= ?right_id //.
- move:(Hg i'). by rewrite !lookup_op lookup_singleton_ne // !left_id.
Qed.
Lemma alloc_unit_singleton_updateP' (P: A Prop) u i :
u LeftId () u ()
u ~~>: P ~~>: λ m, y, m = {[ i := y ]} P y.
Proof. eauto using alloc_unit_singleton_updateP. Qed.
Lemma alloc_unit_singleton_update (u : A) i (y : A) :
u LeftId () u () u ~~> y (:gmap K A) ~~> {[ i := y ]}.
Proof.
rewrite !cmra_update_updateP;
eauto using alloc_unit_singleton_updateP with subst.
Qed.
End freshness.
Lemma alloc_unit_singleton_updateP (P : A Prop) (Q : gmap K A Prop) u i :
u LeftId () u ()
u ~~>: P ( y, P y Q {[ i := y ]}) ~~>: Q.
Proof.
intros ?? Hx HQ. apply cmra_total_updateP=> n gf Hg.
destruct (Hx n (gf !! i)) as (y&?&Hy).
{ move:(Hg i). rewrite !left_id.
case: (gf !! i)=>[x|]; rewrite /= ?left_id //.
intros; by apply cmra_valid_validN. }
exists {[ i := y ]}; split; first by auto.
intros i'; destruct (decide (i' = i)) as [->|].
- rewrite lookup_op lookup_singleton.
move:Hy; case: (gf !! i)=>[x|]; rewrite /= ?right_id //.
- move:(Hg i'). by rewrite !lookup_op lookup_singleton_ne // !left_id.
Qed.
Lemma alloc_unit_singleton_updateP' (P: A Prop) u i :
u LeftId () u ()
u ~~>: P ~~>: λ m, y, m = {[ i := y ]} P y.
Proof. eauto using alloc_unit_singleton_updateP. Qed.
Lemma alloc_unit_singleton_update (u : A) i (y : A) :
u LeftId () u () u ~~> y (:gmap K A) ~~> {[ i := y ]}.
Proof.
rewrite !cmra_update_updateP;
eauto using alloc_unit_singleton_updateP with subst.
Qed.
Lemma alloc_local_update m1 m2 i x :
m1 !! i = None x (m1,m2) ~l~> (<[i:=x]>m1, <[i:=x]>m2).
Proof.
......
......@@ -43,8 +43,6 @@ Section iprod_cofe.
Qed.
(** Properties of iprod_insert. *)
Context `{EqDecision A}.
Global Instance iprod_insert_ne n x :
Proper (dist n ==> dist n ==> dist n) (iprod_insert x).
Proof.
......
......@@ -255,6 +255,8 @@ End fixpoint.
(** Mutual fixpoints *)
Section fixpoint2.
Local Unset Default Proof Using.
Context `{Cofe A, Cofe B, !Inhabited A, !Inhabited B}.
Context (fA : A B A).
Context (fB : A B B).
......
......@@ -107,7 +107,7 @@ Section total_updates.
rewrite cmra_total_updateP; setoid_rewrite <-cmra_discrete_valid_iff.
naive_solver eauto using 0.
Qed.
Lemma cmra_discrete_update `{CMRADiscrete A} (x y : A) :
Lemma cmra_discrete_update (x y : A) :
x ~~> y z, (x z) (y z).
Proof.
rewrite cmra_total_update; setoid_rewrite <-cmra_discrete_valid_iff.
......
......@@ -16,7 +16,7 @@ Instance subG_stsΣ Σ sts :
Proof. intros ?%subG_inG ?. by split. Qed.
Section definitions.
Context `{invG Σ, stsG Σ sts} (γ : gname).
Context `{stsG Σ sts} (γ : gname).
Definition sts_ownS (S : sts.states sts) (T : sts.tokens sts) : iProp Σ :=
own γ (sts_frag S T).
......@@ -24,7 +24,7 @@ Section definitions.
own γ (sts_frag_up s T).
Definition sts_inv (φ : sts.state sts iProp Σ) : iProp Σ :=
( s, own γ (sts_auth s ) φ s)%I.
Definition sts_ctx (N : namespace) (φ: sts.state sts iProp Σ) : iProp Σ :=
Definition sts_ctx `{!invG Σ} (N : namespace) (φ: sts.state sts iProp Σ) : iProp Σ :=
inv N (sts_inv φ).
Global Instance sts_inv_ne n :
......@@ -37,13 +37,13 @@ Section definitions.
Proof. solve_proper. Qed.
Global Instance sts_own_proper s : Proper (() ==> (⊣⊢)) (sts_own s).
Proof. solve_proper. Qed.
Global Instance sts_ctx_ne n N :
Global Instance sts_ctx_ne `{!invG Σ} n N :
Proper (pointwise_relation _ (dist n) ==> dist n) (sts_ctx N).
Proof. solve_proper. Qed.
Global Instance sts_ctx_proper N :
Global Instance sts_ctx_proper `{!invG Σ} N :
Proper (pointwise_relation _ () ==> (⊣⊢)) (sts_ctx N).
Proof. solve_proper. Qed.
Global Instance sts_ctx_persistent N φ : PersistentP (sts_ctx N φ).
Global Instance sts_ctx_persistent `{!invG Σ} N φ : PersistentP (sts_ctx N φ).
Proof. apply _. Qed.
Global Instance sts_own_peristent s : PersistentP (sts_own s ).
Proof. apply _. Qed.
......
......@@ -32,7 +32,7 @@ Qed.
(** * Choice principles *)
Section choice.
Context `{Countable A} (P : A Prop) `{ x, Decision (P x)}.
Context `{Countable A} (P : A Prop).
Inductive choose_step: relation positive :=
| choose_step_None {p} : decode p = None choose_step (Psucc p) p
......@@ -50,6 +50,9 @@ Section choice.
constructor. intros j.
inversion 1 as [? Hd|? y Hd]; subst; auto with lia.
Qed.
Context `{ x, Decision (P x)}.
Fixpoint choose_go {i} (acc : Acc choose_step i) : A :=
match Some_dec (decode i) with
| inleft (xHx) =>
......
......@@ -118,7 +118,13 @@ Context `{FinMap K M}.
(** ** Setoids *)
Section setoid.
Context `{Equiv A} `{!Equivalence (() : relation A)}.
Context `{Equiv A}.
Lemma map_equiv_lookup_l (m1 m2 : M A) i x :
m1 m2 m1 !! i = Some x y, m2 !! i = Some y x y.
Proof. generalize (equiv_Some_inv_l (m1 !! i) (m2 !! i) x); naive_solver. Qed.
Context `{!Equivalence (() : relation A)}.
Global Instance map_equivalence : Equivalence (() : relation (M A)).
Proof.
split.
......@@ -173,9 +179,6 @@ Section setoid.
split; [intros Hm; apply map_eq; intros i|by intros ->].
by rewrite lookup_empty, <-equiv_None, Hm, lookup_empty.
Qed.
Lemma map_equiv_lookup_l (m1 m2 : M A) i x :
m1 m2 m1 !! i = Some x y, m2 !! i = Some y x y.
Proof. generalize (equiv_Some_inv_l (m1 !! i) (m2 !! i) x); naive_solver. Qed.
Global Instance map_fmap_proper `{Equiv B} (f : A B) :
Proper (() ==> ()) f Proper (() ==> ()) (fmap (M:=M) f).
Proof.
......
......@@ -171,13 +171,15 @@ Proof. apply finite_bijective. eauto. Qed.
(** Decidability of quantification over finite types *)
Section forall_exists.
Context `{Finite A} (P : A Prop) `{ x, Decision (P x)}.
Context `{Finite A} (P : A Prop).
Lemma Forall_finite : Forall P (enum A) ( x, P x).
Proof. rewrite Forall_forall. intuition auto using elem_of_enum. Qed.
Lemma Exists_finite : Exists P (enum A) ( x, P x).
Proof. rewrite Exists_exists. naive_solver eauto using elem_of_enum. Qed.
Context `{ x, Decision (P x)}.
Global Instance forall_dec: Decision ( x, P x).
Proof.
refine (cast_if (decide (Forall P (enum A))));
......
......@@ -735,6 +735,28 @@ End no_dup_dec.
(** ** Set operations on lists *)
Section list_set.
Lemma elem_of_list_intersection_with f l k x :
x list_intersection_with f l k x1 x2,
x1 l x2 k f x1 x2 = Some x.
Proof.
split.
- induction l as [|x1 l IH]; simpl; [by rewrite elem_of_nil|].
intros Hx. setoid_rewrite elem_of_cons.
cut (( x2, x2 k f x1 x2 = Some x)
x list_intersection_with f l k); [naive_solver|].
clear IH. revert Hx. generalize (list_intersection_with f l k).
induction k; simpl; [by auto|].
case_match; setoid_rewrite elem_of_cons; naive_solver.
- intros (x1&x2&Hx1&Hx2&Hx). induction Hx1 as [x1|x1 ? l ? IH]; simpl.
+ generalize (list_intersection_with f l k).
induction Hx2; simpl; [by rewrite Hx; left |].
case_match; simpl; try setoid_rewrite elem_of_cons; auto.
+ generalize (IH Hx). clear Hx IH Hx2.
generalize (list_intersection_with f l k).
induction k; simpl; intros; [done|].
case_match; simpl; rewrite ?elem_of_cons; auto.
Qed.
Context `{!EqDecision A}.
Lemma elem_of_list_difference l k x : x list_difference l k x l x k.
Proof.
......@@ -773,27 +795,6 @@ Section list_set.
- constructor. rewrite elem_of_list_intersection; intuition. done.
- done.
Qed.
Lemma elem_of_list_intersection_with f l k x :
x list_intersection_with f l k x1 x2,
x1 l x2 k f x1 x2 = Some x.
Proof.
split.
- induction l as [|x1 l IH]; simpl; [by rewrite elem_of_nil|].
intros Hx. setoid_rewrite elem_of_cons.
cut (( x2, x2 k f x1 x2 = Some x)
x list_intersection_with f l k); [naive_solver|].
clear IH. revert Hx. generalize (list_intersection_with f l k).
induction k; simpl; [by auto|].
case_match; setoid_rewrite elem_of_cons; naive_solver.
- intros (x1&x2&Hx1&Hx2&Hx). induction Hx1 as [x1|x1 ? l ? IH]; simpl.
+ generalize (list_intersection_with f l k).
induction Hx2; simpl; [by rewrite Hx; left |].
case_match; simpl; try setoid_rewrite elem_of_cons; auto.
+ generalize (IH Hx). clear Hx IH Hx2.
generalize (list_intersection_with f l k).
induction k; simpl; intros; [done|].
case_match; simpl; rewrite ?elem_of_cons; auto.
Qed.
End list_set.
(** ** Properties of the [filter] function *)
......@@ -2171,7 +2172,7 @@ Section Forall_Exists.
Lemma Forall_replicate n x : P x Forall P (replicate n x).
Proof. induction n; simpl; constructor; auto. Qed.
Lemma Forall_replicate_eq n (x : A) : Forall (x =) (replicate n x).
Proof. induction n; simpl; constructor; auto. Qed.
Proof using -(P). induction n; simpl; constructor; auto. Qed.
Lemma Forall_take n l : Forall P l Forall P (take n l).
Proof. intros Hl. revert n. induction Hl; intros [|?]; simpl; auto. Qed.
Lemma Forall_drop n l : Forall P l Forall P (drop n l).
......@@ -2741,7 +2742,7 @@ End Forall3.
(** Setoids *)
Section setoid.
Context `{Equiv A} `{!Equivalence (() : relation A)}.
Context `{Equiv A}.
Implicit Types l k : list A.
Lemma equiv_Forall2 l k : l k Forall2 () l k.
......@@ -2752,6 +2753,8 @@ Section setoid.
by setoid_rewrite equiv_option_Forall2.
Qed.
Context {Hequiv: Equivalence (() : relation A)}.
Global Instance list_equivalence : Equivalence (() : relation (list A)).
Proof.
split.
......@@ -2763,42 +2766,42 @@ Section setoid.
Proof. induction 1; f_equal; fold_leibniz; auto. Qed.
Global Instance cons_proper : Proper (() ==> () ==> ()) (@cons A).
Proof. by constructor. Qed.
Proof using -(Hequiv). by constructor. Qed.
Global Instance app_proper : Proper (() ==> () ==> ()) (@app A).
Proof. induction 1; intros ???; simpl; try constructor; auto. Qed.
Proof using -(Hequiv). induction 1; intros ???; simpl; try constructor; auto. Qed.
Global Instance length_proper : Proper (() ==> (=)) (@length A).
Proof. induction 1; f_equal/=; auto. Qed.
Proof using -(Hequiv). induction 1; f_equal/=; auto. Qed.
Global Instance tail_proper : Proper (() ==> ()) (@tail A).
Proof. by destruct 1. Qed.
Global Instance take_proper n : Proper (() ==> ()) (@take A n).
Proof. induction n; destruct 1; constructor; auto. Qed.
Proof using -(Hequiv). induction n; destruct 1; constructor; auto. Qed.
Global Instance drop_proper n : Proper (() ==> ()) (@drop A n).
Proof. induction n; destruct 1; simpl; try constructor; auto. Qed.
Proof using -(Hequiv). induction n; destruct 1; simpl; try constructor; auto. Qed.
Global Instance list_lookup_proper i :
Proper (() ==> ()) (lookup (M:=list A) i).
Proof. induction i; destruct 1; simpl; f_equiv; auto. Qed.
Global Instance list_alter_proper f i :
Proper (() ==> ()) f Proper (() ==> ()) (alter (M:=list A) f i).
Proof. intros. induction i; destruct 1; constructor; eauto. Qed.
Proof using -(Hequiv). intros. induction i; destruct 1; constructor; eauto. Qed.
Global Instance list_insert_proper i :
Proper (() ==> () ==> ()) (insert (M:=list A) i).
Proof. intros ???; induction i; destruct 1; constructor; eauto. Qed.
Proof using -(Hequiv). intros ???; induction i; destruct 1; constructor; eauto. Qed.
Global Instance list_inserts_proper i :
Proper (() ==> () ==> ()) (@list_inserts A i).
Proof.
Proof using -(Hequiv).
intros k1 k2 Hk; revert i.
induction Hk; intros ????; simpl; try f_equiv; naive_solver.
Qed.
Global Instance list_delete_proper i :
Proper (() ==> ()) (delete (M:=list A) i).
Proof. induction i; destruct 1; try constructor; eauto. Qed.
Proof using -(Hequiv). induction i; destruct 1; try constructor; eauto. Qed.
Global Instance option_list_proper : Proper (() ==> ()) (@option_list A).
Proof. destruct 1; by constructor. Qed.
Global Instance list_filter_proper P `{ x, Decision (P x)} :
Proper (() ==> iff) P Proper (() ==> ()) (filter (B:=list A) P).
Proof. intros ???. rewrite !equiv_Forall2. by apply Forall2_filter. Qed.
Proof using -(Hequiv). intros ???. rewrite !equiv_Forall2. by apply Forall2_filter. Qed.
Global Instance replicate_proper n : Proper (() ==> ()) (@replicate A n).
Proof. induction n; constructor; auto. Qed.
Proof using -(Hequiv). induction n; constructor; auto. Qed.
Global Instance reverse_proper : Proper (() ==> ()) (@reverse A).
Proof. induction 1; rewrite ?reverse_cons; repeat (done || f_equiv). Qed.
Global Instance last_proper : Proper (() ==> ()) (@last A).
......
......@@ -115,18 +115,18 @@ End Forall2.
Instance option_equiv `{Equiv A} : Equiv (option A) := option_Forall2 ().
Section setoids.
Context `{Equiv A} `{!Equivalence (() : relation A)}.
Context `{Equiv A} {Hequiv: Equivalence (() : relation A)}.
Implicit Types mx my : option A.
Lemma equiv_option_Forall2 mx my : mx my option_Forall2 () mx my.
Proof. done. Qed.
Proof using -(Hequiv). done. Qed.
Global Instance option_equivalence : Equivalence (() : relation (option A)).
Proof. apply _. Qed.
Global Instance Some_proper : Proper (() ==> ()) (@Some A).
Proof. by constructor. Qed.
Proof using -(Hequiv). by constructor. Qed.
Global Instance Some_equiv_inj : Inj () () (@Some A).
Proof. by inversion_clear 1. Qed.
Proof using -(Hequiv). by inversion_clear 1. Qed.
Global Instance option_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (option A).
Proof. intros x y; destruct 1; fold_leibniz; congruence. Qed.
......@@ -134,17 +134,17 @@ Section setoids.
Proof. split; [by inversion_clear 1|by intros ->]. Qed.
Lemma equiv_Some_inv_l mx my x :
mx my mx = Some x y, my = Some y x y.
Proof. destruct 1; naive_solver. Qed.
Proof using -(Hequiv). destruct 1; naive_solver. Qed.
Lemma equiv_Some_inv_r mx my y :
mx my my = Some y x, mx = Some x x y.
Proof. destruct 1; naive_solver. Qed.
Proof using -(Hequiv). destruct 1; naive_solver. Qed.
Lemma equiv_Some_inv_l' my x : Some x my x', Some x' = my x x'.
Proof. intros ?%(equiv_Some_inv_l _ _ x); naive_solver. Qed.
Proof using -(Hequiv). intros ?%(equiv_Some_inv_l _ _ x); naive_solver. Qed.
Lemma equiv_Some_inv_r' mx y : mx Some y y', mx = Some y' y y'.
Proof. intros ?%(equiv_Some_inv_r _ _ y); naive_solver. Qed.
Global Instance is_Some_proper : Proper (() ==> iff) (@is_Some A).
Proof. inversion_clear 1; split; eauto. Qed.
Proof using -(Hequiv). inversion_clear 1; split; eauto. Qed.
Global Instance from_option_proper {B} (R : relation B) (f : A B) :
Proper (() ==> R) f Proper (R ==> () ==> R) (from_option f).
Proof. destruct 3; simpl; auto. Qed.
......
  • I am not sure we should add Proof using directions to internal helping lemmas that should never be referred to, e.g. to lemmas in fixpoint2 and cofe_solver.

  • It doesn't hurt, and it keeps the proofs a little smaller. This doesn't mean we should do this everywhere, but I felt like doing it here.

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