coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
>
>
>
- [Coq-Club] why does simpl fail?, Jeremy Dawson, 04/25/2020
- Re: [Coq-Club] why does simpl fail?, BEGAY Pierre-leo, 04/25/2020
- Re: [Coq-Club] why does simpl fail?, Théo Winterhalter, 04/25/2020
- Re: [Coq-Club] why does simpl fail?, Jeremy Dawson, 04/25/2020
- Re: [Coq-Club] why does simpl fail?, Théo Winterhalter, 04/25/2020
- Re: [Coq-Club] why does simpl fail?, BEGAY Pierre-leo, 04/25/2020
Archive powered by MHonArc 2.6.18.