Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Matching on specific Type argument values?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Matching on specific Type argument values?


Chronological Thread 
  • From: Jason Gross <jasongross9 AT gmail.com>
  • To: Michiel Helvensteijn <mhelvens AT gmail.com>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Matching on specific Type argument values?
  • Date: Sat, 15 Jun 2013 21:22:30 -0400

Type does not have decidable equality, and you cannot productively destruct/match on a thing of type Type.  Additionally, the match you use is in Ltac; it matches on a syntactic level, unlike the non-ltac match.  You will probably want to reify your types so that you can distinguish function types from other types.

Appologies if this is not enough information; I'm typing from my cellphone at the moment and thus being concise.

-Jason

On Jun 15, 2013 8:05 PM, "Michiel Helvensteijn" <mhelvens AT gmail.com> wrote:
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!



Archive powered by MHonArc 2.6.18.

Top of Page