[Agda] pattern matching order

[Andreas Abel]

On 03.04.2017 23:12, Martin Escardo wrote:
> 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.

;)

Got me!  That already exceeded what was left of my Latin training.

But I called upon the Great Database, and it delivered me from the state 
of ignorance.

--Andreas

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