Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] why does simpl fail?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] why does simpl fail?


Chronological Thread 
  • From: Théo Winterhalter <theo.winterhalter AT ens-cachan.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] why does simpl fail?
  • Date: Sat, 25 Apr 2020 13:03:24 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=theo.winterhalter AT ens-cachan.fr; spf=Pass smtp.mailfrom=theo.winterhalter AT ens-cachan.fr; spf=Pass smtp.helo=postmaster AT ariane2.ens-cachan.fr
  • Ironport-phdr: 9a23:NlMjWhRsyY/JD6e5y5gEXfxeRdpsv+yvbD5Q0YIujvd0So/mwa6yZBCN2/xhgRfzUJnB7Loc0qyK6v2mBDBLuM7JmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRW7oR/Ru8QZjoduN7o9wQbVr3VVfOhb2XlmLk+JkRbm4cew8p9j8yBOtP8k6sVNT6b0cbkmQLJBFDgpPHw768PttRnYUAuA/WAcXXkMkhpJGAfK8hf3VYrsvyTgt+p93C6aPdDqTb0xRD+v4btnRAPuhSwaMTMy7WPZhdFqjK9DoByuuxNxzIHJbo+bOvpwYKHSc9AdS2daQsZRTilBDp+8b4cTDecMO/tToYnnp1sJqBuzHReiBOP1zT9PnnD53aw60+I9EQ7YxgwgH8gBsHDIrNrrLqcZTOe4zLXIzTrdaPNawzn86InOchA9v/6MR7JwftDVyUkzCQzFlE6dppLjPzOOz+gCr3KU4PZgVe21jW4rsQ9xoiK2y8oql4LHhZoVx0jZ+Sh3w4s5P8O0RUBmbdK+DZddtSCXO5F2T84tW21kpTo2x7kctZO1YCQG0okryhHDZ/CdcoWF7BTuX/uLLzhinnJqYre/ig6y8Ue+zu38UdG530xQripEiNbMsG4C2wLJ5seZTPt95V6t1iqV2A/P6uFLO0Y0mbDVK5472rIwl5wTvlrfHiLuhUn7gqybel869uWm9ujreKjqq52dOoNuigzzPbwimsmlDuQ5NggOUXKb+eO51LD74U35QKtFjvosnqjXsZDaI9gbqbCjAw9VyIkj7wq/ACm80NkDg3YHKklFdAubgIfzJ17OIOr3DfGlj1Siijdn3+rGMaH5ApXRMnjDl6/scqp6605F0QY80dRf549PBbwaO/LyWkrxtMTCARMjMgy0xfznCNRn2Y8EV2KPGPzRDKSHuliRo+krPuOkZYkPuT+7JeJ2yeTpiCoFmd4aSpao24cacnCxGuhrOQ3NfXrhhZEeEGEWsxA+Rej2hUeqXDhIIn27VKI14Hc1EtT1Xs/4WomxjenZj2+AFZpMazUeUw3eITLTb4yBHsw0RmeSL8tmyGdWXKKgQoksj1ejshS/wLNsLuPSvCMC58u6hYpFotbLnBR3zgRaSsGU0mWDVWZxxz5aSjktmat2qkx0zBGNy/oh2qAKJZlo//pMFzwCG9vE1eUjVoL/XBmEdd6CSF+gBNu8U2k8

Even a fixpoint with no recursive call, has a recursive argument.
This argument is then used a syntactic guard to block reduction, unless it is
a constructor.

If you print your term you will see that the recursive argument is probably
not ders but the first argument that is of an inductive type.
You can fix this as Pierre-Léo suggest by using Definition instead of
Fixpoint, or by explicitly saying that ders is the recursive argument by
adding {struct ders} before the :=.

> Le 25 avr. 2020 à 12:58, BEGAY Pierre-leo
> <pbegay AT ens-cachan.fr>
> a écrit :
>
> Hello,
>
> I've had the same issue recently, the problem was that I used a Fixpoint
> where a Definition was sufficient. I guess simpl does not perform "terminal
> computations" on Fixpoints, but only tries to simplify the recursive call,
> maybe someone else can elaborate on that.
>
> As far as I can tell, you do not need to use a Fixpoint either, so that may
> be the source of your problem.
>
> Cheers,
> Pierre-Léo Bégay
>
>
> Jeremy Dawson
> <Jeremy.Dawson AT anu.edu.au>
> a écrit :
>
>> Hi,
>>
>> I have a definition
>>
>> Fixpoint dersrec_hd X rules prems c cs
>> (ders : @dersrec X rules prems (c :: cs)) :=
>> match ders with
>> | dlCons d ds => d
>> end.
>>
>> but when I try do prove the following, I would expect the simpl step to
>> simplify it to d = d
>>
>> Lemma dersrec_hd_eq X rs ps c cs
>> (d : @derrec X rs ps c) (ds : @dersrec X rs ps cs) :
>> dersrec_hd (dlCons d ds) = d.
>> Proof. simpl. (* does nothing *)
>>
>> What could be the reason for failure here?
>>
>> Thanks
>>
>> Jeremy Dawson
>
>
>




Archive powered by MHonArc 2.6.18.

Top of Page