cardinal_3.v

Require Import FMaps FMapFacts ZArith.

Module Import Test := Make (Z_as_OT).
Module Import P := Properties Test.

Module First_proof.

Lemma remove_In_Add : forall {A} k e (m : t A),
  MapsTo k e m ->
  Add k e (remove k m) m.
Proof.
  intros. unfold Add.
  intros.
  rewrite F.add_o.
  destruct (F.eq_dec k y).
  - subst. apply find_1; assumption.
  - rewrite F.remove_neq_o by assumption. reflexivity.
Qed.

Lemma cardinal_3 :
  forall {A} (m m' : t A) x e, In x m -> Add x e m m' -> cardinal m = cardinal m'.
Proof.
  intros.
  assert (Equal (remove x m) (remove x m')).
  { intros y. rewrite 2!F.remove_o.
    destruct (F.eq_dec x y). reflexivity.
    unfold Add in H0. rewrite H0.
    rewrite F.add_neq_o by assumption. reflexivity.
  }
  apply Equal_cardinal in H1.
  rewrite 2!cardinal_fold.
  destruct H as (e' & H).
  rewrite fold_Add with (eqA:=eq) (m1:=remove x m) (m2:=m) (k:=x) (e:=e');
    try now (compute; auto).
  rewrite fold_Add with (eqA:=eq) (m1:=remove x m') (m2:=m') (k:=x) (e:=e);
    try now (compute; auto).
  rewrite <- 2!cardinal_fold. congruence.
  apply remove_1. reflexivity.
  apply remove_In_Add.
  apply find_2. unfold Add in H0. rewrite H0.
  rewrite F.add_eq_o; reflexivity.
  apply remove_1. reflexivity.
  apply remove_In_Add. assumption.
Qed.

End First_proof.

Module Second_proof.

Definition Same_keys {A} (m1 m2 : t A) := forall k, In k m1 <-> In k m2.

Global Instance Same_keys_equiv {A} : Equivalence (Same_keys (A:=A)).
Proof.
  split.
  - intros m. intros k. reflexivity.
  - intros m1 m2. intros. intros k. rewrite (H k). reflexivity.
  - intros m1 m2 m3 H1 H2. intros k.
    rewrite (H1 k). apply H2.
Qed.

Lemma InA_eqk_eqke : forall elt k e l,
  InA (eq_key (elt:=elt)) (k, e) l ->
  exists e', InA (eq_key_elt (elt:=elt)) (k, e') l.
Proof.
  intros.
  apply InA_alt in H. destruct H as ((k', e') & H0 & H1).
  unfold eq_key, Raw.PX.eqk in H0. simpl in H0. subst.
  exists e'. apply InA_alt. eexists (_, _). split.
  split; reflexivity. assumption.
Qed.

Global Instance elements_respectful : forall {A},
  Proper (Same_keys ==> eqlistA (eq_key (elt:=A))) (elements (elt:=A)).
Proof.
  intros A m1 m2 m_equiv.
  eapply SortA_equivlistA_eqlistA with (ltA:=lt_key (elt:=A));
    try typeclasses eauto; try apply elements_3.
  intros (k, v).
  split; intros.
  - apply InA_eqk_eqke in H.
    apply F.elements_in_iff in H. apply m_equiv in H.
    apply -> F.elements_in_iff in H. destruct H as (e & H).
    eapply InA_eqke_eqk; try eassumption. reflexivity.
  - apply InA_eqk_eqke in H.
    apply F.elements_in_iff in H. apply m_equiv in H.
    apply -> F.elements_in_iff in H. destruct H as (e & H).
    eapply InA_eqke_eqk; try eassumption. reflexivity.
Qed.

Global Instance length_eqlistA : forall {A} (eqA : A -> A -> Prop),
  Proper (eqlistA eqA ==> eq) (length (A:=A)).
Proof.
  intros A eqA l1 l2 l_eq.
  eapply eqlistA_length; eassumption.
Qed.

Lemma Same_keys_cardinal : forall elt (m m' : t elt),
  Same_keys m m' -> cardinal m = cardinal m'.
Proof.
  intros.
  rewrite 2!Test.cardinal_1.
  rewrite H. reflexivity.
Qed.

Lemma cardinal_3 :
  forall {A} (m m' : t A) x e, In x m -> Add x e m m' ->
  cardinal m = cardinal m'.
Proof.
  intros. apply Same_keys_cardinal.
  unfold Same_keys.
  intros.
  rewrite F.in_find_iff with (m := m').
  rewrite H0.
  rewrite F.add_o.
  destruct (F.eq_dec x k).
  - subst. split; intros; [discriminate|assumption].
  - rewrite <- F.in_find_iff. reflexivity.
Qed.

End Second_proof.