proposition: Lemma elements_filter {elt} (m : M.t elt) (P : M.key → elt → bool) : M.elements (P.filter P m) = filter (fun p => P (fst p) (snd p)) (M.elements m).
proof: Proof. unfold P.filter. apply P.fold_rec; intros. - rewrite (proj1 (P.elements_Empty m0) H); simpl. apply P.elements_empty. - destruct (P k e) eqn:Heqe. + apply add_equal_iff in H1. Abort. Lemma length_elements_filter {elt} (m : M.t elt) k v (P : M.key * elt → bool) : length (filter P (M.elements (M.add k v m))) = length (filter P ((k, v) :: M.elements m)). Proof. Abort. Theorem elements_rect {elt} (P : list (M.key * elt) → Type) : (∀ m1 m2, M.Equal m1 m2 → P (M.elements m1) → P (M.elements m2)) → ∀ m k v, P ((k, v) :: M.elements m) → P (M.elements (M.add k v m)). Proof. Abort. Lemma ThreeArrows_card_3 : cardinality ThreeArrows = 3%nat. Proof. assert (P.transpose_neqkey M.Equal (λ (k : M.key) (e : nat) (m : M.t nat), if (let '(dom, cod) := k in λ v : nat, (dom =? v)%nat && (cod =? v)%nat) e then k +=> e m else m)). { intros ??????. destruct k, k'. assert (n ≠ n1 \/ n0 ≠ n2). { destruct (Nat.eq_dec n n1); subst. - right; congruence. - left; assumption. } destruct ((n =? e)%nat && (n0 =? e)%nat) eqn:Heqe. - apply andb_true_iff in Heqe. destruct Heqe. apply Nat.eqb_eq in H1. apply Nat.eqb_eq in H2. subst. destruct ((n1 =? e')%nat && (n2 =? e')%nat) eqn:Heqe2. * apply andb_true_iff in Heqe2. destruct Heqe2. apply Nat.eqb_eq in H1. apply Nat.eqb_eq in H2. subst. apply add_associative. intros; congruence. * reflexivity. - destruct ((n1 =? e')%nat && (n2 =? e')%nat) eqn:Heqe2. * apply andb_true_iff in Heqe2. destruct Heqe2. apply Nat.eqb_eq in H1. apply Nat.eqb_eq in H2. subst. reflexivity. * reflexivity. } assert (Proper (eq ==> eq ==> M.Equal ==> M.Equal) (λ (k : M.key) (e : nat) (m : M.t nat), if (let '(dom, cod) := k in λ v : nat, (dom =? v)%nat && (cod =? v)%nat) e then k +=> e m else m)). { intros ?????????. destruct x, y; subst. inversion H0; clear H0; subst. destruct ((n1 =? y0)%nat && (n2 =? y0)%nat) eqn:Heqe. - apply andb_true_iff in Heqe. destruct Heqe. apply Nat.eqb_eq in H0. apply Nat.eqb_eq in H1. subst. rewrite H2; reflexivity. - assumption. } unfold cardinality; simpl. unfold P.filter; simpl. repeat (rewrite P.fold_add; eauto; relational; simpl); try (apply not_in_mapsto_iff; intros; repeat (unfold not; intros; simplify_maps; try congruence)). rewrite P.fold_Empty; auto; [| apply M.empty_1 ]. assert (P.transpose_neqkey eq (λ (_ : M.key) (_ : nat), S)) by proper. rewrite P.cardinal_fold. repeat (rewrite P.fold_add; eauto; relational; simpl); try (apply not_in_mapsto_iff; intros; repeat (unfold not; intros; simplify_maps; try congruence)). rewrite P.fold_Empty; auto; apply M.empty_1. Qed.
imports: Coq.Structures.DecidableTypeEx Coq.FSets.FMapFacts Category.Lib.FMapExt Coq.Arith.PeanoNat Category.Lib Category.Theory.Category