The Coq mailing list

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

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
>>
>