[Agda] pattern matching order

[Andreas Abel]

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/