Commit aeb449a7 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'robbert/hintmode' into 'master'

More missing `Hint Mode`s.

See merge request iris/stdpp!271
parents f65bf936 c75cd874
......@@ -40,6 +40,8 @@ API-breaking change is listed.
+ Add lemma `Permutation_cross_split`.
+ Make lemma `elem_of_Permutation` a biimplication
- Add function `kmap` to transform the keys of finite maps.
- Set `Hint Mode` for the classes `PartialOrder`, `TotalOrder`, `MRet`, `MBind`,
`MJoin`, `FMap`, `OMap`, `MGuard`, `SemiSet`, `Set_`, `TopSet`, and `Infinite`.
The following `sed` script should perform most of the renaming
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
......
......@@ -460,14 +460,18 @@ Proof. auto. Qed.
relation [R] instead of [⊆] to support multiple orders on the same type. *)
Definition strict {A} (R : relation A) : relation A := λ X Y, R X Y ¬R Y X.
Global Instance: Params (@strict) 2 := {}.
Class PartialOrder {A} (R : relation A) : Prop := {
partial_order_pre :> PreOrder R;
partial_order_anti_symm :> AntiSymm (=) R
}.
Global Hint Mode PartialOrder ! ! : typeclass_instances.
Class TotalOrder {A} (R : relation A) : Prop := {
total_order_partial :> PartialOrder R;
total_order_trichotomy :> Trichotomy (strict R)
}.
Global Hint Mode TotalOrder ! ! : typeclass_instances.
(** * Logic *)
Global Instance prop_inhabited : Inhabited Prop := populate True.
......@@ -1007,18 +1011,27 @@ class with the monad laws). *)
Class MRet (M : Type Type) := mret: {A}, A M A.
Global Arguments mret {_ _ _} _ : assert.
Global Instance: Params (@mret) 3 := {}.
Global Hint Mode MRet ! : typeclass_instances.
Class MBind (M : Type Type) := mbind : {A B}, (A M B) M A M B.
Global Arguments mbind {_ _ _ _} _ !_ / : assert.
Global Instance: Params (@mbind) 4 := {}.
Global Hint Mode MBind ! : typeclass_instances.
Class MJoin (M : Type Type) := mjoin: {A}, M (M A) M A.
Global Arguments mjoin {_ _ _} !_ / : assert.
Global Instance: Params (@mjoin) 3 := {}.
Global Hint Mode MJoin ! : typeclass_instances.
Class FMap (M : Type Type) := fmap : {A B}, (A B) M A M B.
Global Arguments fmap {_ _ _ _} _ !_ / : assert.
Global Instance: Params (@fmap) 4 := {}.
Global Hint Mode FMap ! : typeclass_instances.
Class OMap (M : Type Type) := omap: {A B}, (A option B) M A M B.
Global Arguments omap {_ _ _ _} _ !_ / : assert.
Global Instance: Params (@omap) 4 := {}.
Global Hint Mode OMap ! : typeclass_instances.
Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : stdpp_scope.
Notation "( m ≫=.)" := (λ f, mbind f m) (only parsing) : stdpp_scope.
......@@ -1044,6 +1057,7 @@ Notation "ps .*2" := (fmap (M:=list) snd ps)
Class MGuard (M : Type Type) :=
mguard: P {dec : Decision P} {A}, (P M A) M A.
Global Arguments mguard _ _ _ !_ _ _ / : assert.
Global Hint Mode MGuard ! : typeclass_instances.
Notation "'guard' P ; z" := (mguard P (λ _, z))
(at level 20, z at level 200, only parsing, right associativity) : stdpp_scope.
Notation "'guard' P 'as' H ; z" := (mguard P (λ H, z))
......@@ -1283,18 +1297,23 @@ Class SemiSet A C `{ElemOf A C,
elem_of_singleton (x y : A) : x @{C} {[ y ]} x = y;
elem_of_union (X Y : C) (x : A) : x X Y x X x Y
}.
Global Hint Mode SemiSet - ! - - - - : typeclass_instances.
Class Set_ A C `{ElemOf A C, Empty C, Singleton A C,
Union C, Intersection C, Difference C} : Prop := {
set_semi_set :> SemiSet A C;
elem_of_intersection (X Y : C) (x : A) : x X Y x X x Y;
elem_of_difference (X Y : C) (x : A) : x X Y x X x Y
}.
Global Hint Mode Set_ - ! - - - - - - : typeclass_instances.
Class TopSet A C `{ElemOf A C, Empty C, Top C, Singleton A C,
Union C, Intersection C, Difference C} : Prop := {
top_set_set :> Set_ A C;
elem_of_top' (x : A) : x @{C} ⊤; (* We prove [elem_of_top : x ∈@{C} ⊤ ↔ True]
in [sets.v], which is more convenient for rewriting. *)
}.
Global Hint Mode TopSet - ! - - - - - - - : typeclass_instances.
(** We axiomative a finite set as a set whose elements can be
enumerated as a list. These elements, given by the [elements] function, may be
......@@ -1386,6 +1405,7 @@ Class Infinite A := {
infinite_is_fresh (xs : list A) : fresh xs xs;
infinite_fresh_Permutation :> Proper (@Permutation A ==> (=)) fresh;
}.
Global Hint Mode Infinite ! : typeclass_instances.
Global Arguments infinite_fresh : simpl never.
(** * Miscellaneous *)
......
......@@ -138,7 +138,7 @@ End infinite.
Definition coGpick `{Countable A, Infinite A} (X : coGset A) : A :=
fresh (match X with FinGSet _ => | CoFinGset X => X end).
Lemma coGpick_elem_of `{Countable A, Infinite A} X :
Lemma coGpick_elem_of `{Countable A, Infinite A} (X : coGset A) :
¬set_finite X coGpick X X.
Proof.
unfold coGpick.
......
......@@ -316,7 +316,7 @@ Proof.
destruct (decide (Exists (λ ix, m1 !! ix.1 = None) (map_to_list m2)))
as [[[i x] [?%elem_of_map_to_list ?]]%Exists_exists
|Hm%(not_Exists_Forall _)]; [eauto|].
destruct Heq; apply (anti_symm _), map_subseteq_spec; [done|intros i x Hi].
destruct Heq; apply (anti_symm ()), map_subseteq_spec; [done|intros i x Hi].
assert (is_Some (m1 !! i)) as [x' ?].
{ by apply not_eq_None_Some,
(proj1 (Forall_forall _ _) Hm (i,x)), elem_of_map_to_list. }
......@@ -689,24 +689,25 @@ Lemma lookup_omap_id_Some {A} (m : M (option A)) i x :
omap id m !! i = Some x m !! i = Some (Some x).
Proof. rewrite lookup_omap_Some. naive_solver. Qed.
Lemma fmap_empty {A B} (f : A B) : f <$> = .
Lemma fmap_empty {A B} (f : A B) : f <$> =@{M B} .
Proof. apply map_empty; intros i. by rewrite lookup_fmap, lookup_empty. Qed.
Lemma omap_empty {A B} (f : A option B) : omap f = .
Lemma omap_empty {A B} (f : A option B) : omap f =@{M B} .
Proof. apply map_empty; intros i. by rewrite lookup_omap, lookup_empty. Qed.
Lemma fmap_empty_inv {A B} (f : A B) m : f <$> m = m = .
Lemma fmap_empty_inv {A B} (f : A B) m : f <$> m =@{M B} m = .
Proof.
intros Hm. apply map_eq; intros i. generalize (f_equal (lookup i) Hm).
by rewrite lookup_fmap, !lookup_empty, fmap_None.
Qed.
Lemma fmap_insert {A B} (f: A B) m i x: f <$> <[i:=x]>m = <[i:=f x]>(f <$> m).
Lemma fmap_insert {A B} (f: A B) (m : M A) i x :
f <$> <[i:=x]>m = <[i:=f x]>(f <$> m).
Proof.
apply map_eq; intros i'; destruct (decide (i' = i)) as [->|].
- by rewrite lookup_fmap, !lookup_insert.
- by rewrite lookup_fmap, !lookup_insert_ne, lookup_fmap by done.
Qed.
Lemma omap_insert {A B} (f : A option B) m i x :
Lemma omap_insert {A B} (f : A option B) (m : M A) i x :
omap f (<[i:=x]>m) =
(match f x with Some y => <[i:=y]> | None => delete i end) (omap f m).
Proof.
......@@ -719,20 +720,21 @@ Proof.
+ by rewrite lookup_insert_ne, lookup_omap by done.
+ by rewrite lookup_delete_ne, lookup_omap by done.
Qed.
Lemma omap_insert_Some {A B} (f : A option B) m i x y :
Lemma omap_insert_Some {A B} (f : A option B) (m : M A) i x y :
f x = Some y omap f (<[i:=x]>m) = <[i:=y]>(omap f m).
Proof. intros Hx. by rewrite omap_insert, Hx. Qed.
Lemma omap_insert_None {A B} (f : A option B) m i x :
Lemma omap_insert_None {A B} (f : A option B) (m : M A) i x :
f x = None omap f (<[i:=x]>m) = delete i (omap f m).
Proof. intros Hx. by rewrite omap_insert, Hx. Qed.
Lemma fmap_delete {A B} (f: A B) m i: f <$> delete i m = delete i (f <$> m).
Lemma fmap_delete {A B} (f: A B) (m : M A) i :
f <$> delete i m = delete i (f <$> m).
Proof.
apply map_eq; intros i'; destruct (decide (i' = i)) as [->|].
- by rewrite lookup_fmap, !lookup_delete.
- by rewrite lookup_fmap, !lookup_delete_ne, lookup_fmap by done.
Qed.
Lemma omap_delete {A B} (f: A option B) m i :
Lemma omap_delete {A B} (f: A option B) (m : M A) i :
omap f (delete i m) = delete i (omap f m).
Proof.
apply map_eq; intros i'; destruct (decide (i' = i)) as [->|].
......@@ -740,22 +742,23 @@ Proof.
- by rewrite lookup_omap, !lookup_delete_ne, lookup_omap by done.
Qed.
Lemma map_fmap_singleton {A B} (f : A B) i x : f <$> {[i := x]} = {[i := f x]}.
Lemma map_fmap_singleton {A B} (f : A B) i x :
f <$> {[i := x]} =@{M B} {[i := f x]}.
Proof.
by unfold singletonM, map_singleton; rewrite fmap_insert, fmap_empty.
Qed.
Lemma omap_singleton {A B} (f : A option B) i x :
omap f {[ i := x ]} = match f x with Some y => {[ i:=y ]} | None => end.
omap f {[ i := x ]} =@{M B} match f x with Some y => {[ i:=y ]} | None => end.
Proof.
rewrite <-insert_empty, omap_insert, omap_empty. destruct (f x) as [y|]; simpl.
- by rewrite insert_empty.
- by rewrite delete_empty.
Qed.
Lemma omap_singleton_Some {A B} (f : A option B) i x y :
f x = Some y omap f {[ i := x ]} = {[ i := y ]}.
f x = Some y omap f {[ i := x ]} =@{M B} {[ i := y ]}.
Proof. intros Hx. by rewrite omap_singleton, Hx. Qed.
Lemma omap_singleton_None {A B} (f : A option B) i x :
f x = None omap f {[ i := x ]} = .
f x = None omap f {[ i := x ]} =@{M B} .
Proof. intros Hx. by rewrite omap_singleton, Hx. Qed.
Lemma map_fmap_id {A} (m : M A) : id <$> m = m.
......@@ -1608,14 +1611,14 @@ Section more_merge.
<[i:=x]>(merge f m1 m2) = merge f m1 (<[i:=z]>m2).
Proof. by intros; apply partial_alter_merge_r. Qed.
Lemma fmap_merge {D} (g : C D) m1 m2 :
Lemma fmap_merge {D} (g : C D) (m1 : M A) (m2 : M B) :
g <$> merge f m1 m2 = merge (λ mx1 mx2, g <$> f mx1 mx2) m1 m2.
Proof.
assert (DiagNone (λ mx1 mx2, g <$> f mx1 mx2)).
{ unfold DiagNone. by rewrite diag_none. }
apply map_eq; intros i. by rewrite lookup_fmap, !lookup_merge by done.
Qed.
Lemma omap_merge {D} (g : C option D) m1 m2 :
Lemma omap_merge {D} (g : C option D) (m1 : M A) (m2 : M B) :
omap g (merge f m1 m2) = merge (λ mx1 mx2, f mx1 mx2 = g) m1 m2.
Proof.
assert (DiagNone (λ mx1 mx2, f mx1 mx2 = g)).
......@@ -1682,7 +1685,8 @@ Proof.
rewrite <- (map_fmap_id m1) at 1. by rewrite map_zip_with_fmap.
Qed.
Lemma map_fmap_zip_with {A B C D} (f : A B C) (g : C D) m1 m2 :
Lemma map_fmap_zip_with {A B C D} (f : A B C) (g : C D)
(m1 : M A) (m2 : M B) :
g <$> map_zip_with f m1 m2 = map_zip_with (λ x y, g (f x y)) m1 m2.
Proof.
apply map_eq; intro i. rewrite lookup_fmap, !map_lookup_zip_with.
......@@ -2533,7 +2537,7 @@ Section map_seq.
Qed.
Lemma fmap_map_seq {B} (f : A B) start xs :
f <$> map_seq start xs = map_seq start (f <$> xs).
f <$> map_seq start xs =@{M B} map_seq start (f <$> xs).
Proof.
revert start. induction xs as [|x xs IH]; intros start; csimpl.
{ by rewrite fmap_empty. }
......
......@@ -3558,7 +3558,7 @@ Section fmap.
Proper (() ==> ()) f Proper (() ==> ()) (fmap f).
Proof. induction 2; simpl; [constructor|solve_proper]. Qed.
Global Instance fmap_inj: Inj (=) (=) f Inj (=) (=) (fmap f).
Global Instance fmap_inj: Inj (=) (=) f Inj (=@{list A}) (=) (fmap f).
Proof.
intros ? l1. induction l1 as [|x l1 IH]; [by intros [|??]|].
intros [|??]; intros; f_equal/=; simplify_eq; auto.
......
......@@ -190,7 +190,7 @@ Global Instance natmap_to_list {A} : FinMapToList nat A (natmap A) := λ m,
let (l,_) := m in natmap_to_list_raw 0 l.
Definition natmap_map_raw {A B} (f : A B) : natmap_raw A natmap_raw B :=
fmap (fmap f).
fmap (fmap (M:=option) f).
Lemma natmap_map_wf {A B} (f : A B) l :
natmap_wf l natmap_wf (natmap_map_raw f l).
Proof.
......
......@@ -853,7 +853,7 @@ Global Instance Qp_mul_inj_r p : Inj (=) (=) (Qp_mul p).
Proof.
destruct p as [p ?]. intros [q1 ?] [q2 ?]. rewrite <-!Qp_to_Qc_inj_iff; simpl.
intros Hpq.
apply (anti_symm _); apply (Qcmult_le_mono_pos_l _ _ p); by rewrite ?Hpq.
apply (anti_symm Qcle); apply (Qcmult_le_mono_pos_l _ _ p); by rewrite ?Hpq.
Qed.
Global Instance Qp_mul_inj_l p : Inj (=) (=) (λ q, q * p).
Proof.
......
......@@ -205,10 +205,10 @@ Lemma fmap_None {A B} (f : A → B) mx : f <$> mx = None ↔ mx = None.
Proof. by destruct mx. Qed.
Lemma option_fmap_id {A} (mx : option A) : id <$> mx = mx.
Proof. by destruct mx. Qed.
Lemma option_fmap_compose {A B} (f : A B) {C} (g : B C) mx :
Lemma option_fmap_compose {A B} (f : A B) {C} (g : B C) (mx : option A) :
g f <$> mx = g <$> (f <$> mx).
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 : option A) :
( x, f x = g x) f <$> mx = g <$> mx.
Proof. intros; destruct mx; f_equal/=; auto. Qed.
Lemma option_fmap_equiv_ext {A} `{Equiv B} (f g : A B) (mx : option A) :
......
......@@ -13,7 +13,7 @@ Section orders.
Lemma reflexive_eq `{!Reflexive R} X Y : X = Y X Y.
Proof. by intros <-. Qed.
Lemma anti_symm_iff `{!PartialOrder R} X Y : X = Y R X Y R Y X.
Proof. split; [by intros ->|]. by intros [??]; apply (anti_symm _). Qed.
Proof. split; [by intros ->|]. by intros [??]; apply (anti_symm R). Qed.
Lemma strict_spec X Y : X Y X Y Y X.
Proof. done. Qed.
Lemma strict_include X Y : X Y X Y.
......
Supports Markdown
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