The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

The normal method in Coq is indeed to define a setoid equality on lists.

An alternative method of defining quotient has been played with in the recent month within the framework of homotopy type theory: higher inductive type (in which case it would work nicely with Coq's native equality rather than a setoid equality). It is not available in Coq yet (though I understand there is a prototype out there). But it would look like that:

Inductive fbag (A:Type) :=
| empty : fbag A
| insert : A -> fbag A -> fbag A
| permutation : forall (a a2:A) (b:fbag A), insert a (insert a2 b) = insert a2 (insert a b)
.

(typically in homotopy type theory, one would prefer something slightly different so that   forall (A:Type) (a b:fbag A) (r s:a=b), r=s   is provable, but that's another story)

Some more thoughts and links there: http://homotopytypetheory.org/2011/04/24/higher-inductive-types-a-tour-of-the-menagerie/

On 5 May 2013 11:48, Andreas Schropp <schropp AT in.tum.de> wrote:

Hi all,

is there an established methodology to introduce
inductive data types modulo equations in Coq?
The algebraic specification community calls this the
initial algebra approach towards abstract data types.

I am talking about examples like introducing the type
of finite bags as a copy of the list datatype modulo
cons-permutation. In fantasy Coq-ish notation:

      DatatypeModulo fbag (A : Type) :=
      |  empty : fbag A
      |  insert : A -> fbag A -> fbag A
      where
   insert a (insert a2 b) = insert a2 (insert a b)


It seems to me such a construction can be realized in Coq
by defining a setoid over the free data type (i.e. a copy
of the list data type) with the equivalence relation inductively
defined by the clauses

      b ~ b
      b ~ b2  ->  b2 ~ b
      b ~ b2  ->  b2 ~ b3  ->  b ~ b3
      b ~ b2  ->  insert a (insert a2 b) ~ insert a2 (insert a b2)

Setoid rewriting can then be used to animate this identification of
constructor terms.
Defining functions by recursion on data types modulo equations
works by recursively defining the function on the free data type
as usual and then establishing invariance under (~),
i.e. b ~ b2 -> f b = f b2, by induction on the derivation of (~).


I am collaborating on a paper about a package for data types modulo
equations in Isabelle/HOL, so the nature of this request is mainly
gathering references to related work in Coq.


Cheers,
  Andy