Commit 9774ce9c by Robbert Krebbers

### Use scheme - then + then * for bullets.

parent 2e9c3f77
 ... @@ -21,11 +21,11 @@ Instance bset_collection {A} `{∀ x y : A, Decision (x = y)} : ... @@ -21,11 +21,11 @@ Instance bset_collection {A} `{∀ x y : A, Decision (x = y)} : Collection A (bset A). Collection A (bset A). Proof. Proof. split; [split| |]. split; [split| |]. * by intros x ?. - by intros x ?. * by intros x y; rewrite <-(bool_decide_spec (x = y)). - by intros x y; rewrite <-(bool_decide_spec (x = y)). * split. apply orb_prop_elim. apply orb_prop_intro. - split. apply orb_prop_elim. apply orb_prop_intro. * split. apply andb_prop_elim. apply andb_prop_intro. - split. apply andb_prop_elim. apply andb_prop_intro. * intros X Y x; unfold elem_of, bset_elem_of; simpl. - intros X Y x; unfold elem_of, bset_elem_of; simpl. destruct (bset_car X x), (bset_car Y x); simpl; tauto. destruct (bset_car X x), (bset_car Y x); simpl; tauto. Qed. Qed. Instance bset_elem_of_dec {A} x (X : bset A) : Decision (x ∈ X) := _. Instance bset_elem_of_dec {A} x (X : bset A) : Decision (x ∈ X) := _. ... ...
 ... @@ -65,10 +65,10 @@ Lemma coPset_eq t1 t2 : ... @@ -65,10 +65,10 @@ Lemma coPset_eq t1 t2 : Proof. Proof. revert t2. revert t2. induction t1 as [b1|b1 l1 IHl r1 IHr]; intros [b2|b2 l2 r2] Ht ??; simpl in *. induction t1 as [b1|b1 l1 IHl r1 IHr]; intros [b2|b2 l2 r2] Ht ??; simpl in *. * f_equal; apply (Ht 1). - f_equal; apply (Ht 1). * by discriminate (coPLeaf_wf (coPNode b2 l2 r2) b1). - by discriminate (coPLeaf_wf (coPNode b2 l2 r2) b1). * by discriminate (coPLeaf_wf (coPNode b1 l1 r1) b2). - by discriminate (coPLeaf_wf (coPNode b1 l1 r1) b2). * f_equal; [apply (Ht 1)| |]. - f_equal; [apply (Ht 1)| |]. + apply IHl; try apply (λ x, Ht (x~0)); eauto. + apply IHl; try apply (λ x, Ht (x~0)); eauto. + apply IHr; try apply (λ x, Ht (x~1)); eauto. + apply IHr; try apply (λ x, Ht (x~1)); eauto. Qed. Qed. ... @@ -163,13 +163,13 @@ Instance coPset_elem_of_dec (p : positive) (X : coPset) : Decision (p ∈ X) := ... @@ -163,13 +163,13 @@ Instance coPset_elem_of_dec (p : positive) (X : coPset) : Decision (p ∈ X) := Instance coPset_collection : Collection positive coPset. Instance coPset_collection : Collection positive coPset. Proof. Proof. split; [split| |]. split; [split| |]. * by intros ??. - by intros ??. * intros p q. apply elem_to_Pset_singleton. - intros p q. apply elem_to_Pset_singleton. * intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_union; simpl. - intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_union; simpl. by rewrite elem_to_Pset_union, orb_True. by rewrite elem_to_Pset_union, orb_True. * intros [t] [t'] p; unfold elem_of,coPset_elem_of,coPset_intersection; simpl. - intros [t] [t'] p; unfold elem_of,coPset_elem_of,coPset_intersection; simpl. by rewrite elem_to_Pset_intersection, andb_True. by rewrite elem_to_Pset_intersection, andb_True. * intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_difference; simpl. - intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_difference; simpl. by rewrite elem_to_Pset_intersection, by rewrite elem_to_Pset_intersection, elem_to_Pset_opp, andb_True, negb_True. elem_to_Pset_opp, andb_True, negb_True. Qed. Qed. ... @@ -192,7 +192,7 @@ Lemma coPset_finite_spec X : set_finite X ↔ coPset_finite (`X). ... @@ -192,7 +192,7 @@ Lemma coPset_finite_spec X : set_finite X ↔ coPset_finite (`X). Proof. Proof. destruct X as [t Ht]. destruct X as [t Ht]. unfold set_finite, elem_of at 1, coPset_elem_of; simpl; clear Ht; split. unfold set_finite, elem_of at 1, coPset_elem_of; simpl; clear Ht; split. * induction t as [b|b l IHl r IHr]; simpl. - induction t as [b|b l IHl r IHr]; simpl. { destruct b; simpl; [intros [l Hl]|done]. { destruct b; simpl; [intros [l Hl]|done]. by apply (is_fresh (of_list l : Pset)), elem_of_of_list, Hl. } by apply (is_fresh (of_list l : Pset)), elem_of_of_list, Hl. } intros [ll Hll]; rewrite andb_True; split. intros [ll Hll]; rewrite andb_True; split. ... @@ -200,7 +200,7 @@ Proof. ... @@ -200,7 +200,7 @@ Proof. rewrite elem_of_list_omap; intros; exists (i~0); auto. rewrite elem_of_list_omap; intros; exists (i~0); auto. + apply IHr; exists (omap (maybe (~1)) ll); intros i. + apply IHr; exists (omap (maybe (~1)) ll); intros i. rewrite elem_of_list_omap; intros; exists (i~1); auto. rewrite elem_of_list_omap; intros; exists (i~1); auto. * induction t as [b|b l IHl r IHr]; simpl; [by exists []; destruct b|]. - induction t as [b|b l IHl r IHr]; simpl; [by exists []; destruct b|]. rewrite andb_True; intros [??]; destruct IHl as [ll ?], IHr as [rl ?]; auto. rewrite andb_True; intros [??]; destruct IHl as [ll ?], IHr as [rl ?]; auto. exists ([1] ++ ((~0) <\$> ll) ++ ((~1) <\$> rl))%list; intros [i|i|]; simpl; exists ([1] ++ ((~0) <\$> ll) ++ ((~1) <\$> rl))%list; intros [i|i|]; simpl; rewrite elem_of_cons, elem_of_app, !elem_of_list_fmap; naive_solver. rewrite elem_of_cons, elem_of_app, !elem_of_list_fmap; naive_solver. ... @@ -237,8 +237,8 @@ Qed. ... @@ -237,8 +237,8 @@ Qed. Lemma coPpick_elem_of X : ¬set_finite X → coPpick X ∈ X. Lemma coPpick_elem_of X : ¬set_finite X → coPpick X ∈ X. Proof. Proof. destruct X as [t ?]; unfold coPpick; destruct (coPpick_raw _) as [j|] eqn:?. destruct X as [t ?]; unfold coPpick; destruct (coPpick_raw _) as [j|] eqn:?. * by intros; apply coPpick_raw_elem_of. - by intros; apply coPpick_raw_elem_of. * by intros []; apply coPset_finite_spec, coPpick_raw_None. - by intros []; apply coPset_finite_spec, coPpick_raw_None. Qed. Qed. (** * Conversion to psets *) (** * Conversion to psets *) ... @@ -270,8 +270,8 @@ Fixpoint of_Pset_raw (t : Pmap_raw ()) : coPset_raw := ... @@ -270,8 +270,8 @@ Fixpoint of_Pset_raw (t : Pmap_raw ()) : coPset_raw := Lemma of_Pset_wf t : Pmap_wf t → coPset_wf (of_Pset_raw t). Lemma of_Pset_wf t : Pmap_wf t → coPset_wf (of_Pset_raw t). Proof. Proof. induction t as [|[] l IHl r IHr]; simpl; rewrite ?andb_True; auto. induction t as [|[] l IHl r IHr]; simpl; rewrite ?andb_True; auto. * intros [??]; destruct l as [|[]], r as [|[]]; simpl in *; auto. - intros [??]; destruct l as [|[]], r as [|[]]; simpl in *; auto. * destruct l as [|[]], r as [|[]]; simpl in *; rewrite ?andb_true_r; - destruct l as [|[]], r as [|[]]; simpl in *; rewrite ?andb_true_r; rewrite ?andb_True; rewrite ?andb_True in IHl, IHr; intuition. rewrite ?andb_True; rewrite ?andb_True in IHl, IHr; intuition. Qed. Qed. Lemma elem_of_of_Pset_raw i t : e_of i (of_Pset_raw t) ↔ t !! i = Some (). Lemma elem_of_of_Pset_raw i t : e_of i (of_Pset_raw t) ↔ t !! i = Some (). ... @@ -327,9 +327,9 @@ Definition coPset_suffixes (p : positive) : coPset := ... @@ -327,9 +327,9 @@ Definition coPset_suffixes (p : positive) : coPset := Lemma elem_coPset_suffixes p q : p ∈ coPset_suffixes q ↔ ∃ q', p = q' ++ q. Lemma elem_coPset_suffixes p q : p ∈ coPset_suffixes q ↔ ∃ q', p = q' ++ q. Proof. Proof. unfold elem_of, coPset_elem_of; simpl; split. unfold elem_of, coPset_elem_of; simpl; split. * revert p; induction q; intros [?|?|]; simpl; - revert p; induction q; intros [?|?|]; simpl; rewrite ?coPset_elem_of_node; naive_solver. rewrite ?coPset_elem_of_node; naive_solver. * by intros [q' ->]; induction q; simpl; rewrite ?coPset_elem_of_node. - by intros [q' ->]; induction q; simpl; rewrite ?coPset_elem_of_node. Qed. Qed. Lemma coPset_suffixes_infinite p : ¬set_finite (coPset_suffixes p). Lemma coPset_suffixes_infinite p : ¬set_finite (coPset_suffixes p). Proof. Proof. ... ...
 ... @@ -48,8 +48,8 @@ Section simple_collection. ... @@ -48,8 +48,8 @@ Section simple_collection. Lemma elem_of_subseteq_singleton x X : x ∈ X ↔ {[ x ]} ⊆ X. Lemma elem_of_subseteq_singleton x X : x ∈ X ↔ {[ x ]} ⊆ X. Proof. Proof. split. split. * intros ??. rewrite elem_of_singleton. by intros ->. - intros ??. rewrite elem_of_singleton. by intros ->. * intros Ex. by apply (Ex x), elem_of_singleton. - intros Ex. by apply (Ex x), elem_of_singleton. Qed. Qed. Global Instance singleton_proper : Proper ((=) ==> (≡)) (singleton (B:=C)). Global Instance singleton_proper : Proper ((=) ==> (≡)) (singleton (B:=C)). Proof. by repeat intro; subst. Qed. Proof. by repeat intro; subst. Qed. ... @@ -59,9 +59,9 @@ Section simple_collection. ... @@ -59,9 +59,9 @@ Section simple_collection. Lemma elem_of_union_list Xs x : x ∈ ⋃ Xs ↔ ∃ X, X ∈ Xs ∧ x ∈ X. Lemma elem_of_union_list Xs x : x ∈ ⋃ Xs ↔ ∃ X, X ∈ Xs ∧ x ∈ X. Proof. Proof. split. split. * induction Xs; simpl; intros HXs; [by apply elem_of_empty in HXs|]. - induction Xs; simpl; intros HXs; [by apply elem_of_empty in HXs|]. setoid_rewrite elem_of_cons. apply elem_of_union in HXs. naive_solver. setoid_rewrite elem_of_cons. apply elem_of_union in HXs. naive_solver. * intros [X []]. induction 1; simpl; [by apply elem_of_union_l |]. - intros [X []]. induction 1; simpl; [by apply elem_of_union_l |]. intros. apply elem_of_union_r; auto. intros. apply elem_of_union_r; auto. Qed. Qed. Lemma non_empty_singleton x : ({[ x ]} : C) ≢ ∅. Lemma non_empty_singleton x : ({[ x ]} : C) ≢ ∅. ... @@ -113,9 +113,9 @@ Section of_option_list. ... @@ -113,9 +113,9 @@ Section of_option_list. Lemma elem_of_of_list (x : A) l : x ∈ of_list l ↔ x ∈ l. Lemma elem_of_of_list (x : A) l : x ∈ of_list l ↔ x ∈ l. Proof. Proof. split. split. * induction l; simpl; [by rewrite elem_of_empty|]. - induction l; simpl; [by rewrite elem_of_empty|]. rewrite elem_of_union,elem_of_singleton; intros [->|?]; constructor; auto. rewrite elem_of_union,elem_of_singleton; intros [->|?]; constructor; auto. * induction 1; simpl; rewrite elem_of_union, elem_of_singleton; auto. - induction 1; simpl; rewrite elem_of_union, elem_of_singleton; auto. Qed. Qed. End of_option_list. End of_option_list. ... @@ -356,11 +356,11 @@ Section collection_ops. ... @@ -356,11 +356,11 @@ Section collection_ops. Forall2 (∈) xs Xs ∧ y ∈ Y ∧ foldr (λ x, (≫= f x)) (Some y) xs = Some x. Forall2 (∈) xs Xs ∧ y ∈ Y ∧ foldr (λ x, (≫= f x)) (Some y) xs = Some x. Proof. Proof. split. split. * revert x. induction Xs; simpl; intros x HXs; [eexists [], x; intuition|]. - revert x. induction Xs; simpl; intros x HXs; [eexists [], x; intuition|]. rewrite elem_of_intersection_with in HXs; destruct HXs as (x1&x2&?&?&?). rewrite elem_of_intersection_with in HXs; destruct HXs as (x1&x2&?&?&?). destruct (IHXs x2) as (xs & y & hy & ? & ?); trivial. destruct (IHXs x2) as (xs & y & hy & ? & ?); trivial. eexists (x1 :: xs), y. intuition (simplify_option_equality; auto). eexists (x1 :: xs), y. intuition (simplify_option_equality; auto). * intros (xs & y & Hxs & ? & Hx). revert x Hx. - intros (xs & y & Hxs & ? & Hx). revert x Hx. induction Hxs; intros; simplify_option_equality; [done |]. induction Hxs; intros; simplify_option_equality; [done |]. rewrite elem_of_intersection_with. naive_solver. rewrite elem_of_intersection_with. naive_solver. Qed. Qed. ... @@ -389,8 +389,8 @@ Section NoDup. ... @@ -389,8 +389,8 @@ Section NoDup. Global Instance: Proper (R ==> (≡) ==> iff) elem_of_upto. Global Instance: Proper (R ==> (≡) ==> iff) elem_of_upto. Proof. Proof. intros ?? E1 ?? E2. split; intros [z [??]]; exists z. intros ?? E1 ?? E2. split; intros [z [??]]; exists z. * rewrite <-E1, <-E2; intuition. - rewrite <-E1, <-E2; intuition. * rewrite E1, E2; intuition. - rewrite E1, E2; intuition. Qed. Qed. Global Instance: Proper ((≡) ==> iff) set_NoDup. Global Instance: Proper ((≡) ==> iff) set_NoDup. Proof. firstorder. Qed. Proof. firstorder. Qed. ... @@ -575,8 +575,8 @@ Section collection_monad. ... @@ -575,8 +575,8 @@ Section collection_monad. l ∈ mapM f k ↔ Forall2 (λ x y, x ∈ f y) l k. l ∈ mapM f k ↔ Forall2 (λ x y, x ∈ f y) l k. Proof. Proof. split. split. * revert l. induction k; solve_elem_of. - revert l. induction k; solve_elem_of. * induction 1; solve_elem_of. - induction 1; solve_elem_of. Qed. Qed. Lemma collection_mapM_length {A B} (f : A → M B) l k : Lemma collection_mapM_length {A B} (f : A → M B) l k : l ∈ mapM f k → length l = length k. l ∈ mapM f k → length l = length k. ... ...
 ... @@ -20,9 +20,9 @@ Proof. by exists (elements X); intros; rewrite elem_of_elements. Qed. ... @@ -20,9 +20,9 @@ Proof. by exists (elements X); intros; rewrite elem_of_elements. Qed. Global Instance elements_proper: Proper ((≡) ==> (≡ₚ)) (elements (C:=C)). Global Instance elements_proper: Proper ((≡) ==> (≡ₚ)) (elements (C:=C)). Proof. Proof. intros ?? E. apply NoDup_Permutation. intros ?? E. apply NoDup_Permutation. * apply NoDup_elements. - apply NoDup_elements. * apply NoDup_elements. - apply NoDup_elements. * intros. by rewrite !elem_of_elements, E. - intros. by rewrite !elem_of_elements, E. Qed. Qed. Global Instance collection_size_proper: Proper ((≡) ==> (=)) (@size C _). Global Instance collection_size_proper: Proper ((≡) ==> (=)) (@size C _). Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed. Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed. ... @@ -45,9 +45,9 @@ Lemma size_singleton (x : A) : size {[ x ]} = 1. ... @@ -45,9 +45,9 @@ Lemma size_singleton (x : A) : size {[ x ]} = 1. Proof. Proof. change (length (elements {[ x ]}) = length [x]). change (length (elements {[ x ]}) = length [x]). apply Permutation_length, NoDup_Permutation. apply Permutation_length, NoDup_Permutation. * apply NoDup_elements. - apply NoDup_elements. * apply NoDup_singleton. - apply NoDup_singleton. * intros y. - intros y. by rewrite elem_of_elements, elem_of_singleton, elem_of_list_singleton. by rewrite elem_of_elements, elem_of_singleton, elem_of_list_singleton. Qed. Qed. Lemma size_singleton_inv X x y : size X = 1 → x ∈ X → y ∈ X → x = y. Lemma size_singleton_inv X x y : size X = 1 → x ∈ X → y ∈ X → x = y. ... @@ -59,8 +59,8 @@ Qed. ... @@ -59,8 +59,8 @@ Qed. Lemma collection_choose_or_empty X : (∃ x, x ∈ X) ∨ X ≡ ∅. Lemma collection_choose_or_empty X : (∃ x, x ∈ X) ∨ X ≡ ∅. Proof. Proof. destruct (elements X) as [|x l] eqn:HX; [right|left]. destruct (elements X) as [|x l] eqn:HX; [right|left]. * apply equiv_empty; intros x. by rewrite <-elem_of_elements, HX, elem_of_nil. - apply equiv_empty; intros x. by rewrite <-elem_of_elements, HX, elem_of_nil. * exists x. rewrite <-elem_of_elements, HX. by left. - exists x. rewrite <-elem_of_elements, HX. by left. Qed. Qed. Lemma collection_choose X : X ≢ ∅ → ∃ x, x ∈ X. Lemma collection_choose X : X ≢ ∅ → ∃ x, x ∈ X. Proof. intros. by destruct (collection_choose_or_empty X). Qed. Proof. intros. by destruct (collection_choose_or_empty X). Qed. ... @@ -75,17 +75,17 @@ Lemma size_1_elem_of X : size X = 1 → ∃ x, X ≡ {[ x ]}. ... @@ -75,17 +75,17 @@ Lemma size_1_elem_of X : size X = 1 → ∃ x, X ≡ {[ x ]}. Proof. Proof. intros E. destruct (size_pos_elem_of X); auto with lia. intros E. destruct (size_pos_elem_of X); auto with lia. exists x. apply elem_of_equiv. split. exists x. apply elem_of_equiv. split. * rewrite elem_of_singleton. eauto using size_singleton_inv. - rewrite elem_of_singleton. eauto using size_singleton_inv. * solve_elem_of. - solve_elem_of. Qed. Qed. Lemma size_union X Y : X ∩ Y ≡ ∅ → size (X ∪ Y) = size X + size Y. Lemma size_union X Y : X ∩ Y ≡ ∅ → size (X ∪ Y) = size X + size Y. Proof. Proof. intros [E _]. unfold size, collection_size. simpl. rewrite <-app_length. intros [E _]. unfold size, collection_size. simpl. rewrite <-app_length. apply Permutation_length, NoDup_Permutation. apply Permutation_length, NoDup_Permutation. * apply NoDup_elements. - apply NoDup_elements. * apply NoDup_app; repeat split; try apply NoDup_elements. - apply NoDup_app; repeat split; try apply NoDup_elements. intros x; rewrite !elem_of_elements; solve_elem_of. intros x; rewrite !elem_of_elements; solve_elem_of. * intros. by rewrite elem_of_app, !elem_of_elements, elem_of_union. - intros. by rewrite elem_of_app, !elem_of_elements, elem_of_union. Qed. Qed. Instance elem_of_dec_slow (x : A) (X : C) : Decision (x ∈ X) | 100. Instance elem_of_dec_slow (x : A) (X : C) : Decision (x ∈ X) | 100. Proof. Proof. ... @@ -129,9 +129,9 @@ Proof. ... @@ -129,9 +129,9 @@ Proof. intros ? Hemp Hadd. apply well_founded_induction with (⊂). intros ? Hemp Hadd. apply well_founded_induction with (⊂). { apply collection_wf. } { apply collection_wf. } intros X IH. destruct (collection_choose_or_empty X) as [[x ?]|HX]. intros X IH. destruct (collection_choose_or_empty X) as [[x ?]|HX]. * rewrite (union_difference {[ x ]} X) by solve_elem_of. - rewrite (union_difference {[ x ]} X) by solve_elem_of. apply Hadd. solve_elem_of. apply IH; solve_elem_of. apply Hadd. solve_elem_of. apply IH; solve_elem_of. * by rewrite HX. - by rewrite HX. Qed. Qed. Lemma collection_fold_ind {B} (P : B → C → Prop) (f : A → B → B) (b : B) : Lemma collection_fold_ind {B} (P : B → C → Prop) (f : A → B → B) (b : B) : Proper ((=) ==> (≡) ==> iff) P → Proper ((=) ==> (≡) ==> iff) P → ... @@ -143,9 +143,9 @@ Proof. ... @@ -143,9 +143,9 @@ Proof. { intros help ?. apply help; [apply NoDup_elements|]. { intros help ?. apply help; [apply NoDup_elements|]. symmetry. apply elem_of_elements. } symmetry. apply elem_of_elements. } induction 1 as [|x l ?? IH]; simpl. induction 1 as [|x l ?? IH]; simpl. * intros X HX. setoid_rewrite elem_of_nil in HX. - intros X HX. setoid_rewrite elem_of_nil in HX. rewrite equiv_empty. done. solve_elem_of. rewrite equiv_empty. done. solve_elem_of. * intros X HX. setoid_rewrite elem_of_cons in HX. - intros X HX. setoid_rewrite elem_of_cons in HX. rewrite (union_difference {[ x ]} X) by solve_elem_of. rewrite (union_difference {[ x ]} X) by solve_elem_of. apply Hadd. solve_elem_of. apply IH. solve_elem_of. apply Hadd. solve_elem_of. apply IH. solve_elem_of. Qed. Qed. ... ...
This diff is collapsed.
 ... @@ -30,8 +30,8 @@ Proof. ... @@ -30,8 +30,8 @@ Proof. destruct finA as [xs Hxs HA]; unfold encode_nat, encode, card; simpl. destruct finA as [xs Hxs HA]; unfold encode_nat, encode, card; simpl. rewrite Nat2Pos.id by done; simpl. rewrite Nat2Pos.id by done; simpl. destruct (list_find _ xs) as [[i y]|] eqn:?; simpl. destruct (list_find _ xs) as [[i y]|] eqn:?; simpl. * destruct (list_find_Some (x =) xs i y); eauto using lookup_lt_Some. - destruct (list_find_Some (x =) xs i y); eauto using lookup_lt_Some. * destruct xs; simpl. exfalso; eapply not_elem_of_nil, (HA x). lia. - destruct xs; simpl. exfalso; eapply not_elem_of_nil, (HA x). lia. Qed. Qed. Lemma encode_decode A `{finA: Finite A} i : Lemma encode_decode A `{finA: Finite A} i : i < card A → ∃ x, decode_nat i = Some x ∧ encode_nat x = i. i < card A → ∃ x, decode_nat i = Some x ∧ encode_nat x = i. ... @@ -80,8 +80,8 @@ Lemma finite_inj_Permutation `{Finite A} `{Finite B} (f : A → B) ... @@ -80,8 +80,8 @@ Lemma finite_inj_Permutation `{Finite A} `{Finite B} (f : A → B) `{!Inj (=) (=) 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_inj_contains. - by apply finite_inj_contains. Qed. Qed. Lemma finite_inj_surj `{Finite A} `{Finite B} (f : A → B) Lemma finite_inj_surj `{Finite A} `{Finite B} (f : A → B) `{!Inj (=) (=) f} : card A = card B → Surj (=) f. `{!Inj (=) (=) f} : card A = card B → Surj (=) f. ... @@ -103,20 +103,20 @@ Lemma finite_inj A `{Finite A} B `{Finite B} : ... @@ -103,20 +103,20 @@ Lemma finite_inj A `{Finite A} B `{Finite B} : card A ≤ card B ↔ ∃ f : A → B, Inj (=) (=) 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_surj A B) as (g&?); auto with lia. destruct (finite_surj A B) as (g&?); auto with lia. destruct (surj_cancel g) as (f&?). exists f. apply cancel_inj. 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_inj_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, Inj (=) (=) f ∧ Surj (=) f. card A = card B ↔ ∃ f : A → B, Inj (=) (=) f ∧ Surj (=) f. Proof. Proof. split. split. * intros; destruct (proj1 (finite_inj A B)) as [f ?]; auto with lia. - intros; destruct (proj1 (finite_inj A B)) as [f ?]; auto with lia. exists f; auto using (finite_inj_surj f). exists f; auto using (finite_inj_surj f). * intros (f&?&?). apply (anti_symm (≤)); apply finite_inj. - intros (f&?&?). apply (anti_symm (≤)); apply finite_inj. + by exists f. + by exists f. + destruct (surj_cancel f) as (g&?); eauto using cancel_inj. + destruct (surj_cancel f) as (g&?); eauto using cancel_inj. Qed. Qed. ... @@ -193,8 +193,8 @@ Program Instance option_finite `{Finite A} : Finite (option A) := ... @@ -193,8 +193,8 @@ Program Instance option_finite `{Finite A} : Finite (option A) := {| enum := None :: Some <\$> enum A |}. {| enum := None :: Some <\$> enum A |}. Next Obligation. Next Obligation. constructor. constructor. * rewrite elem_of_list_fmap. by intros (?&?&?). - rewrite elem_of_list_fmap. by intros (?&?&?). * apply (NoDup_fmap_2 _); auto using NoDup_enum. - apply (NoDup_fmap_2 _); auto using NoDup_enum. Qed. Qed. Next Obligation. Next Obligation. intros ??? [x|]; [right|left]; auto. intros ??? [x|]; [right|left]; auto. ... @@ -221,9 +221,9 @@ Program Instance sum_finite `{Finite A, Finite B} : Finite (A + B)%type := ... @@ -221,9 +221,9 @@ Program Instance sum_finite `{Finite A, Finite B} : Finite (A + B)%type := {| enum := (inl <\$> enum A) ++ (inr <\$> enum B) |}. {| enum := (inl <\$> enum A) ++ (inr <\$> enum B) |}. Next Obligation. Next Obligation. intros. apply NoDup_app; split_ands. intros. apply NoDup_app; split_ands. * apply (NoDup_fmap_2 _). by apply NoDup_enum. - apply (NoDup_fmap_2 _). by apply NoDup_enum. * intro. rewrite !elem_of_list_fmap. intros (?&?&?) (?&?&?); congruence. - intro. rewrite !elem_of_list_fmap. intros (?&?&?) (?&?&?); congruence. * apply (NoDup_fmap_2 _). by apply NoDup_enum. - apply (NoDup_fmap_2 _). by apply NoDup_enum. Qed. Qed. Next Obligation. Next Obligation. intros ?????? [x|y]; rewrite elem_of_app, !elem_of_list_fmap; intros ?????? [x|y]; rewrite elem_of_app, !elem_of_list_fmap; ... @@ -238,20 +238,20 @@ Next Obligation. ... @@ -238,20 +238,20 @@ Next Obligation. intros ??????. induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl. intros ??????. induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl. { constructor. } { constructor. } apply NoDup_app; split_ands. apply NoDup_app; split_ands. * by apply (NoDup_fmap_2 _), NoDup_enum. - by apply (NoDup_fmap_2 _), NoDup_enum. * intros [? y]. rewrite elem_of_list_fmap. intros (?&?&?); simplify_equality. - intros [? y]. rewrite elem_of_list_fmap. intros (?&?&?); simplify_equality. clear IH. induction Hxs as [|x' xs ?? IH]; simpl. clear IH. induction Hxs as [|x' xs ?? IH]; simpl. { rewrite elem_of_nil. tauto. } { rewrite elem_of_nil. tauto. } rewrite elem_of_app, elem_of_list_fmap. rewrite elem_of_app, elem_of_list_fmap. intros [(?&?&?)|?]; simplify_equality. intros [(?&?&?)|?]; simplify_equality. + destruct Hx. by left. + destruct Hx. by left. + destruct IH. by intro; destruct Hx; right. auto. + destruct IH. by intro; destruct Hx; right. auto. * done. - done. Qed. Qed. Next Obligation. Next Obligation. intros ?????? [x y]. induction (elem_of_enum x); simpl. intros ?????? [x y]. induction (elem_of_enum x); simpl. * rewrite elem_of_app, !elem_of_list_fmap. eauto using @elem_of_enum. - rewrite elem_of_app, !elem_of_list_fmap. eauto using @elem_of_enum. * rewrite elem_of_app; eauto. - rewrite elem_of_app; eauto. Qed. Qed. Lemma prod_card `{Finite A} `{Finite B} : card (A * B) = card A * card B. Lemma prod_card `{Finite A} `{Finite B} : card (A * B) = card A * card B. Proof. Proof. ... @@ -272,13 +272,13 @@ Next Obligation. ... @@ -272,13 +272,13 @@ Next Obligation. revert IH. generalize (list_enum (enum A) n). intros l Hl. revert IH. generalize (list_enum (enum A) n). intros l Hl. induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl; auto; [constructor |]. induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl; auto; [constructor |]. apply NoDup_app; split_ands. apply NoDup_app; split_ands. * by apply (NoDup_fmap_2 _). - by apply (NoDup_fmap_2 _). * intros [k1 Hk1]. clear Hxs IH. rewrite elem_of_list_fmap. - intros [k1 Hk1]. clear Hxs IH. rewrite elem_of_list_fmap. intros ([k2 Hk2]&?&?) Hxk2; simplify_equality'. destruct Hx. revert Hxk2. intros ([k2 Hk2]&?&?) Hxk2; simplify_equality'. destruct Hx. revert Hxk2. induction xs as [|x' xs IH]; simpl in *; [by rewrite elem_of_nil |]. induction xs as [|x' xs IH]; simpl in *; [by rewrite elem_of_nil |]. rewrite elem_of_app, elem_of_list_fmap, elem_of_cons. rewrite elem_of_app, elem_of_list_fmap, elem_of_cons. intros [([??]&?&?)|?]; simplify_equality'; auto. intros [([??]&?&?)|?]; simplify_equality'; auto. * apply IH. - apply IH. Qed. Qed. Next Obligation. Next Obligation. intros ???? [l Hl]. revert l Hl. intros ???? [l Hl]. revert l Hl. ... @@ -286,9 +286,9 @@ Next Obligation. ... @@ -286,9 +286,9 @@ Next Obligation. { apply elem_of_list_singleton. by apply (sig_eq_pi _). } { apply elem_of_list_singleton. by apply (sig_eq_pi _). } revert IH. generalize (list_enum (enum A) n). intros k Hk. revert IH. generalize (list_enum (enum A) n). intros k Hk. induction (elem_of_enum x) as [x xs|x xs]; simpl in *. induction (elem_of_enum x) as [x xs|x xs]; simpl in *. * rewrite elem_of_app, elem_of_list_fmap. left. injection Hl. intros Hl'. - rewrite elem_of_app, elem_of_list_fmap. left. injection Hl. intros Hl'. eexists (l↾Hl'). split. by apply (sig_eq_pi _). done. eexists (l↾Hl'). split. by apply (sig_eq_pi _). done. * rewrite elem_of_app. eauto. - rewrite elem_of_app. eauto. Qed. Qed. Lemma list_card `{Finite A} n : card { l | length l = n } = card A ^ n. Lemma list_card `{Finite A} n : card { l | length l = n } = card A ^ n. Proof. Proof. ... ...
 ... @@ -37,8 +37,8 @@ Lemma gmap_partial_alter_wf `{Countable K} {A} (f : option A → option A) m i : ... @@ -37,8 +37,8 @@ Lemma gmap_partial_alter_wf `{Countable K} {A} (f : option A → option A) m i : gmap_wf m → gmap_wf (partial_alter f (encode i) m). gmap_wf m → gmap_wf (partial_alter f (encode i) m). Proof. Proof. intros Hm p x. destruct (decide (encode i = p)) as [<-|?]. intros Hm p x. destruct (decide (encode i = p)) as [<-|?]. * rewrite decode_encode; eauto. - rewrite decode_encode; eauto. * rewrite lookup_partial_alter_ne by done. by apply Hm. - rewrite lookup_partial_alter_ne by done. by apply Hm. Qed. Qed. Instance gmap_partial_alter `{Countable K} {A} : Instance gmap_partial_alter `{Countable K} {A} : PartialAlter K A (gmap K A) := λ f i m, PartialAlter K A (gmap K A) := λ f i m, ... @@ -78,7 +78,7 @@ Instance gmap_to_list `{Countable K} {A} : FinMapToList K A (gmap K A) := λ m, ... @@ -78,7 +78,7 @@ Instance gmap_to_list `{Countable K} {A} : FinMapToList K A (gmap K A) := λ m, Instance gmap_finmap `{Countable K} : FinMap K (gmap K). Instance gmap_finmap `{Countable K} : FinMap K (gmap K). Proof. Proof. split. split. * unfold lookup; intros A [m1 Hm1] [m2 Hm2] Hm. - unfold lookup; intros A [m1 Hm1] [m2 Hm2] Hm. apply gmap_eq, map_eq; intros i; simpl in *. apply gmap_eq, map_eq; intros i; simpl in *. apply bool_decide_unpack in Hm1; apply bool_decide_unpack in Hm2. apply bool_decide_unpack in Hm1; apply bool_decide_unpack in Hm2. apply option_eq; intros x; split; intros Hi. apply option_eq; intros x; split; intros Hi. ... @@ -86,12 +86,12 @@ Proof. ... @@ -86,12 +86,12 @@ Proof. by destruct (decode i); simplify_equality'; rewrite <-Hm. by destruct (decode i); simplify_equality'; rewrite <-Hm. + pose proof (Hm2 i x Hi); simpl in *. + pose proof (Hm2 i x Hi); simpl in *. by destruct (decode i); simplify_equality'; rewrite Hm. by destruct (decode i); simplify_equality'; rewrite Hm.