Proof arguments in Coq

Question

I'm trying to define a function on a weakly-specified type in Coq. Specifically, I have a type that is defined inductively by a set of recursive constructors, and I want to define a function that is only defined when the argument has been constructed using a subset of these.

To be more concrete, I have the following type definition:

Inductive Example : Set :=
  | Example_cons0 : nat -> Example
  | Example_cons1 : Example -> Example
  .

Now, I have a function that only applies to the ground case. (The following definition will not work obviously, but is meant to suggest my intent.)

Definition example (x:Example) : nat :=
  match x with
    | Example_cons0 n => n
  end.

Ideally, I'd like to communicate that my argument, x, has been constructed using a subset of the general type constructors, in this case, Example_cons0. I thought that I could do this by defining a predicate that states this fact and passing a proof of the predicate as an argument. For example:

Definition example_pred (x:Example) : Prop :=
  match x with
    | Example_cons0 _ => True
    | _ => False
  end.

And then (following the recommendation given by Robin Green) something like,

Definition example2 (x:Example) : example_pred x -> nat :=
  (use proof to define example2?)

Unfortunately, I'm not sure how I would go about doing any of this. I'm not even sure that this is the correct way to define restricted functions on weakly-specified types.

Any guidance, hints, or suggestions would be strongly appreciated! - Lee

Update:

Following recommendations by jozefg, the example function can be defined as:

Definition example (x:Example) : example_pred x -> nat :=
  match x with
    | Example_cons0 n => fun _ => n
    | _               => fun proof => match proof with end 
  end.

See his comments for details. This function can be evaluated using the following syntax, which also demonstrates how proof terms are represented in Coq:

Coq < Eval compute in Example.example (Example.Example_cons0 0) (I : Example.example_pred (Example.Example_cons0 0)).
    = 0
    : nat

Answer 1

Here's how I'd write this as a simplified example

Consider a simple data type

Inductive Foo :=
| Bar : nat -> Foo
| Baz.

And now we define a helpful function

Definition bar f :=
  match f with
    | Bar _ => True
    | Baz   => False
  end.

And finally what you want to write:

Definition example f :=
  match f return bar f -> nat with
    | Bar n => fun _ => n
    | Baz   => fun p => match p with end
  end.

This has the type forall f : Foo, bar f -> nat. This works by making sure that in the case that example was not supplied a Bar, that the user must supply a proof of false (impossible).

This can be called like this

example (Bar n) I

But the problem is, you may have to manually prove some term is constructed by Bar, otherwise how is Coq supposed to know?

Answer 2

Yes, you are on the right lines. You want:

Definition example2 (x:Example) (example_pred x) : nat :=

and how to proceed further would depend on what you wanted to prove.

You might find it helpful to make a definition by proving with tactics, using the Curry-Howard correspondence:

Definition example2 (x:Example) (example_pred x) : nat.
Proof.
  some proof
Defined.

Also, I'd like to point out that the sig and sigT types are often used to combine "weakly-specified types" with predicates to constrain them.