The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Dear Coq-Club,

Is there any way to tell "Program" not to mess with certain matches?

Whenever a definition is performed using "Program", all the matches in
this definition will end up being dependent matches that introduce an
additional equation within the match arms. That's often very useful, but
sometimes totally unnecessary - and combined with "destruct" not working
well on dependent matches, it can really get into the way.

I attached a (contrived, simple) example demonstrating this: In the
second definition, there's no reason for the match to become dependent.
However, there are some proofs that I have to fill out, so I'd still
like to use "Program". Currently, what I have to do is
* either put the match into a non-Program definition, and write
  Program definitions for the arms (or the context) insofar as
  there are proof terms that have to be constructed there. This
  results in fairly pointless splitting of definitions, and
  it introduces additional delta-steps that some tactics stumble
  over.
* or use "refine". This results in a rather weird-looking definition,
  and if what I define is a *type* involving "forall", refine
  doesn't even work: "refine (forall (t:T), _)" says this is not
  supported. This came up for me when I was defining a complicated
  proposition.

So, I wonder - is there something I can do with the match, e.g. some
kind of marker I could apply somehow, that tells "Program" not to mess
with it? That would be very useful.

Kind regards,
Ralf
Program Definition proj_Some (o: option nat) (H: o <> None): nat :=
  match o with
  | None => _
  | Some n => n
  end.
Next Obligation.
  intros. subst. now contradiction H.
Qed.

Program Definition zero_or_Some (n: nat) (o: option nat) (H: o = Some n): nat :=
  match n with
  | O => 42
  | S n => proj_Some o _
  end.
Next Obligation.
  intros. destruct o; discriminate.
Qed.

Print zero_or_Some.