The Coq mailing list

[Kirill Taran <kirill.t256 AT gmail.com>]

I also tried (not very hard) to invent "opposite" of previous definition:

Definition Wrap tag (m : Element tag) : Node :=
  match tag with
  | L => left m
  | R => right m
  end.

But that fails, too. (Coq expects m to be Element L instead of Element tag.)
I definetely should to glance at CPDT, but hadn't time for that yet.

Sincerely,
Kirill Taran

On Fri, Feb 14, 2014 at 3:35 AM, Kirill Taran <kirill.t256 AT gmail.com> wrote:

Hello again,

What about such piece of code?

Inductive  Tag := L | R.
Definition Element tag :=
  match tag with
  | L => nat
  | R => bool
  end.
Inductive Node :=
  | left  : Element L -> Node
  | right : Element R -> Node.

Definition Cast tag (n : Node) : Element tag :=
  match tag with
  | L => match n return Element L with left  e => e end
  | R => match n return Element R with right e => e end
  end.

Coq can't infer that there enough branches and complains on definition of Cast.

Pierre,

I didn't find how to launch code with absurd pattern (!), your example doesn't work for me.
Have I to enable any settings?

Sincerely,
Kirill Taran

On Fri, Feb 14, 2014 at 12:32 AM, Kirill Taran <kirill.t256 AT gmail.com> wrote:

Daniel,
Ow, I didn't try that; thanks.

Pierre,
Thanks for advices about return and !. By the way, I really noticed that the code I am working on now becomes pretty difficult in the sense that I have to do some manual work.

Maybe there are any libs like lenses for haskell? (For reducing boilerplate, when you need to extract something from the bottom of structure with different dependencies.)

Sincerely,
Kirill Taran

On Thu, Feb 13, 2014 at 11:11 PM, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

On 13/02/2014 19:54, Kirill Taran wrote:
> But Coq complains about definition of Matching: it says that pattern
> matching is non-exhaustive and there are can be branches L right and R
> left. But we never can construct such objects. Why Coq can't infer that?

Because this is undecidable in general. You have to write out return
clauses by hand when you start messing with dependent pattern-matching.

Or you can use Program to do the dirty job for you.

Program Definition Matching (n : Node) :=

  match n with
  | L left  => True
  | R right => True

  | _ => !
  end.

(Here '!' stands for the absurd case. Have a look at the generated term
to understand how it works.)

The more your inductives will be dependent, the more you will need to do
things by hand. I recommend the reading of CPDT to get a handful of neat
design patterns when programming with dependent types.

PMP