prove that all associations of elements in a semigroup are equal

semigroup_assoc.v

Require Import Coq.micromega.Lia.
Require Import Coq.Arith.Arith.
Require Import Coq.Lists.List.
Import ListNotations.
Local Open Scope list_scope.

Inductive tree : nat -> Set :=
| leaf : tree 1
| node {x y} : tree x -> tree y -> tree (x + y).

Fixpoint right_tree (n : nat) : tree (S n) :=
  match n with
  | O => leaf
  | S n => node leaf (right_tree n)
  end.

Ltac reify' op v :=
  lazymatch v with
  | op ?x ?y
    => let x := reify' op x in
       let y := reify' op y in
       lazymatch constr:((x, y)) with
       | ((?xt, ?xargs), (?yt, ?yargs))
         => constr:((node xt yt, xargs ++ yargs))
       end
  | ?x => constr:((leaf, [x]))
  end.

Ltac reify evalf op v :=
  let v := reify' op v in
  lazymatch v with
  | (?t, ?args) => let args := (eval cbn ["++"] in args) in
                   constr:(evalf args t)
  end.

Section with_semigroup.
  Context (G : Type)
          (op : G -> G -> G).
  Infix "*" := op.
  Context (assoc : forall a b c, a * (b * c) = (a * b) * c).

  Fixpoint eval {n} (args : list G) (t : tree n) : option G
    := match t with
       | leaf => match args with
                 | [x] => Some x
                 | _ => None
                 end
       | @node x y tx ty
         => match eval (firstn x args) tx, eval (skipn x args) ty with
            | Some a, Some b => Some (op a b)
            | _, _ => None
            end
       end.

  Lemma no_zero_tree : tree 0 -> False.
  Proof.
    remember 0 as n eqn:H.
    induction 1; try lia.
  Qed.

  Lemma eval_right_tree_split arg args x y
    : length args = x + S y
      -> eval (arg :: args) (right_tree (length args))
         = match eval (arg :: firstn x args) (right_tree x),
                 eval (skipn x args) (right_tree y)
           with
           | Some a, Some b => Some (a * b)
           | _, _ => None
           end.
  Proof using assoc.
    revert arg args y.
    induction x as [|x IH]; cbn.
    all: repeat first [ rewrite assoc
                      | progress intros
                      | progress cbn ["+" eval length right_tree firstn skipn] in *
                      | lia
                      | reflexivity
                      | match goal with
                        | [ |- context[match ?x with _ => _ end] ]
                          => is_var x; destruct x
                        | [ H : length ?x = S _ |- _ ] => is_var x; destruct x
                        | [ H : S _ = S _ |- _ ] => inversion H; clear H
                        end
                      | erewrite IH by eassumption
                      | match goal with
                        | [ |- context[match ?x with _ => _ end] ]
                          => lazymatch x with
                             | context[match _ with _ => _ end] => fail
                             | _ => destruct x eqn:?
                             end
                        end ].
  Qed.

  Theorem eq_right n
    : forall (args : list G)
             (t : tree n)
             (Hn : length args = n),
      eval args t = eval args (right_tree (pred n)).
  Proof using assoc.
    induction (lt_wf n) as [n _ IH]; intros.
    destruct t.
    { cbn.
      repeat match goal with |- context[match ?x with _ => _ end] => is_var x; destruct x end.
      all: reflexivity. }
    { specialize (fun y => IH (S y)).
      cbn.
      match goal with H : length _ = ?x + ?y |- _ => destruct x, y end.
      all: repeat first [ progress cbn [length "+" firstn skipn Init.Nat.pred] in *
                        | lia
                        | now exfalso; eapply no_zero_tree
                        | match goal with
                          | [ H : length ?x = 0 |- _ ] => is_var x; destruct x
                          | [ H : length ?x = S _ |- _ ] => is_var x; destruct x
                          | [ H : S _ = S _ |- _ ] => inversion H; clear H
                          end ].
      erewrite eval_right_tree_split by eassumption.
      (do 2 ((unshelve erewrite <- IH by now cbn [length]; rewrite ?firstn_length, ?skipn_length; try eassumption; lia); [ eassumption .. | ])).
      reflexivity. }
  Qed.

  Corollary all_eq n m
    : forall (args : list G)
             (t1 : tree n) (t2 : tree m)
             (Hn : length args = n)
             (Hm : length args = m),
      eval args t1 = eval args t2.
  Proof using assoc.
    intros; subst.
    etransitivity; [ | symmetry ]; eapply eq_right; reflexivity.
  Qed.

  (** ================================== *)
  (** Now we prove things about specific sizes *)

  Ltac reify_sides :=
    lazymatch goal with
    | [ |- ?x = ?y :> G ]
      => let x := reify uconstr:(eval) op x in
         let y := reify uconstr:(eval) op y in
         cut (x = y); [ cbn [eval firstn skipn "+"]; congruence | ]
    end.

  Lemma all_eq4
    : forall a b c d : G,
      exists v,
        a * (b * (c * d)) = v
        /\ a * ((b * c) * d) = v
        /\ (a * (b * c)) * d = v
        /\ ((a * b) * c) * d = v
        /\ (a * b) * (c * d) = v.
  Proof using assoc.
    intros; repeat esplit; reify_sides; apply all_eq; reflexivity.
  Qed.

  (** ============================ *)
  (** Enumeration of sizes *)

  Fixpoint enum_trees (n : nat) : list { m : nat & tree m }
    := match n with
       | 0 => []
       | S n
         => let ts := enum_trees n in
            (existT tree _ leaf)
              :: (List.flat_map
                    (fun '(existT _ x t1)
                     => List.map
                          (fun '(existT _ y t2)
                           => existT tree _ (node t1 t2))
                          ts)
                    ts)
       end.

  Import EqNotations.

  Definition enum_trees_of_size (n : nat) : list (tree n)
    := List.flat_map
         (fun '(existT _ x t)
          => match Nat.eq_dec x n with
             | left pf => [rew pf in t]
             | right _ => []
             end)
         (enum_trees n).

  Definition enum_assocs_of_args (args : list G)
    := List.flat_map
         (fun v => match v with Some v => [v] | None => [] end)
         (List.map (eval args) (enum_trees_of_size (length args))).

  Compute fun a b c d => enum_assocs_of_args [a; b; c; d].
  (*      = fun a b c d : G =>
       [a * (b * (c * d)); a * (b * c * d); a * b * (c * d);
       a * (b * c) * d; a * b * c * d]
     : G -> G -> G -> G -> list G
*)
End with_semigroup.