The Coq mailing list

[Andreas Schropp <schropp AT in.tum.de>]

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