[Agda] pattern matching order

[Andreas Abel]

   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.

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

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