The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2014-07-29 16:40 GMT+02:00 coqcdp <coqcdpnxj AT 163.com>:

Hi,

      Recently I want to prove associativity law in algebra ,I have proved that with 3 parameters,but I don't know how to prove that with arbitrary n parameters. for example I can prove  (a+b)+c = a +(b+c)  with coq , but  I don't know how to prove  or  formalize (a1+a2)+...+an=a1+(a2+a3)+...+an=...=a1+a2+...+(an-1+an). I hope you can give me some suggestions. Thank you .

As far as I know, once you have proved "(a+b)+c = a +(b+c)", then all your "(a₁+a₂)+...+aₙ=a₁+(a₂+a₃)+...+aₙ=...=a₁+a₂+...+(aₙ-₁+an)" hold.
What you can do is reification of formulæ. For instance, you can define:

Inductive skeleton : nat -> Type :=
| Slot : skeleton 1
| Compose : forall m n, skeleton m -> skeleton n -> skeleton (m+n).

Inductive vector (A:Type) : nat -> Type :=
| Nil : vector O
| Cons : forall n, A -> vector A n -> vector A (S n).

Definition head (A : Type) (n:nat) (v : vector A (S n)) : A :=
  match v in vector _ n return match n with S _ => A | _ => unit end with
  | Cons _ a _ => a
  | Nil => tt
  end.

Definition tail (A : Type) (n : nat) (v : vector A (S n)) : vector A n :=
  match v in vector _ n return match n with S m => vector A m | _ => unit end with
  | Cons m _ v => v
  | Nil => tt
  end.

Definition split (A : Type) (n : nat) : forall m, vector A (m+n) -> (vector A m * vector A n) :=
  fix split m :=
  match m as m return vector A (m+n) -> (vector A m * vector A n) with
  | O => fun v => (Nil A, v)
  | S m => fun v => let (x, y) := split m (tail A m v) in (Cons A (head A m v) x, y)
  end.

Definition eval (A : Type) (binop : A -> A -> A) : forall n (s : skeleton n) (l : vector A n), A :=
  fix eval n s :=
  match s in skeleton m return vector m -> A with
  | Slot => fun v => head A O v
  | Compose m n sm sn => fun v => let (x, y) := split A n m v in binop (eval m sm x) (eval n sn y)
  end.

Lemma full_assoc  (A:Type) (binop : A -> A -> A) (assoc : forall x y z, binop (binop x y) z = binop x (binop y z)) :
  forall n (s₁ s₂ : skeleton n) (v : vector A n), eval A binop n s₁ v = eval A binop n s₂ v.
Proof.
(*TODO*)
Qed.

==========================
I warn you, I did not try it, so there are some typos.
It highly requires understanding of dependant types, and may not be trivial for a beginner.
For the proof, one way to do so is to "normalize" skeletons: you show that full_assoc stands for s₁=<Compose Slot (Compose Slot (Compose Slot …))>

In practice a+(b+c)=(a+b)+c is largely sufficient, as you can use "repeat rewrite <associativity proof> in …" in any hypothesis to "normalize" it, without to care on arbitrary n.


 

    

        Yours Sincerely ,

                                   D.P.Chen

--
.../Sedrikov\...