proposition: Lemma Equal_implies_eqv: forall [elt A: Type] [eqv: A -> A -> Prop] (eqv_rel: Equivalence eqv) (lift: key -> elt -> A) (lift_prop: forall k k' x, K.eq k k' -> eqv (lift k x) (lift k' x)) (f: A -> A -> A) (f_mor: forall x1 y1, eqv x1 y1 -> forall x2 y2, eqv x2 y2 -> eqv (f x1 x2) (f y1 y2)) (f_assoc: forall x y z : A, eqv (f x (f y z)) (f (f x y) z)) (f_commut: forall x y : A, eqv (f x y) (f y x)) (u: A) (u_unit: forall x, eqv (f u x) x) (g: key -> elt -> A -> A) (g_eqv: forall k x a, eqv (g k x a) (f (lift k x) a)) (tab1 tab2: t elt), tab1 == tab2 -> eqv (fold g tab1 u) (fold g tab2 u).
proof: Proof. intros. assert (ND1 := bindings_3w tab1). assert (ND2 := bindings_3w tab2). assert (Equivalence (eq_key (elt:=elt))). { unfold eq_key, Fst; split; hnf; intros. reflexivity. symmetry; auto. etransitivity; eassumption. } rewrite !fold_spec. rewrite <- !fold_left_rev_right. transitivity (fold_right (fun p => f (lift (fst p) (snd p))) u (rev (bindings tab1))); [ | transitivity (fold_right (fun p => f (lift (fst p) (snd p))) u (rev (bindings tab2)))]. clear u_unit; revert u; induction (rev (bindings tab1)) as [ | [a y] al]; simpl; intros; [reflexivity | ]; rewrite g_eqv; apply f_mor; [reflexivity | ]; apply IHal. 2: symmetry; clear u_unit; revert u; induction (rev (bindings tab2)) as [ | [a y] al]; simpl; intros; [reflexivity | ]; rewrite g_eqv; apply f_mor; [reflexivity | ]; apply IHal. clear g g_eqv u_unit. assert (forall x, InA (keyb_eq (elt:=elt)) x (rev (bindings tab1)) <-> InA (keyb_eq (elt:=elt)) x (rev (bindings tab2))) by (intros; rewrite !InA_rev; apply bindings_Equal; auto). apply NoDupA_rev in ND1, ND2; auto. change K.t with key in *. set (al := rev (bindings tab1)) in *; clearbody al. set (bl := rev (bindings tab2)) in *; clearbody bl. clear H tab1 tab2. revert bl ND2 H1; induction al as [ | [a x] al]; intros. - inversion ND2; clear ND2; subst. reflexivity. assert (Hx: InA (keyb_eq (elt:=elt)) x nil); [ | inversion Hx]. apply H1. left; reflexivity. - assert (exists a': key, K.eq a a' /\ List.In (a',x) bl). { clear - H1 ND2 ND1. inversion ND1; clear ND1; subst. specialize (H1 (a,x)). destruct H1 as [? _]. specialize (H (ltac:(left; reflexivity))). clear - H. induction bl as [ | [b y] bl]; simpl; inversion H; clear H; subst. + destruct H1; simpl in *. subst. exists b; split; auto. + destruct (IHbl H1) as [z [? ?]]. exists z; split; auto. } destruct H as [a' [? ?]]. inversion ND1; clear ND1; subst. simpl. specialize (IHal H6 (List.filter (fun p => negb (eqb (fst p) a')) bl)). etransitivity. apply f_mor. apply (lift_prop a a'); auto. apply IHal; try eassumption. apply NoDupA_filter; auto. + clear - H1 H5 H H0. rename H0 into EQ0. assert (PR: Proper (keyb_eq (elt:=elt) ==> eq) (fun p : K.t * elt => negb (eqb (fst p) a'))). { clear. hnf; intros. destruct H as [? _]. unfold key in *. f_equal. destruct (eqb (fst x) a') eqn:?H, (eqb (fst y) a') eqn:?H; try congruence. apply eqb_eq in H0. rewrite H in H0. apply eqb_eq in H0. congruence. apply eqb_eq in H1. rewrite <- H in H1. apply eqb_eq in H1. congruence. } intros [k y]. specialize (H1 (k,y)). revert bl H1; induction al; intros. split; intro. inversion H0. apply filter_InA in H0; auto. destruct H0. simpl in H2. rewrite <- H1 in H0. inversion H0; clear H0; subst. destruct H4; simpl in *. subst. rewrite H in H0. apply eqb_eq in H0. rewrite H0 in H2. inversion H2. inversion H4. split; intro. assert (InA (keyb_eq (elt:=elt)) (k, y) bl) by (rewrite <- H1; right; auto). apply filter_InA; auto. split; auto. simpl. destruct (eqb k a') eqn:?H; auto. apply eqb_eq in H3. contradiction H5. rewrite <- H in H3. clear - H0 H3. inversion H0; clear H0; subst. left. destruct H1. simpl in *. unfold key in *. rewrite H3 in H; auto. right. induction al as [| [j z] al]; inversion H1; clear H1; subst. left. hnf. simpl. rewrite <- H3. destruct H0; auto. right. apply IHal. auto. apply filter_InA in H0; auto. destruct H0. simpl in H2. rewrite <- H1 in H0. inversion H0; clear H0; subst. destruct H4. simpl in H0. unfold key in H. rewrite H in H0. apply eqb_eq in H0. rewrite H0 in H2. discriminate. auto. + clear IHal H H5 H6 al H1. induction bl. inversion H2. inversion ND2; clear ND2; subst. specialize (IHbl H4). destruct H2. * subst. simpl. apply f_mor. reflexivity. assert (K.eq a' a') by reflexivity. apply eqb_eq in H. rewrite H. simpl. clear IHbl H4 H. induction bl. simpl. reflexivity. assert (~ K.eq a' (fst a0) /\ ~ InA eq_key (a',x) bl). split; contradict H3. left; auto. right; auto. destruct H. simpl. unfold key in *. destruct (eqb (fst a0) a') eqn:?H. apply eqb_eq in H2. symmetry in H2. contradiction. simpl. apply f_mor. reflexivity. auto. * simpl. destruct (eqb (fst a0) a') eqn:?H. apply eqb_eq in H1. contradiction H3. clear - H1 H. { induction bl. inversion H. destruct H. subst. left; auto. right; auto. } unfold key in *. rewrite H1. simpl. etransitivity. 2: apply f_mor; [ | apply IHbl; auto]. instantiate (1:= (lift (fst a0) (snd a0))). rewrite f_assoc. etransitivity. apply f_mor. apply f_commut. reflexivity. rewrite <- f_assoc. reflexivity. reflexivity. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)