[Agda] pattern matching order

[Martin Escardo]

On 03/04/17 21:34, Andreas Abel wrote:
>   I have surely seen the affliction of my people which are in Egypt, and
> have heard their cry by reason of their taskmasters; for I know their
> sorrows.

Absit iniuria.

Abundans cautela non nocet.

Martin

> 
> On 03.04.2017 21:12, Martin Escardo wrote:
>>
>>
>> On 03/04/17 17:21, Thorsten Altenkirch wrote:
>>> Thank you, Andreas.
>>>
>>> Wouldn’t it be possible to have a flag to say wether one wants the old
>>> behaviour or the new one?
>>
>> In any case, please, please try to not break code: some of us have spent
>> countless hours, days, months and years producing proofs, some of which
>> haven't been written down in research papers yet. If you have to break
>> my proofs because they are wrong, then so be it. But please think twice
>> if you are going to break them just to improve the language.
>>
>> Thanks!
>>
>> Best,
>> Martin
>>
>>
>>>
>>> Cheers,
>>> Thorsten
>>>
>>> On 03/04/2017, 15:21, "Agda on behalf of Andreas Abel"
>>> <agda-bounces at lists.chalmers.se on behalf of abela at chalmers.se> wrote:
>>>
>>>> Hi Thorsten,
>>>>
>>>> this is this issue #408
>>>>
>>>>   https://github.com/agda/agda/issues/408
>>>>
>>>> You can read there that I implemented a split strategy that would make
>>>> your code work, but did not activate it, since fixes the split strategy
>>>> to an extend where changing the order of clauses could not give you the
>>>> other behavior.  In particular, it was not backwards-compatible.
>>>> Whether we should turn on the new split strategy is still undecided
>>>> (since 2012).
>>>>
>>>> However, now you can use the --exact-split flag to let Agda alert you
>>>> when your clauses do not lead to definitional equalities.
>>>>
>>>> Cheers,
>>>> Andreas
>>>>
>>>> On 03.04.2017 15:08, Thorsten Altenkirch wrote:
>>>>> Hi,
>>>>>
>>>>> I tried to define the following function by pattern matching
>>>>>
>>>>> codeDouble : ∀{n : ℕ} → Bool × Fin n → Fin (double n)
>>>>> codeDouble {zero} (b , ())
>>>>> codeDouble {suc n} (false , zero) = zero
>>>>> codeDouble {suc n} (true , zero) = suc zero
>>>>> codeDouble {suc n} (b , suc x) = suc (suc (codeDouble (b , x)) )
>>>>>
>>>>> But to my confusion the term "codeDouble {suc n} (b , suc x) “ didn’t
>>>>> reduce. This can be fixed by changing the order
>>>>>
>>>>> codeDouble : ∀{n : ℕ} → Bool × Fin n → Fin (double n)
>>>>> codeDouble {zero} (b , ())
>>>>> codeDouble {suc n} (b , suc x) = suc (suc (codeDouble (b , x)) )
>>>>> codeDouble {suc n} (false , zero) = zero
>>>>> codeDouble {suc n} (true , zero) = suc zero
>>>>>
>>>>> I guess I can answer this myself: since I first match on the boolean
>>>>> agda decides also to do case analysis first on the boolean and then on
>>>>> the Fin which duplicates my last line and has the effect that the
>>>>> defining equality doesn’t hold definitionally (this is always a bit
>>>>> agda). In this case agda could have matched my definition by changing
>>>>> the order. Is this too much to ask for?
>>>>>
>>>>> Cheers,
>>>>> Thorsten
>>>>>
>>>>>
>>>>>
>>>>> This message and any attachment are intended solely for the addressee
>>>>> and may contain confidential information. If you have received this
>>>>> message in error, please send it back to me, and immediately delete
>>>>> it.
>>>>>
>>>>> Please do not use, copy or disclose the information contained in this
>>>>> message or in any attachment.  Any views or opinions expressed by the
>>>>> author of this email do not necessarily reflect the views of the
>>>>> University of Nottingham.
>>>>>
>>>>> This message has been checked for viruses but the contents of an
>>>>> attachment may still contain software viruses which could damage your
>>>>> computer system, you are advised to perform your own checks. Email
>>>>> communications with the University of Nottingham may be monitored as
>>>>> permitted by UK legislation.
>>>>>
>>>>>
>>>>>
>>>>> _______________________________________________
>>>>> Agda mailing list
>>>>> Agda at lists.chalmers.se
>>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>>>
>>>>
>>>>
>>>> -- 
>>>> Andreas Abel  <><      Du bist der geliebte Mensch.
>>>>
>>>> Department of Computer Science and Engineering
>>>> Chalmers and Gothenburg University, Sweden
>>>>
>>>> andreas.abel at gu.se
>>>> http://www.cse.chalmers.se/~abela/
>>>> _______________________________________________
>>>> Agda mailing list
>>>> Agda at lists.chalmers.se
>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>>>
>>>
>>>
>>>
>>> This message and any attachment are intended solely for the addressee
>>> and may contain confidential information. If you have received this
>>> message in error, please send it back to me, and immediately delete it.
>>>
>>> Please do not use, copy or disclose the information contained in this
>>> message or in any attachment.  Any views or opinions expressed by the
>>> author of this email do not necessarily reflect the views of the
>>> University of Nottingham.
>>>
>>> This message has been checked for viruses but the contents of an
>>> attachment may still contain software viruses which could damage your
>>> computer system, you are advised to perform your own checks. Email
>>> communications with the University of Nottingham may be monitored as
>>> permitted by UK legislation.
>>>
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>>
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe