Commit 070a85d9 authored by Robbert Krebbers's avatar Robbert Krebbers

Tweak some proof using tweaks for setoid stuff.

parent 6bbc6b49
Pipeline #3587 passed with stage
in 10 minutes and 40 seconds
......@@ -124,8 +124,8 @@ Section setoid.
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).
......
......@@ -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 *)
......
......@@ -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