The Coq mailing list

["Michiel Helvensteijn" <mhelvens AT gmail.com>]

Hello all,

I've created (I think) an inductive type with an 'open-ended' / 'mixed'
content:

Inductive Delta : Type :=
  |  primitive   {T: Type} (_:T) : Delta
  |  composition    (_ _: Delta) : Delta.

This basically creates an abstract syntax tree, on top of which I would later
create a quotient algebra (using a setoid) and add axioms such as
associativity. I could then, for example, instantiate it with natural numbers
and multiplication.

I would want to convert 'mult' to operate on 'Delta's instead of natural
numbers. To cover this need in the general case, I'm trying to create a
function which takes an operator of type 'T -> U' and returns a corresponding
operator of type 'Delta -> option U':

Definition delta_op {T U: Type} (op: T -> U) (d: Delta) : option U.

The 'option' should cover the case that something other than a 'T'-primitive
is passed to the new operator. 'U' can again be a function type, so I can
later call the 'delta_op' recursively to cover operators of any arity.
Converting the end-value to a 'Delta' afterwards is then done with a simple
application of 'primitive'.

But I can't seem to find a way to define this function. This is my latest
attempt:

Definition delta_op {T U: Type} (op: T -> U) (d: Delta) : option U.
  elim d; [|intros; exact None ..].
  intros T0 t.
  match T0 with
  | T => exact (Some (op t))
  | _ => exact None
  end.
Defined.

Upon inspecting the result, it seems 'T0' is never matched with 'T' and 'op'
is never invoked. I guess that I'm making a wrong assumption somewhere. Could
someone explain, and perhaps help me with a correct approach?

Thanks!