Folding a commutative idempotent function over a list respects extensional equality

list_ext.v

From Stdlib Require Import List Relations Classes.RelationClasses Classes.Morphisms.

Definition list_ext A : relation (list A) := fun l l' => forall x, In x l <-> In x l'.

Class Associative {A : Type} (op : A -> A -> A) :=
  assoc : forall x y z, op x (op y z) = op (op x y) z.

Class Commutative {A : Type} {B : Type} (op : A -> A -> B) :=
  comm : forall x y, op x y = op y x.

Class Idempotent {A : Type} (op : A -> A -> A) :=
  idem : forall x, op x x = x.

Lemma comm_idem_eq {A : Type} (P : Type)
  (base : P)
  (into : A -> P)
  (rec : P -> P -> P)
  `{! Associative rec}
  `{! Commutative rec} 
  `{! Idempotent rec} :
  Proper (list_ext A ==> eq) (fold_right (fun a => (rec (into a))) base).
Proof.
  assert (swap : forall a b x : P, rec a (rec b x) = rec b (rec a x)).
  { intros a' b' x'; rewrite assoc, (@comm _ _ rec _ a'), <- assoc; auto. }

  assert (fold_incl : forall l l', (forall x, In x l -> In x l') ->
    rec (fold_right (fun a => rec (into a)) base l)
        (fold_right (fun a => rec (into a)) base l') =
    fold_right (fun a => rec (into a)) base l').
  { induction l as [|a l IH]; cbn; intros l' Hsub.
    - clear Hsub; induction l' as [|? l']; cbn;
      [apply idem | rewrite swap; f_equal; auto].
    - rewrite <- assoc, (IH _ (fun x H => Hsub x (or_intror H))).
      assert (Hin : In a l') by auto.
      clear Hsub IH; induction l' as [|? l' IH]; [easy | destruct Hin as [-> | ?]]; cbn;
      [rewrite assoc, idem | rewrite swap; f_equal]; auto. }

  intros l l' E;
  pose proof (fold_incl l l' (fun x H => proj1 (E x) H)) as Hlr;
  pose proof (fold_incl l' l (fun x H => proj2 (E x) H)) as Hrl;
  rewrite (@comm _ _ rec _) in Hrl; congruence.
Qed.