Commit 22fac635 authored by Ralf Jung's avatar Ralf Jung

rename _setoid suffix to _equiv; add variant of fmap_Some_setoid that can be usefully destructed

parent 2407263c
...@@ -275,7 +275,7 @@ Lemma auth_map_ext {A B : ofeT} (f g : A → B) x : ...@@ -275,7 +275,7 @@ Lemma auth_map_ext {A B : ofeT} (f g : A → B) x :
( x, f x g x) auth_map f x auth_map g x. ( x, f x g x) auth_map f x auth_map g x.
Proof. Proof.
constructor; simpl; auto. constructor; simpl; auto.
apply option_fmap_setoid_ext=> a; by apply excl_map_ext. apply option_fmap_equiv_ext=> a; by apply excl_map_ext.
Qed. Qed.
Instance auth_map_ne {A B : ofeT} n : Instance auth_map_ne {A B : ofeT} n :
Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@auth_map A B). Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@auth_map A B).
......
...@@ -1250,11 +1250,11 @@ Next Obligation. ...@@ -1250,11 +1250,11 @@ Next Obligation.
Qed. Qed.
Next Obligation. Next Obligation.
intros F A B x. rewrite /= -{2}(option_fmap_id x). intros F A B x. rewrite /= -{2}(option_fmap_id x).
apply option_fmap_setoid_ext=>y; apply rFunctor_id. apply option_fmap_equiv_ext=>y; apply rFunctor_id.
Qed. Qed.
Next Obligation. Next Obligation.
intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose. intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose.
apply option_fmap_setoid_ext=>y; apply rFunctor_compose. apply option_fmap_equiv_ext=>y; apply rFunctor_compose.
Qed. Qed.
Instance optionURF_contractive F : Instance optionURF_contractive F :
......
...@@ -475,11 +475,11 @@ Next Obligation. ...@@ -475,11 +475,11 @@ Next Obligation.
Qed. Qed.
Next Obligation. Next Obligation.
intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x). intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x).
apply map_fmap_setoid_ext=>y ??; apply cFunctor_id. apply map_fmap_equiv_ext=>y ??; apply cFunctor_id.
Qed. Qed.
Next Obligation. Next Obligation.
intros K ?? F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -map_fmap_compose. intros K ?? F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -map_fmap_compose.
apply map_fmap_setoid_ext=>y ??; apply cFunctor_compose. apply map_fmap_equiv_ext=>y ??; apply cFunctor_compose.
Qed. Qed.
Instance gmapCF_contractive K `{Countable K} F : Instance gmapCF_contractive K `{Countable K} F :
cFunctorContractive F cFunctorContractive (gmapCF K F). cFunctorContractive F cFunctorContractive (gmapCF K F).
...@@ -496,11 +496,11 @@ Next Obligation. ...@@ -496,11 +496,11 @@ Next Obligation.
Qed. Qed.
Next Obligation. Next Obligation.
intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x). intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x).
apply map_fmap_setoid_ext=>y ??; apply rFunctor_id. apply map_fmap_equiv_ext=>y ??; apply rFunctor_id.
Qed. Qed.
Next Obligation. Next Obligation.
intros K ?? F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -map_fmap_compose. intros K ?? F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -map_fmap_compose.
apply map_fmap_setoid_ext=>y ??; apply rFunctor_compose. apply map_fmap_equiv_ext=>y ??; apply rFunctor_compose.
Qed. Qed.
Instance gmapRF_contractive K `{Countable K} F : Instance gmapRF_contractive K `{Countable K} F :
rFunctorContractive F urFunctorContractive (gmapURF K F). rFunctorContractive F urFunctorContractive (gmapURF K F).
......
...@@ -108,11 +108,11 @@ Next Obligation. ...@@ -108,11 +108,11 @@ Next Obligation.
Qed. Qed.
Next Obligation. Next Obligation.
intros F A B x. rewrite /= -{2}(list_fmap_id x). intros F A B x. rewrite /= -{2}(list_fmap_id x).
apply list_fmap_setoid_ext=>y. apply cFunctor_id. apply list_fmap_equiv_ext=>y. apply cFunctor_id.
Qed. Qed.
Next Obligation. Next Obligation.
intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -list_fmap_compose. intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -list_fmap_compose.
apply list_fmap_setoid_ext=>y; apply cFunctor_compose. apply list_fmap_equiv_ext=>y; apply cFunctor_compose.
Qed. Qed.
Instance listCF_contractive F : Instance listCF_contractive F :
...@@ -452,11 +452,11 @@ Next Obligation. ...@@ -452,11 +452,11 @@ Next Obligation.
Qed. Qed.
Next Obligation. Next Obligation.
intros F A B x. rewrite /= -{2}(list_fmap_id x). intros F A B x. rewrite /= -{2}(list_fmap_id x).
apply list_fmap_setoid_ext=>y. apply urFunctor_id. apply list_fmap_equiv_ext=>y. apply urFunctor_id.
Qed. Qed.
Next Obligation. Next Obligation.
intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -list_fmap_compose. intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -list_fmap_compose.
apply list_fmap_setoid_ext=>y; apply urFunctor_compose. apply list_fmap_equiv_ext=>y; apply urFunctor_compose.
Qed. Qed.
Instance listURF_contractive F : Instance listURF_contractive F :
......
...@@ -820,11 +820,11 @@ Next Obligation. ...@@ -820,11 +820,11 @@ Next Obligation.
Qed. Qed.
Next Obligation. Next Obligation.
intros F A B x. rewrite /= -{2}(option_fmap_id x). intros F A B x. rewrite /= -{2}(option_fmap_id x).
apply option_fmap_setoid_ext=>y; apply cFunctor_id. apply option_fmap_equiv_ext=>y; apply cFunctor_id.
Qed. Qed.
Next Obligation. Next Obligation.
intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose. intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose.
apply option_fmap_setoid_ext=>y; apply cFunctor_compose. apply option_fmap_equiv_ext=>y; apply cFunctor_compose.
Qed. Qed.
Instance optionCF_contractive F : Instance optionCF_contractive F :
......
...@@ -556,7 +556,7 @@ Proof. apply map_eq; intros i; by rewrite lookup_fmap, option_fmap_id. Qed. ...@@ -556,7 +556,7 @@ Proof. apply map_eq; intros i; by rewrite lookup_fmap, option_fmap_id. Qed.
Lemma map_fmap_compose {A B C} (f : A B) (g : B C) (m : M A) : Lemma map_fmap_compose {A B C} (f : A B) (g : B C) (m : M A) :
g f <$> m = g <$> f <$> m. g f <$> m = g <$> f <$> m.
Proof. apply map_eq; intros i; by rewrite !lookup_fmap,option_fmap_compose. Qed. Proof. apply map_eq; intros i; by rewrite !lookup_fmap,option_fmap_compose. Qed.
Lemma map_fmap_setoid_ext `{Equiv A, Equiv B} (f1 f2 : A B) m : Lemma map_fmap_equiv_ext `{Equiv A, Equiv B} (f1 f2 : A B) m :
( i x, m !! i = Some x f1 x f2 x) f1 <$> m f2 <$> m. ( i x, m !! i = Some x f1 x f2 x) f1 <$> m f2 <$> m.
Proof. Proof.
intros Hi i; rewrite !lookup_fmap. intros Hi i; rewrite !lookup_fmap.
......
...@@ -2802,7 +2802,7 @@ Section fmap. ...@@ -2802,7 +2802,7 @@ Section fmap.
Lemma list_fmap_ext (g : A B) (l1 l2 : list A) : Lemma list_fmap_ext (g : A B) (l1 l2 : list A) :
( x, f x = g x) l1 = l2 fmap f l1 = fmap g l2. ( x, f x = g x) l1 = l2 fmap f l1 = fmap g l2.
Proof. intros ? <-. induction l1; f_equal/=; auto. Qed. Proof. intros ? <-. induction l1; f_equal/=; auto. Qed.
Lemma list_fmap_setoid_ext `{Equiv B} (g : A B) l : Lemma list_fmap_equiv_ext `{Equiv B} (g : A B) l :
( x, f x g x) f <$> l g <$> l. ( x, f x g x) f <$> l g <$> l.
Proof. induction l; constructor; auto. Qed. Proof. induction l; constructor; auto. Qed.
......
...@@ -180,7 +180,7 @@ Proof. unfold is_Some; destruct mx; naive_solver. Qed. ...@@ -180,7 +180,7 @@ Proof. unfold is_Some; destruct mx; naive_solver. Qed.
Lemma fmap_Some {A B} (f : A B) mx y : Lemma fmap_Some {A B} (f : A B) mx y :
f <$> mx = Some y x, mx = Some x y = f x. f <$> mx = Some y x, mx = Some x y = f x.
Proof. destruct mx; naive_solver. Qed. Proof. destruct mx; naive_solver. Qed.
Lemma fmap_Some_setoid {A B} `{Equiv B} `{!Equivalence (() : relation B)} Lemma fmap_Some_equiv {A B} `{Equiv B} `{!Equivalence (() : relation B)}
(f : A B) mx y : (f : A B) mx y :
f <$> mx Some y x, mx = Some x y f x. f <$> mx Some y x, mx = Some x y f x.
Proof. Proof.
...@@ -190,6 +190,10 @@ Proof. ...@@ -190,6 +190,10 @@ Proof.
- intros ?%symmetry%equiv_None. done. - intros ?%symmetry%equiv_None. done.
- intros (? & ? & ?). done. - intros (? & ? & ?). done.
Qed. Qed.
Lemma fmap_Some_equiv' {A B} `{Equiv B} `{!Equivalence (() : relation B)}
(f : A B) mx y :
f <$> mx Some y x, mx = Some x y f x.
Proof. intros. apply fmap_Some_equiv. done. Qed.
Lemma fmap_None {A B} (f : A B) mx : f <$> mx = None mx = None. Lemma fmap_None {A B} (f : A B) mx : f <$> mx = None mx = None.
Proof. by destruct mx. Qed. Proof. by destruct mx. Qed.
Lemma option_fmap_id {A} (mx : option A) : id <$> mx = mx. Lemma option_fmap_id {A} (mx : option A) : id <$> mx = mx.
...@@ -200,7 +204,7 @@ Proof. by destruct mx. Qed. ...@@ -200,7 +204,7 @@ Proof. by destruct mx. Qed.
Lemma option_fmap_ext {A B} (f g : A B) mx : Lemma option_fmap_ext {A B} (f g : A B) mx :
( x, f x = g x) f <$> mx = g <$> mx. ( x, f x = g x) f <$> mx = g <$> mx.
Proof. intros; destruct mx; f_equal/=; auto. Qed. Proof. intros; destruct mx; f_equal/=; auto. Qed.
Lemma option_fmap_setoid_ext `{Equiv A, Equiv B} (f g : A B) mx : Lemma option_fmap_equiv_ext `{Equiv A, Equiv B} (f g : A B) mx :
( x, f x g x) f <$> mx g <$> mx. ( x, f x g x) f <$> mx g <$> mx.
Proof. destruct mx; constructor; auto. Qed. Proof. destruct mx; constructor; auto. Qed.
Lemma option_fmap_bind {A B C} (f : A B) (g : B option C) mx : Lemma option_fmap_bind {A B C} (f : A B) (g : B option C) mx :
......
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