The Coq mailing list

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

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