coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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!
- [Coq-Club] Matching on specific Type argument values?, Michiel Helvensteijn, 06/16/2013
- Re: [Coq-Club] Matching on specific Type argument values?, Jason Gross, 06/16/2013
- Re: [Coq-Club] Matching on specific Type argument values?, Michiel Helvensteijn, 06/16/2013
- Re: [Coq-Club] Matching on specific Type argument values?, Jason Gross, 06/16/2013
- Re: [Coq-Club] Matching on specific Type argument values?, Michiel Helvensteijn, 06/18/2013
- Re: [Coq-Club] Matching on specific Type argument values?, Jason Gross, 06/16/2013
- Re: [Coq-Club] Matching on specific Type argument values?, Michiel Helvensteijn, 06/16/2013
- Re: [Coq-Club] Matching on specific Type argument values?, Jason Gross, 06/16/2013
Archive powered by MHonArc 2.6.18.