Commit 44b18f4d authored by Robbert Krebbers's avatar Robbert Krebbers

Shorter names for common math notions.

Also do some minor clean up.
parent 7ebc1859
This diff is collapsed.
...@@ -15,13 +15,13 @@ Definition encode_nat `{Countable A} (x : A) : nat := ...@@ -15,13 +15,13 @@ Definition encode_nat `{Countable A} (x : A) : nat :=
pred (Pos.to_nat (encode x)). pred (Pos.to_nat (encode x)).
Definition decode_nat `{Countable A} (i : nat) : option A := Definition decode_nat `{Countable A} (i : nat) : option A :=
decode (Pos.of_nat (S i)). decode (Pos.of_nat (S i)).
Instance encode_injective `{Countable A} : Injective (=) (=) encode. Instance encode_inj `{Countable A} : Inj (=) (=) encode.
Proof. Proof.
intros x y Hxy; apply (injective Some). intros x y Hxy; apply (inj Some).
by rewrite <-(decode_encode x), Hxy, decode_encode. by rewrite <-(decode_encode x), Hxy, decode_encode.
Qed. Qed.
Instance encode_nat_injective `{Countable A} : Injective (=) (=) encode_nat. Instance encode_nat_inj `{Countable A} : Inj (=) (=) encode_nat.
Proof. unfold encode_nat; intros x y Hxy; apply (injective encode); lia. Qed. Proof. unfold encode_nat; intros x y Hxy; apply (inj encode); lia. Qed.
Lemma decode_encode_nat `{Countable A} x : decode_nat (encode_nat x) = Some x. Lemma decode_encode_nat `{Countable A} x : decode_nat (encode_nat x) = Some x.
Proof. Proof.
pose proof (Pos2Nat.is_pos (encode x)). pose proof (Pos2Nat.is_pos (encode x)).
...@@ -70,11 +70,11 @@ Section choice. ...@@ -70,11 +70,11 @@ Section choice.
Definition choice (HA : x, P x) : { x | P x } := _choose_correct HA. Definition choice (HA : x, P x) : { x | P x } := _choose_correct HA.
End choice. End choice.
Lemma surjective_cancel `{Countable A} `{ x y : B, Decision (x = y)} Lemma surj_cancel `{Countable A} `{ x y : B, Decision (x = y)}
(f : A B) `{!Surjective (=) f} : { g : B A & Cancel (=) f g }. (f : A B) `{!Surj (=) f} : { g : B A & Cancel (=) f g }.
Proof. Proof.
exists (λ y, choose (λ x, f x = y) (surjective f y)). exists (λ y, choose (λ x, f x = y) (surj f y)).
intros y. by rewrite (choose_correct (λ x, f x = y) (surjective f y)). intros y. by rewrite (choose_correct (λ x, f x = y) (surj f y)).
Qed. Qed.
(** * Instances *) (** * Instances *)
...@@ -197,7 +197,7 @@ Lemma list_encode_app' `{Countable A} (l1 l2 : list A) acc : ...@@ -197,7 +197,7 @@ Lemma list_encode_app' `{Countable A} (l1 l2 : list A) acc :
Proof. Proof.
revert acc; induction l1; simpl; auto. revert acc; induction l1; simpl; auto.
induction l2 as [|x l IH]; intros acc; simpl; [by rewrite ?(left_id_L _ _)|]. induction l2 as [|x l IH]; intros acc; simpl; [by rewrite ?(left_id_L _ _)|].
by rewrite !(IH (Nat.iter _ _ _)), (associative_L _), x0_iter_x1. by rewrite !(IH (Nat.iter _ _ _)), (assoc_L _), x0_iter_x1.
Qed. Qed.
Program Instance list_countable `{Countable A} : Countable (list A) := Program Instance list_countable `{Countable A} : Countable (list A) :=
{| encode := list_encode 1; decode := list_decode [] 0 |}. {| encode := list_encode 1; decode := list_decode [] 0 |}.
...@@ -211,7 +211,7 @@ Next Obligation. ...@@ -211,7 +211,7 @@ Next Obligation.
{ by intros help l; rewrite help, (right_id_L _ _). } { by intros help l; rewrite help, (right_id_L _ _). }
induction l as [|x l IH] using @rev_ind; intros acc; [done|]. induction l as [|x l IH] using @rev_ind; intros acc; [done|].
rewrite list_encode_app'; simpl; rewrite <-x0_iter_x1, decode_iter; simpl. rewrite list_encode_app'; simpl; rewrite <-x0_iter_x1, decode_iter; simpl.
by rewrite decode_encode_nat; simpl; rewrite IH, <-(associative_L _). by rewrite decode_encode_nat; simpl; rewrite IH, <-(assoc_L _).
Qed. Qed.
Lemma list_encode_app `{Countable A} (l1 l2 : list A) : Lemma list_encode_app `{Countable A} (l1 l2 : list A) :
encode (l1 ++ l2)%list = encode l1 ++ encode l2. encode (l1 ++ l2)%list = encode l1 ++ encode l2.
......
...@@ -12,7 +12,7 @@ Proof. firstorder. Qed. ...@@ -12,7 +12,7 @@ Proof. firstorder. Qed.
Lemma Is_true_reflect (b : bool) : reflect b b. Lemma Is_true_reflect (b : bool) : reflect b b.
Proof. destruct b. by left. right. intros []. Qed. Proof. destruct b. by left. right. intros []. Qed.
Instance: Injective (=) () Is_true. Instance: Inj (=) () Is_true.
Proof. intros [] []; simpl; intuition. Qed. Proof. intros [] []; simpl; intuition. Qed.
(** We introduce [decide_rel] to avoid inefficienct computation due to eager (** We introduce [decide_rel] to avoid inefficienct computation due to eager
......
...@@ -47,7 +47,7 @@ Lemma error_fmap_bind {S E A B C} (f : A → B) (g : B → error S E C) x s : ...@@ -47,7 +47,7 @@ Lemma error_fmap_bind {S E A B C} (f : A → B) (g : B → error S E C) x s :
((f <$> x) = g) s = (x = g f) s. ((f <$> x) = g) s = (x = g f) s.
Proof. by compute; destruct (x s) as [|[??]]. Qed. Proof. by compute; destruct (x s) as [|[??]]. Qed.
Lemma error_associative {S E A B C} (f : A error S E B) (g : B error S E C) x s : Lemma error_assoc {S E A B C} (f : A error S E B) (g : B error S E C) x s :
((x = f) = g) s = (a x; f a = g) s. ((x = f) = g) s = (a x; f a = g) s.
Proof. by compute; destruct (x s) as [|[??]]. Qed. Proof. by compute; destruct (x s) as [|[??]]. Qed.
Lemma error_of_option_bind {S E A B} (f : A option B) o e : Lemma error_of_option_bind {S E A B} (f : A option B) o e :
...@@ -114,7 +114,7 @@ Tactic Notation "error_proceed" := ...@@ -114,7 +114,7 @@ Tactic Notation "error_proceed" :=
| H : (gets _ = _) _ = _ |- _ => rewrite error_left_gets in H | H : (gets _ = _) _ = _ |- _ => rewrite error_left_gets in H
| H : (modify _ = _) _ = _ |- _ => rewrite error_left_modify in H | H : (modify _ = _) _ = _ |- _ => rewrite error_left_modify in H
| H : ((_ <$> _) = _) _ = _ |- _ => rewrite error_fmap_bind in H | H : ((_ <$> _) = _) _ = _ |- _ => rewrite error_fmap_bind in H
| H : ((_ = _) = _) _ = _ |- _ => rewrite error_associative in H | H : ((_ = _) = _) _ = _ |- _ => rewrite error_assoc in H
| H : (error_guard _ _ _) _ = _ |- _ => | H : (error_guard _ _ _) _ = _ |- _ =>
let H' := fresh in apply error_guard_ret in H; destruct H as [H' H] let H' := fresh in apply error_guard_ret in H; destruct H as [H' H]
| _ => progress simplify_equality' | _ => progress simplify_equality'
......
...@@ -108,7 +108,7 @@ Lemma size_union_alt X Y : size (X ∪ Y) = size X + size (Y ∖ X). ...@@ -108,7 +108,7 @@ Lemma size_union_alt X Y : size (X ∪ Y) = size X + size (Y ∖ X).
Proof. Proof.
rewrite <-size_union by solve_elem_of. rewrite <-size_union by solve_elem_of.
setoid_replace (Y X) with ((Y X) X) by solve_elem_of. setoid_replace (Y X) with ((Y X) X) by solve_elem_of.
rewrite <-union_difference, (commutative ()); solve_elem_of. rewrite <-union_difference, (comm ()); solve_elem_of.
Qed. Qed.
Lemma subseteq_size X Y : X Y size X size Y. Lemma subseteq_size X Y : X Y size X size Y.
Proof. intros. rewrite (union_difference X Y), size_union_alt by done. lia. Qed. Proof. intros. rewrite (union_difference X Y), size_union_alt by done. lia. Qed.
......
...@@ -820,28 +820,28 @@ Proof. ...@@ -820,28 +820,28 @@ Proof.
intros ??. apply map_eq. intros. intros ??. apply map_eq. intros.
by rewrite !(lookup_merge f), lookup_empty, (right_id_L None f). by rewrite !(lookup_merge f), lookup_empty, (right_id_L None f).
Qed. Qed.
Lemma merge_commutative m1 m2 : Lemma merge_comm m1 m2 :
( i, f (m1 !! i) (m2 !! i) = f (m2 !! i) (m1 !! i)) ( i, f (m1 !! i) (m2 !! i) = f (m2 !! i) (m1 !! i))
merge f m1 m2 = merge f m2 m1. merge f m1 m2 = merge f m2 m1.
Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed. Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed.
Global Instance: Commutative (=) f Commutative (=) (merge f). Global Instance: Comm (=) f Comm (=) (merge f).
Proof. Proof.
intros ???. apply merge_commutative. intros. by apply (commutative f). intros ???. apply merge_comm. intros. by apply (comm f).
Qed. Qed.
Lemma merge_associative m1 m2 m3 : Lemma merge_assoc m1 m2 m3 :
( i, f (m1 !! i) (f (m2 !! i) (m3 !! i)) = ( i, f (m1 !! i) (f (m2 !! i) (m3 !! i)) =
f (f (m1 !! i) (m2 !! i)) (m3 !! i)) f (f (m1 !! i) (m2 !! i)) (m3 !! i))
merge f m1 (merge f m2 m3) = merge f (merge f m1 m2) m3. merge f m1 (merge f m2 m3) = merge f (merge f m1 m2) m3.
Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed. Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed.
Global Instance: Associative (=) f Associative (=) (merge f). Global Instance: Assoc (=) f Assoc (=) (merge f).
Proof. Proof.
intros ????. apply merge_associative. intros. by apply (associative_L f). intros ????. apply merge_assoc. intros. by apply (assoc_L f).
Qed. Qed.
Lemma merge_idempotent m1 : Lemma merge_idemp m1 :
( i, f (m1 !! i) (m1 !! i) = m1 !! i) merge f m1 m1 = m1. ( i, f (m1 !! i) (m1 !! i) = m1 !! i) merge f m1 m1 = m1.
Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed. Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed.
Global Instance: Idempotent (=) f Idempotent (=) (merge f). Global Instance: IdemP (=) f IdemP (=) (merge f).
Proof. intros ??. apply merge_idempotent. intros. by apply (idempotent f). Qed. Proof. intros ??. apply merge_idemp. intros. by apply (idemp f). Qed.
End merge. End merge.
Section more_merge. Section more_merge.
...@@ -1033,19 +1033,19 @@ Global Instance: LeftId (@eq (M A)) ∅ (union_with f). ...@@ -1033,19 +1033,19 @@ Global Instance: LeftId (@eq (M A)) ∅ (union_with f).
Proof. unfold union_with, map_union_with. apply _. Qed. Proof. unfold union_with, map_union_with. apply _. Qed.
Global Instance: RightId (@eq (M A)) (union_with f). Global Instance: RightId (@eq (M A)) (union_with f).
Proof. unfold union_with, map_union_with. apply _. Qed. Proof. unfold union_with, map_union_with. apply _. Qed.
Lemma union_with_commutative m1 m2 : Lemma union_with_comm m1 m2 :
( i x y, m1 !! i = Some x m2 !! i = Some y f x y = f y x) ( i x y, m1 !! i = Some x m2 !! i = Some y f x y = f y x)
union_with f m1 m2 = union_with f m2 m1. union_with f m1 m2 = union_with f m2 m1.
Proof. Proof.
intros. apply (merge_commutative _). intros i. intros. apply (merge_comm _). intros i.
destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; simpl; eauto. destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; simpl; eauto.
Qed. Qed.
Global Instance: Commutative (=) f Commutative (@eq (M A)) (union_with f). Global Instance: Comm (=) f Comm (@eq (M A)) (union_with f).
Proof. intros ???. apply union_with_commutative. eauto. Qed. Proof. intros ???. apply union_with_comm. eauto. Qed.
Lemma union_with_idempotent m : Lemma union_with_idemp m :
( i x, m !! i = Some x f x x = Some x) union_with f m m = m. ( i x, m !! i = Some x f x x = Some x) union_with f m m = m.
Proof. Proof.
intros. apply (merge_idempotent _). intros i. intros. apply (merge_idemp _). intros i.
destruct (m !! i) eqn:?; simpl; eauto. destruct (m !! i) eqn:?; simpl; eauto.
Qed. Qed.
Lemma alter_union_with (g : A A) m1 m2 i : Lemma alter_union_with (g : A A) m1 m2 i :
...@@ -1100,14 +1100,14 @@ End union_with. ...@@ -1100,14 +1100,14 @@ End union_with.
(** ** Properties of the [union] operation *) (** ** Properties of the [union] operation *)
Global Instance: LeftId (@eq (M A)) () := _. Global Instance: LeftId (@eq (M A)) () := _.
Global Instance: RightId (@eq (M A)) () := _. Global Instance: RightId (@eq (M A)) () := _.
Global Instance: Associative (@eq (M A)) (). Global Instance: Assoc (@eq (M A)) ().
Proof. Proof.
intros A m1 m2 m3. unfold union, map_union, union_with, map_union_with. intros A m1 m2 m3. unfold union, map_union, union_with, map_union_with.
apply (merge_associative _). intros i. apply (merge_assoc _). intros i.
by destruct (m1 !! i), (m2 !! i), (m3 !! i). by destruct (m1 !! i), (m2 !! i), (m3 !! i).
Qed. Qed.
Global Instance: Idempotent (@eq (M A)) (). Global Instance: IdemP (@eq (M A)) ().
Proof. intros A ?. by apply union_with_idempotent. Qed. Proof. intros A ?. by apply union_with_idemp. Qed.
Lemma lookup_union_Some_raw {A} (m1 m2 : M A) i x : Lemma lookup_union_Some_raw {A} (m1 m2 : M A) i x :
(m1 m2) !! i = Some x (m1 m2) !! i = Some x
m1 !! i = Some x (m1 !! i = None m2 !! i = Some x). m1 !! i = Some x (m1 !! i = None m2 !! i = Some x).
...@@ -1140,9 +1140,9 @@ Proof. intro. rewrite lookup_union_Some_raw; intuition. Qed. ...@@ -1140,9 +1140,9 @@ Proof. intro. rewrite lookup_union_Some_raw; intuition. Qed.
Lemma lookup_union_Some_r {A} (m1 m2 : M A) i x : Lemma lookup_union_Some_r {A} (m1 m2 : M A) i x :
m1 m2 m2 !! i = Some x (m1 m2) !! i = Some x. m1 m2 m2 !! i = Some x (m1 m2) !! i = Some x.
Proof. intro. rewrite lookup_union_Some; intuition. Qed. Proof. intro. rewrite lookup_union_Some; intuition. Qed.
Lemma map_union_commutative {A} (m1 m2 : M A) : m1 m2 m1 m2 = m2 m1. Lemma map_union_comm {A} (m1 m2 : M A) : m1 m2 m1 m2 = m2 m1.
Proof. Proof.
intros Hdisjoint. apply (merge_commutative (union_with (λ x _, Some x))). intros Hdisjoint. apply (merge_comm (union_with (λ x _, Some x))).
intros i. specialize (Hdisjoint i). intros i. specialize (Hdisjoint i).
destruct (m1 !! i), (m2 !! i); compute; naive_solver. destruct (m1 !! i), (m2 !! i); compute; naive_solver.
Qed. Qed.
...@@ -1160,7 +1160,7 @@ Proof. ...@@ -1160,7 +1160,7 @@ Proof.
Qed. Qed.
Lemma map_union_subseteq_r {A} (m1 m2 : M A) : m1 m2 m2 m1 m2. Lemma map_union_subseteq_r {A} (m1 m2 : M A) : m1 m2 m2 m1 m2.
Proof. Proof.
intros. rewrite map_union_commutative by done. by apply map_union_subseteq_l. intros. rewrite map_union_comm by done. by apply map_union_subseteq_l.
Qed. Qed.
Lemma map_union_subseteq_l_alt {A} (m1 m2 m3 : M A) : m1 m2 m1 m2 m3. Lemma map_union_subseteq_l_alt {A} (m1 m2 m3 : M A) : m1 m2 m1 m2 m3.
Proof. intros. transitivity m2; auto using map_union_subseteq_l. Qed. Proof. intros. transitivity m2; auto using map_union_subseteq_l. Qed.
...@@ -1175,7 +1175,7 @@ Qed. ...@@ -1175,7 +1175,7 @@ Qed.
Lemma map_union_preserving_r {A} (m1 m2 m3 : M A) : Lemma map_union_preserving_r {A} (m1 m2 m3 : M A) :
m2 m3 m1 m2 m1 m3 m2 m3. m2 m3 m1 m2 m1 m3 m2 m3.
Proof. Proof.
intros. rewrite !(map_union_commutative _ m3) intros. rewrite !(map_union_comm _ m3)
by eauto using map_disjoint_weaken_l. by eauto using map_disjoint_weaken_l.
by apply map_union_preserving_l. by apply map_union_preserving_l.
Qed. Qed.
...@@ -1189,19 +1189,19 @@ Qed. ...@@ -1189,19 +1189,19 @@ Qed.
Lemma map_union_reflecting_r {A} (m1 m2 m3 : M A) : Lemma map_union_reflecting_r {A} (m1 m2 m3 : M A) :
m1 m3 m2 m3 m1 m3 m2 m3 m1 m2. m1 m3 m2 m3 m1 m3 m2 m3 m1 m2.
Proof. Proof.
intros ??. rewrite !(map_union_commutative _ m3) by done. intros ??. rewrite !(map_union_comm _ m3) by done.
by apply map_union_reflecting_l. by apply map_union_reflecting_l.
Qed. Qed.
Lemma map_union_cancel_l {A} (m1 m2 m3 : M A) : Lemma map_union_cancel_l {A} (m1 m2 m3 : M A) :
m1 m3 m2 m3 m3 m1 = m3 m2 m1 = m2. m1 m3 m2 m3 m3 m1 = m3 m2 m1 = m2.
Proof. Proof.
intros. apply (anti_symmetric ()); intros. apply (anti_symm ());
apply map_union_reflecting_l with m3; auto using (reflexive_eq (R:=())). apply map_union_reflecting_l with m3; auto using (reflexive_eq (R:=())).
Qed. Qed.
Lemma map_union_cancel_r {A} (m1 m2 m3 : M A) : Lemma map_union_cancel_r {A} (m1 m2 m3 : M A) :
m1 m3 m2 m3 m1 m3 = m2 m3 m1 = m2. m1 m3 m2 m3 m1 m3 = m2 m3 m1 = m2.
Proof. Proof.
intros. apply (anti_symmetric ()); intros. apply (anti_symm ());
apply map_union_reflecting_r with m3; auto using (reflexive_eq (R:=())). apply map_union_reflecting_r with m3; auto using (reflexive_eq (R:=())).
Qed. Qed.
Lemma map_disjoint_union_l {A} (m1 m2 m3 : M A) : Lemma map_disjoint_union_l {A} (m1 m2 m3 : M A) :
...@@ -1231,7 +1231,7 @@ Qed. ...@@ -1231,7 +1231,7 @@ Qed.
Lemma insert_union_singleton_r {A} (m : M A) i x : Lemma insert_union_singleton_r {A} (m : M A) i x :
m !! i = None <[i:=x]>m = m {[i x]}. m !! i = None <[i:=x]>m = m {[i x]}.
Proof. Proof.
intro. rewrite insert_union_singleton_l, map_union_commutative; [done |]. intro. rewrite insert_union_singleton_l, map_union_comm; [done |].
by apply map_disjoint_singleton_l. by apply map_disjoint_singleton_l.
Qed. Qed.
Lemma map_disjoint_insert_l {A} (m1 m2 : M A) i x : Lemma map_disjoint_insert_l {A} (m1 m2 : M A) i x :
...@@ -1254,12 +1254,12 @@ Lemma map_disjoint_insert_r_2 {A} (m1 m2 : M A) i x : ...@@ -1254,12 +1254,12 @@ Lemma map_disjoint_insert_r_2 {A} (m1 m2 : M A) i x :
Proof. by rewrite map_disjoint_insert_r. Qed. Proof. by rewrite map_disjoint_insert_r. Qed.
Lemma insert_union_l {A} (m1 m2 : M A) i x : Lemma insert_union_l {A} (m1 m2 : M A) i x :
<[i:=x]>(m1 m2) = <[i:=x]>m1 m2. <[i:=x]>(m1 m2) = <[i:=x]>m1 m2.
Proof. by rewrite !insert_union_singleton_l, (associative_L ()). Qed. Proof. by rewrite !insert_union_singleton_l, (assoc_L ()). Qed.
Lemma insert_union_r {A} (m1 m2 : M A) i x : Lemma insert_union_r {A} (m1 m2 : M A) i x :
m1 !! i = None <[i:=x]>(m1 m2) = m1 <[i:=x]>m2. m1 !! i = None <[i:=x]>(m1 m2) = m1 <[i:=x]>m2.
Proof. Proof.
intro. rewrite !insert_union_singleton_l, !(associative_L ()). intro. rewrite !insert_union_singleton_l, !(assoc_L ()).
rewrite (map_union_commutative m1); [done |]. rewrite (map_union_comm m1); [done |].
by apply map_disjoint_singleton_r. by apply map_disjoint_singleton_r.
Qed. Qed.
Lemma foldr_insert_union {A} (m : M A) l : Lemma foldr_insert_union {A} (m : M A) l :
......
...@@ -71,27 +71,27 @@ Proof. ...@@ -71,27 +71,27 @@ Proof.
unfold card; intros. destruct finA as [[|x ?] ??]; simpl in *; [exfalso;lia|]. unfold card; intros. destruct finA as [[|x ?] ??]; simpl in *; [exfalso;lia|].
constructor; exact x. constructor; exact x.
Qed. Qed.
Lemma finite_injective_contains `{finA: Finite A} `{finB: Finite B} (f: A B) Lemma finite_inj_contains `{finA: Finite A} `{finB: Finite B} (f: A B)
`{!Injective (=) (=) f} : f <$> enum A `contains` enum B. `{!Inj (=) (=) f} : f <$> enum A `contains` enum B.
Proof. Proof.
intros. destruct finA, finB. apply NoDup_contains; auto using NoDup_fmap_2. intros. destruct finA, finB. apply NoDup_contains; auto using NoDup_fmap_2.
Qed. Qed.
Lemma finite_injective_Permutation `{Finite A} `{Finite B} (f : A B) Lemma finite_inj_Permutation `{Finite A} `{Finite B} (f : A B)
`{!Injective (=) (=) f} : card A = card B f <$> enum A enum B. `{!Inj (=) (=) f} : card A = card B f <$> enum A enum B.
Proof. Proof.
intros. apply contains_Permutation_length_eq. intros. apply contains_Permutation_length_eq.
* by rewrite fmap_length. * by rewrite fmap_length.
* by apply finite_injective_contains. * by apply finite_inj_contains.
Qed. Qed.
Lemma finite_injective_surjective `{Finite A} `{Finite B} (f : A B) Lemma finite_inj_surj `{Finite A} `{Finite B} (f : A B)
`{!Injective (=) (=) f} : card A = card B Surjective (=) f. `{!Inj (=) (=) f} : card A = card B Surj (=) f.
Proof. Proof.
intros HAB y. destruct (elem_of_list_fmap_2 f (enum A) y) as (x&?&?); eauto. intros HAB y. destruct (elem_of_list_fmap_2 f (enum A) y) as (x&?&?); eauto.
rewrite finite_injective_Permutation; auto using elem_of_enum. rewrite finite_inj_Permutation; auto using elem_of_enum.
Qed. Qed.
Lemma finite_surjective A `{Finite A} B `{Finite B} : Lemma finite_surj A `{Finite A} B `{Finite B} :
0 < card A card B g : B A, Surjective (=) g. 0 < card A card B g : B A, Surj (=) g.
Proof. Proof.
intros [??]. destruct (finite_inhabited A) as [x']; auto with lia. intros [??]. destruct (finite_inhabited A) as [x']; auto with lia.
exists (λ y : B, from_option x' (decode_nat (encode_nat y))). exists (λ y : B, from_option x' (decode_nat (encode_nat y))).
...@@ -99,38 +99,38 @@ Proof. ...@@ -99,38 +99,38 @@ Proof.
{ pose proof (encode_lt_card x); lia. } { pose proof (encode_lt_card x); lia. }
exists y. by rewrite Hy2, decode_encode_nat. exists y. by rewrite Hy2, decode_encode_nat.
Qed. Qed.
Lemma finite_injective A `{Finite A} B `{Finite B} : Lemma finite_inj A `{Finite A} B `{Finite B} :
card A card B f : A B, Injective (=) (=) f. card A card B f : A B, Inj (=) (=) f.
Proof. Proof.
split. split.
* intros. destruct (decide (card A = 0)) as [HA|?]. * intros. destruct (decide (card A = 0)) as [HA|?].
{ exists (card_0_inv B HA). intros y. apply (card_0_inv _ HA y). } { exists (card_0_inv B HA). intros y. apply (card_0_inv _ HA y). }
destruct (finite_surjective A B) as (g&?); auto with lia. destruct (finite_surj A B) as (g&?); auto with lia.
destruct (surjective_cancel g) as (f&?). exists f. apply cancel_injective. destruct (surj_cancel g) as (f&?). exists f. apply cancel_inj.
* intros [f ?]. unfold card. rewrite <-(fmap_length f). * intros [f ?]. unfold card. rewrite <-(fmap_length f).
by apply contains_length, (finite_injective_contains f). by apply contains_length, (finite_inj_contains f).
Qed. Qed.
Lemma finite_bijective A `{Finite A} B `{Finite B} : Lemma finite_bijective A `{Finite A} B `{Finite B} :
card A = card B f : A B, Injective (=) (=) f Surjective (=) f. card A = card B f : A B, Inj (=) (=) f Surj (=) f.
Proof. Proof.
split. split.
* intros; destruct (proj1 (finite_injective A B)) as [f ?]; auto with lia. * intros; destruct (proj1 (finite_inj A B)) as [f ?]; auto with lia.
exists f; auto using (finite_injective_surjective f). exists f; auto using (finite_inj_surj f).
* intros (f&?&?). apply (anti_symmetric ()); apply finite_injective. * intros (f&?&?). apply (anti_symm ()); apply finite_inj.
+ by exists f. + by exists f.
+ destruct (surjective_cancel f) as (g&?); eauto using cancel_injective. + destruct (surj_cancel f) as (g&?); eauto using cancel_inj.
Qed. Qed.
Lemma injective_card `{Finite A} `{Finite B} (f : A B) Lemma inj_card `{Finite A} `{Finite B} (f : A B)
`{!Injective (=) (=) f} : card A card B. `{!Inj (=) (=) f} : card A card B.
Proof. apply finite_injective. eauto. Qed. Proof. apply finite_inj. eauto. Qed.
Lemma surjective_card `{Finite A} `{Finite B} (f : A B) Lemma surj_card `{Finite A} `{Finite B} (f : A B)
`{!Surjective (=) f} : card B card A. `{!Surj (=) f} : card B card A.
Proof. Proof.
destruct (surjective_cancel f) as (g&?). destruct (surj_cancel f) as (g&?).
apply injective_card with g, cancel_injective. apply inj_card with g, cancel_inj.
Qed. Qed.
Lemma bijective_card `{Finite A} `{Finite B} (f : A B) Lemma bijective_card `{Finite A} `{Finite B} (f : A B)
`{!Injective (=) (=) f} `{!Surjective (=) f} : card A = card B. `{!Inj (=) (=) f} `{!Surj (=) f} : card A = card B.
Proof. apply finite_bijective. eauto. Qed. Proof. apply finite_bijective. eauto. Qed.
(** Decidability of quantification over finite types *) (** Decidability of quantification over finite types *)
...@@ -180,7 +180,7 @@ End enc_finite. ...@@ -180,7 +180,7 @@ End enc_finite.
Section bijective_finite. Section bijective_finite.
Context `{Finite A, x y : B, Decision (x = y)} (f : A B) (g : B A). Context `{Finite A, x y : B, Decision (x = y)} (f : A B) (g : B A).
Context `{!Injective (=) (=) f, !Cancel (=) f g}. Context `{!Inj (=) (=) f, !Cancel (=) f g}.
Program Instance bijective_finite: Finite B := {| enum := f <$> enum A |}. Program Instance bijective_finite: Finite B := {| enum := f <$> enum A |}.
Next Obligation. apply (NoDup_fmap_2 _), NoDup_enum. Qed. Next Obligation. apply (NoDup_fmap_2 _), NoDup_enum. Qed.
......
...@@ -89,7 +89,7 @@ Proof. ...@@ -89,7 +89,7 @@ Proof.
* done. * done.
* intros A f [m Hm] i; apply (lookup_partial_alter f m). * intros A f [m Hm] i; apply (lookup_partial_alter f m).
* intros A f [m Hm] i j Hs; apply (lookup_partial_alter_ne f m). * intros A f [m Hm] i j Hs; apply (lookup_partial_alter_ne f m).
by contradict Hs; apply (injective encode). by contradict Hs; apply (inj encode).
* intros A B f [m Hm] i; apply (lookup_fmap f m). * intros A B f [m Hm] i; apply (lookup_fmap f m).
* intros A [m Hm]; unfold map_to_list; simpl. * intros A [m Hm]; unfold map_to_list; simpl.
apply bool_decide_unpack, map_Forall_to_list in Hm; revert Hm. apply bool_decide_unpack, map_Forall_to_list in Hm; revert Hm.
......
This diff is collapsed.
...@@ -35,7 +35,7 @@ Instance nat_eq_dec: ∀ x y : nat, Decision (x = y) := eq_nat_dec. ...@@ -35,7 +35,7 @@ Instance nat_eq_dec: ∀ x y : nat, Decision (x = y) := eq_nat_dec.
Instance nat_le_dec: x y : nat, Decision (x y) := le_dec. Instance nat_le_dec: x y : nat, Decision (x y) := le_dec.
Instance nat_lt_dec: x y : nat, Decision (x < y) := lt_dec. Instance nat_lt_dec: x y : nat, Decision (x < y) := lt_dec.
Instance nat_inhabited: Inhabited nat := populate 0%nat. Instance nat_inhabited: Inhabited nat := populate 0%nat.
Instance: Injective (=) (=) S. Instance: Inj (=) (=) S.
Proof. by injection 1. Qed. Proof. by injection 1. Qed.
Instance: PartialOrder (). Instance: PartialOrder ().
Proof. repeat split; repeat intro; auto with lia. Qed. Proof. repeat split; repeat intro; auto with lia. Qed.
...@@ -110,9 +110,9 @@ Instance positive_inhabited: Inhabited positive := populate 1. ...@@ -110,9 +110,9 @@ Instance positive_inhabited: Inhabited positive := populate 1.
Instance maybe_xO : Maybe xO := λ p, match p with p~0 => Some p | _ => None end. Instance maybe_xO : Maybe xO := λ p, match p with p~0 => Some p | _ => None end.
Instance maybe_x1 : Maybe xI := λ p, match p with p~1 => Some p | _ => None end. Instance maybe_x1 : Maybe xI := λ p, match p with p~1 => Some p | _ => None end.
Instance: Injective (=) (=) (~0). Instance: Inj (=) (=) (~0).
Proof. by injection 1. Qed. Proof. by injection 1. Qed.
Instance: Injective (=) (=) (~1). Instance: Inj (=) (=) (~1).
Proof. by injection 1. Qed. Proof. by injection 1. Qed.
(** Since [positive] represents lists of bits, we define list operations (** Since [positive] represents lists of bits, we define list operations
...@@ -141,9 +141,9 @@ Global Instance: LeftId (=) 1 (++). ...@@ -141,9 +141,9 @@ Global Instance: LeftId (=) 1 (++).
Proof. intros p. by induction p; intros; f_equal'. Qed. Proof. intros p. by induction p; intros; f_equal'. Qed.
Global Instance: RightId (=) 1 (++). Global Instance: RightId (=) 1 (++).
Proof. done. Qed. Proof. done. Qed.
Global Instance: Associative (=) (++). Global Instance: Assoc (=) (++).
Proof. intros ?? p. by induction p; intros; f_equal'. Qed. Proof. intros ?? p. by induction p; intros; f_equal'. Qed.
Global Instance: p : positive, Injective (=) (=) (++ p). Global Instance: p : positive, Inj (=) (=) (++ p).
Proof. intros p ???. induction p; simplify_equality; auto. Qed. Proof. intros p ???. induction p; simplify_equality; auto. Qed.
Lemma Preverse_go_app p1 p2 p3 : Lemma Preverse_go_app p1 p2 p3 :
...@@ -184,7 +184,7 @@ Infix "`mod`" := N.modulo (at level 35) : N_scope. ...@@ -184,7 +184,7 @@ Infix "`mod`" := N.modulo (at level 35) : N_scope.
Arguments N.add _ _ : simpl never. Arguments N.add _ _ : simpl never.
Instance: Injective (=) (=) Npos. Instance: Inj (=) (=) Npos.
Proof. by injection 1. Qed. Proof. by injection 1. Qed.
Instance N_eq_dec: x y : N, Decision (x = y) := N.eq_dec. Instance N_eq_dec: x y : N, Decision (x = y) := N.eq_dec.
...@@ -220,9 +220,9 @@ Infix "`rem`" := Z.rem (at level 35) : Z_scope. ...@@ -220,9 +220,9 @@ Infix "`rem`" := Z.rem (at level 35) : Z_scope.
Infix "≪" := Z.shiftl (at level 35) : Z_scope. Infix "≪" := Z.shiftl (at level 35) : Z_scope.
Infix "≫" := Z.shiftr (at level 35) : Z_scope. Infix "≫" := Z.shiftr (at level 35) : Z_scope.
Instance: Injective (=) (=) Zpos. Instance: Inj (=) (=) Zpos.