Skip to content

GitLab

Commit 24623c52 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files
Options

Tweak some proof using tweaks for setoid stuff.

parent 47e0f1c4
Hide whitespace changes
Inline Side-by-side
Showing with 49 additions and 42 deletions
theories/fin_maps.v
View file @ 24623c52
......@@ -119,13 +119,13 @@ Context `{FinMap K M}.
(** ** Setoids *)
Section setoid.
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 A) → Equivalence ((≡) : relation (M A)).
Proof.
split.
- by intros m i.
......@@ -147,7 +147,10 @@ Section setoid.
Proof. by intros ???; apply partial_alter_proper; [constructor|]. Qed.
Global Instance singleton_proper k :
Proper ((≡) ==> (≡)) (singletonM k : A → M A).
Proof. by intros ???; apply insert_proper. Qed.
Proof.
intros ???; apply insert_proper; [done|].
intros ?. rewrite lookup_empty; constructor.
Qed.
Global Instance delete_proper (i : K) :
Proper ((≡) ==> (≡)) (delete (M:=M A) i).
Proof. by apply partial_alter_proper; [constructor|]. Qed.
......@@ -170,14 +173,12 @@ Section setoid.
by do 2 destruct 1; first [apply Hf | constructor].
Qed.
Global Instance map_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (M A).
Proof.
intros m1 m2 Hm; apply map_eq; intros i.
by unfold_leibniz; apply lookup_proper.
Qed.
Proof. intros m1 m2 Hm; apply map_eq; intros i. apply leibniz_equiv, Hm. Qed.
Lemma map_equiv_empty (m : M A) : m ≡ ∅ ↔ m = ∅.
Proof.
split; [intros Hm; apply map_eq; intros i|by intros ->].
by rewrite lookup_empty, <-equiv_None, Hm, lookup_empty.
split; [intros Hm; apply map_eq; intros i|intros ->].
- generalize (Hm i). by rewrite lookup_empty, equiv_None.
- intros ?. rewrite lookup_empty; constructor.
Qed.
Global Instance map_fmap_proper `{Equiv B} (f : A → B) :
Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (fmap (M:=M) f).
......
theories/list.v
View file @ 24623c52
......@@ -2753,9 +2753,8 @@ Section setoid.
by setoid_rewrite equiv_option_Forall2.
Qed.
Context {Hequiv: Equivalence ((≡) : relation A)}.
Global Instance list_equivalence : Equivalence ((≡) : relation (list A)).
Global Instance list_equivalence :
Equivalence ((≡) : relation A) → Equivalence ((≡) : relation (list A)).
Proof.
split.
- intros l. by apply equiv_Forall2.
......@@ -2766,48 +2765,53 @@ Section setoid.
Proof. induction 1; f_equal; fold_leibniz; auto. Qed.
Global Instance cons_proper : Proper ((≡) ==> (≡) ==> (≡)) (@cons A).
Proof using -(Hequiv). by constructor. Qed.
Proof. by constructor. Qed.
Global Instance app_proper : Proper ((≡) ==> (≡) ==> (≡)) (@app A).
Proof using -(Hequiv). induction 1; intros ???; simpl; try constructor; auto. Qed.
Proof. induction 1; intros ???; simpl; try constructor; auto. Qed.
Global Instance length_proper : Proper ((≡) ==> (=)) (@length A).
Proof using -(Hequiv). induction 1; f_equal/=; auto. Qed.
Proof. induction 1; f_equal/=; auto. Qed.
Global Instance tail_proper : Proper ((≡) ==> (≡)) (@tail A).
Proof. by destruct 1. Qed.
Proof. destruct 1; try constructor; auto. Qed.
Global Instance take_proper n : Proper ((≡) ==> (≡)) (@take A n).
Proof using -(Hequiv). induction n; destruct 1; constructor; auto. Qed.
Proof. induction n; destruct 1; constructor; auto. Qed.
Global Instance drop_proper n : Proper ((≡) ==> (≡)) (@drop A n).
Proof using -(Hequiv). induction n; destruct 1; simpl; try constructor; auto. Qed.
Proof. 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.
Proof. induction i; destruct 1; simpl; try constructor; auto. Qed.
Global Instance list_alter_proper f i :
Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (alter (M:=list A) f i).
Proof using -(Hequiv). intros. induction i; destruct 1; constructor; eauto. Qed.
Proof. intros. induction i; destruct 1; constructor; eauto. Qed.
Global Instance list_insert_proper i :
Proper ((≡) ==> (≡) ==> (≡)) (insert (M:=list A) i).
Proof using -(Hequiv). intros ???; induction i; destruct 1; constructor; eauto. Qed.
Proof. intros ???; induction i; destruct 1; constructor; eauto. Qed.
Global Instance list_inserts_proper i :
Proper ((≡) ==> (≡) ==> (≡)) (@list_inserts A i).
Proof using -(Hequiv).
Proof.
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 using -(Hequiv). induction i; destruct 1; try constructor; eauto. Qed.
Proof. induction i; destruct 1; try constructor; eauto. Qed.
Global Instance option_list_proper : Proper ((≡) ==> (≡)) (@option_list A).
Proof. destruct 1; by constructor. Qed.
Proof. destruct 1; repeat constructor; auto. Qed.
Global Instance list_filter_proper P `{∀ x, Decision (P x)} :
Proper ((≡) ==> iff) P → Proper ((≡) ==> (≡)) (filter (B:=list A) P).
Proof using -(Hequiv). intros ???. rewrite !equiv_Forall2. by apply Forall2_filter. Qed.
Proof. intros ???. rewrite !equiv_Forall2. by apply Forall2_filter. Qed.
Global Instance replicate_proper n : Proper ((≡) ==> (≡)) (@replicate A n).
Proof using -(Hequiv). induction n; constructor; auto. Qed.
Proof. induction n; constructor; auto. Qed.
Global Instance reverse_proper : Proper ((≡) ==> (≡)) (@reverse A).
Proof. induction 1; rewrite ?reverse_cons; repeat (done || f_equiv). Qed.
Proof.
induction 1; rewrite ?reverse_cons; simpl; [constructor|].
apply app_proper; repeat constructor; auto.
Qed.
Global Instance last_proper : Proper ((≡) ==> (≡)) (@last A).
Proof. induction 1 as [|????? []]; simpl; repeat (done || f_equiv). Qed.
Proof. induction 1 as [|????? []]; simpl; repeat constructor; auto. Qed.
Global Instance resize_proper n : Proper ((≡) ==> (≡) ==> (≡)) (@resize A n).
Proof. induction n; destruct 2; simpl; repeat (auto || f_equiv). Qed.
Proof.
induction n; destruct 2; simpl; repeat (constructor || f_equiv); auto.
Qed.
End setoid.
(** * Properties of the monadic operations *)
......
theories/option.v
View file @ 24623c52
......@@ -115,36 +115,38 @@ End Forall2.
Instance option_equiv `{Equiv A} : Equiv (option A) := option_Forall2 (≡).
Section setoids.
Context `{Equiv A} {Hequiv: Equivalence ((≡) : relation A)}.
Context `{Equiv A}.
Implicit Types mx my : option A.
Lemma equiv_option_Forall2 mx my : mx ≡ my ↔ option_Forall2 (≡) mx my.
Proof using -(Hequiv). done. Qed.
Proof. done. Qed.
Global Instance option_equivalence : Equivalence ((≡) : relation (option A)).
Global Instance option_equivalence :
Equivalence ((≡) : relation A) → Equivalence ((≡) : relation (option A)).
Proof. apply _. Qed.
Global Instance Some_proper : Proper ((≡) ==> (≡)) (@Some A).
Proof using -(Hequiv). by constructor. Qed.
Proof. by constructor. Qed.
Global Instance Some_equiv_inj : Inj (≡) (≡) (@Some A).
Proof using -(Hequiv). by inversion_clear 1. Qed.
Proof. by inversion_clear 1. Qed.
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; f_equal; by apply leibniz_equiv. Qed.
Lemma equiv_None mx : mx ≡ None ↔ mx = None.
Proof. split; [by inversion_clear 1|by intros ->]. Qed.
Proof. split; [by inversion_clear 1|intros ->; constructor]. Qed.
Lemma equiv_Some_inv_l mx my x :
mx ≡ my → mx = Some x → ∃ y, my = Some y ∧ x ≡ y.
Proof using -(Hequiv). destruct 1; naive_solver. Qed.
Proof. 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 using -(Hequiv). destruct 1; naive_solver. Qed.
Proof. destruct 1; naive_solver. Qed.
Lemma equiv_Some_inv_l' my x : Some x ≡ my → ∃ x', Some x' = my ∧ x ≡ x'.
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_l _ _ x); naive_solver. Qed.
Lemma equiv_Some_inv_r' `{!Equivalence ((≡) : relation A)} 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 using -(Hequiv). inversion_clear 1; split; eauto. Qed.
Proof. 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.
......
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