Commit 47e0f1c4 authored by Ralf Jung's avatar Ralf Jung Committed by Robbert Krebbers

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

parent ee3e02f0
...@@ -32,7 +32,7 @@ Qed. ...@@ -32,7 +32,7 @@ Qed.
(** * Choice principles *) (** * Choice principles *)
Section choice. Section choice.
Context `{Countable A} (P : A Prop) `{ x, Decision (P x)}. Context `{Countable A} (P : A Prop).
Inductive choose_step: relation positive := Inductive choose_step: relation positive :=
| choose_step_None {p} : decode p = None choose_step (Psucc p) p | choose_step_None {p} : decode p = None choose_step (Psucc p) p
...@@ -50,6 +50,9 @@ Section choice. ...@@ -50,6 +50,9 @@ Section choice.
constructor. intros j. constructor. intros j.
inversion 1 as [? Hd|? y Hd]; subst; auto with lia. inversion 1 as [? Hd|? y Hd]; subst; auto with lia.
Qed. Qed.
Context `{ x, Decision (P x)}.
Fixpoint choose_go {i} (acc : Acc choose_step i) : A := Fixpoint choose_go {i} (acc : Acc choose_step i) : A :=
match Some_dec (decode i) with match Some_dec (decode i) with
| inleft (xHx) => | inleft (xHx) =>
......
...@@ -118,7 +118,13 @@ Context `{FinMap K M}. ...@@ -118,7 +118,13 @@ Context `{FinMap K M}.
(** ** Setoids *) (** ** Setoids *)
Section setoid. 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)). Global Instance map_equivalence : Equivalence (() : relation (M A)).
Proof. Proof.
split. split.
...@@ -173,9 +179,6 @@ Section setoid. ...@@ -173,9 +179,6 @@ Section setoid.
split; [intros Hm; apply map_eq; intros i|by intros ->]. split; [intros Hm; apply map_eq; intros i|by intros ->].
by rewrite lookup_empty, <-equiv_None, Hm, lookup_empty. by rewrite lookup_empty, <-equiv_None, Hm, lookup_empty.
Qed. 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) : Global Instance map_fmap_proper `{Equiv B} (f : A B) :
Proper (() ==> ()) f Proper (() ==> ()) (fmap (M:=M) f). Proper (() ==> ()) f Proper (() ==> ()) (fmap (M:=M) f).
Proof. Proof.
......
...@@ -171,13 +171,15 @@ Proof. apply finite_bijective. eauto. Qed. ...@@ -171,13 +171,15 @@ Proof. apply finite_bijective. eauto. Qed.
(** Decidability of quantification over finite types *) (** Decidability of quantification over finite types *)
Section forall_exists. 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). Lemma Forall_finite : Forall P (enum A) ( x, P x).
Proof. rewrite Forall_forall. intuition auto using elem_of_enum. Qed. Proof. rewrite Forall_forall. intuition auto using elem_of_enum. Qed.
Lemma Exists_finite : Exists P (enum A) ( x, P x). Lemma Exists_finite : Exists P (enum A) ( x, P x).
Proof. rewrite Exists_exists. naive_solver eauto using elem_of_enum. Qed. 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). Global Instance forall_dec: Decision ( x, P x).
Proof. Proof.
refine (cast_if (decide (Forall P (enum A)))); refine (cast_if (decide (Forall P (enum A))));
......
...@@ -735,6 +735,28 @@ End no_dup_dec. ...@@ -735,6 +735,28 @@ End no_dup_dec.
(** ** Set operations on lists *) (** ** Set operations on lists *)
Section list_set. 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}. Context `{!EqDecision A}.
Lemma elem_of_list_difference l k x : x ∈ list_difference l k ↔ x ∈ l ∧ x ∉ k. Lemma elem_of_list_difference l k x : x ∈ list_difference l k ↔ x ∈ l ∧ x ∉ k.
Proof. Proof.
...@@ -773,27 +795,6 @@ Section list_set. ...@@ -773,27 +795,6 @@ Section list_set.
- constructor. rewrite elem_of_list_intersection; intuition. done. - constructor. rewrite elem_of_list_intersection; intuition. done.
- done. - done.
Qed. 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. End list_set.
(** ** Properties of the [filter] function *) (** ** Properties of the [filter] function *)
...@@ -2171,7 +2172,7 @@ Section Forall_Exists. ...@@ -2171,7 +2172,7 @@ Section Forall_Exists.
Lemma Forall_replicate n x : P x → Forall P (replicate n x). Lemma Forall_replicate n x : P x → Forall P (replicate n x).
Proof. induction n; simpl; constructor; auto. Qed. Proof. induction n; simpl; constructor; auto. Qed.
Lemma Forall_replicate_eq n (x : A) : Forall (x =) (replicate n x). 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). Lemma Forall_take n l : Forall P l → Forall P (take n l).
Proof. intros Hl. revert n. induction Hl; intros [|?]; simpl; auto. Qed. Proof. intros Hl. revert n. induction Hl; intros [|?]; simpl; auto. Qed.
Lemma Forall_drop n l : Forall P l → Forall P (drop n l). Lemma Forall_drop n l : Forall P l → Forall P (drop n l).
...@@ -2741,7 +2742,7 @@ End Forall3. ...@@ -2741,7 +2742,7 @@ End Forall3.
(** Setoids *) (** Setoids *)
Section setoid. Section setoid.
Context `{Equiv A} `{!Equivalence ((≡) : relation A)}. Context `{Equiv A}.
Implicit Types l k : list A. Implicit Types l k : list A.
Lemma equiv_Forall2 l k : l ≡ k ↔ Forall2 (≡) l k. Lemma equiv_Forall2 l k : l ≡ k ↔ Forall2 (≡) l k.
...@@ -2752,6 +2753,8 @@ Section setoid. ...@@ -2752,6 +2753,8 @@ Section setoid.
by setoid_rewrite equiv_option_Forall2. by setoid_rewrite equiv_option_Forall2.
Qed. Qed.
Context {Hequiv: Equivalence ((≡) : relation A)}.
Global Instance list_equivalence : Equivalence ((≡) : relation (list A)). Global Instance list_equivalence : Equivalence ((≡) : relation (list A)).
Proof. Proof.
split. split.
...@@ -2763,42 +2766,42 @@ Section setoid. ...@@ -2763,42 +2766,42 @@ Section setoid.
Proof. induction 1; f_equal; fold_leibniz; auto. Qed. Proof. induction 1; f_equal; fold_leibniz; auto. Qed.
Global Instance cons_proper : Proper ((≡) ==> (≡) ==> (≡)) (@cons A). Global Instance cons_proper : Proper ((≡) ==> (≡) ==> (≡)) (@cons A).
Proof. by constructor. Qed. Proof using -(Hequiv). by constructor. Qed.
Global Instance app_proper : Proper ((≡) ==> (≡) ==> (≡)) (@app A). 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). 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). Global Instance tail_proper : Proper ((≡) ==> (≡)) (@tail A).
Proof. by destruct 1. Qed. Proof. by destruct 1. Qed.
Global Instance take_proper n : Proper ((≡) ==> (≡)) (@take A n). 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). 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 : Global Instance list_lookup_proper i :
Proper ((≡) ==> (≡)) (lookup (M:=list A) i). Proper ((≡) ==> (≡)) (lookup (M:=list A) i).
Proof. induction i; destruct 1; simpl; f_equiv; auto. Qed. Proof. induction i; destruct 1; simpl; f_equiv; auto. Qed.
Global Instance list_alter_proper f i : Global Instance list_alter_proper f i :
Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (alter (M:=list A) 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 : Global Instance list_insert_proper i :
Proper ((≡) ==> (≡) ==> (≡)) (insert (M:=list A) 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 : Global Instance list_inserts_proper i :
Proper ((≡) ==> (≡) ==> (≡)) (@list_inserts A i). Proper ((≡) ==> (≡) ==> (≡)) (@list_inserts A i).
Proof. Proof using -(Hequiv).
intros k1 k2 Hk; revert i. intros k1 k2 Hk; revert i.
induction Hk; intros ????; simpl; try f_equiv; naive_solver. induction Hk; intros ????; simpl; try f_equiv; naive_solver.
Qed. Qed.
Global Instance list_delete_proper i : Global Instance list_delete_proper i :
Proper ((≡) ==> (≡)) (delete (M:=list A) 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). Global Instance option_list_proper : Proper ((≡) ==> (≡)) (@option_list A).
Proof. destruct 1; by constructor. Qed. Proof. destruct 1; by constructor. Qed.
Global Instance list_filter_proper P `{∀ x, Decision (P x)} : Global Instance list_filter_proper P `{∀ x, Decision (P x)} :
Proper ((≡) ==> iff) P → Proper ((≡) ==> (≡)) (filter (B:=list A) P). 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). 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). Global Instance reverse_proper : Proper ((≡) ==> (≡)) (@reverse A).
Proof. induction 1; rewrite ?reverse_cons; repeat (done || f_equiv). Qed. Proof. induction 1; rewrite ?reverse_cons; repeat (done || f_equiv). Qed.
Global Instance last_proper : Proper ((≡) ==> (≡)) (@last A). Global Instance last_proper : Proper ((≡) ==> (≡)) (@last A).
......
...@@ -115,18 +115,18 @@ End Forall2. ...@@ -115,18 +115,18 @@ End Forall2.
Instance option_equiv `{Equiv A} : Equiv (option A) := option_Forall2 (). Instance option_equiv `{Equiv A} : Equiv (option A) := option_Forall2 ().
Section setoids. Section setoids.
Context `{Equiv A} `{!Equivalence (() : relation A)}. Context `{Equiv A} {Hequiv: Equivalence (() : relation A)}.
Implicit Types mx my : option A. Implicit Types mx my : option A.
Lemma equiv_option_Forall2 mx my : mx my option_Forall2 () mx my. 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)). Global Instance option_equivalence : Equivalence (() : relation (option A)).
Proof. apply _. Qed. Proof. apply _. Qed.
Global Instance Some_proper : Proper (() ==> ()) (@Some A). 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). 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). Global Instance option_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (option A).
Proof. intros x y; destruct 1; fold_leibniz; congruence. Qed. Proof. intros x y; destruct 1; fold_leibniz; congruence. Qed.
...@@ -134,17 +134,17 @@ Section setoids. ...@@ -134,17 +134,17 @@ Section setoids.
Proof. split; [by inversion_clear 1|by intros ->]. Qed. Proof. split; [by inversion_clear 1|by intros ->]. Qed.
Lemma equiv_Some_inv_l mx my x : Lemma equiv_Some_inv_l mx my x :
mx my mx = Some x y, my = Some y x y. 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 : Lemma equiv_Some_inv_r mx my y :
mx my my = Some y x, mx = Some x x 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'. 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'. 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. Proof. intros ?%(equiv_Some_inv_r _ _ y); naive_solver. Qed.
Global Instance is_Some_proper : Proper (() ==> iff) (@is_Some A). 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) : Global Instance from_option_proper {B} (R : relation B) (f : A B) :
Proper (() ==> R) f Proper (R ==> () ==> R) (from_option f). Proper (() ==> R) f Proper (R ==> () ==> R) (from_option f).
Proof. destruct 3; simpl; auto. Qed. Proof. destruct 3; simpl; auto. Qed.
......
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