Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] "Program" and match

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] "Program" and match


Chronological Thread 
  • From: Ralf Jung <jung AT mpi-sws.org>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] "Program" and match
  • Date: Mon, 15 Jun 2015 15:48:31 +0200

Hi Matthieu, Arnaud,

Thanks a lot, this is working great!

Kind regards,
Ralf

On 15.06.2015 14:48, Arnaud Spiwack wrote:
> Using `return _` deactivates `Program`'s specific pattern-matching
> compilation (I suppose it may have adverse side effects as well, but it
> generally works fine):
>
> 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 return _ with *
> | O => 42
> | S n => proj_Some o _
> end.
> Next Obligation.
> intros. destruct o; discriminate.
> Qed.
>
> Print zero_or_Some.
>
> Best,
>
> Arnaud Spiwack
>
> On 15 June 2015 at 11:24, Ralf Jung
> <jung AT mpi-sws.org>
> wrote:
>
>> 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
>>
>



Archive powered by MHonArc 2.6.18.

Top of Page