[Agda] two questions on type checker

[Sergei Meshveliani]

Dear Agda developers

I have two notes on a code of kind

----------------------------------------------------
lemma' y (x ∷ x' ∷ xs) _ i@(suc k , 1+k<|xx'xs|) =
begin
...
lookup' (x' ∷ xs) (k , k<|x'xs|)
≡⟨ lemma' y x'xs 0<|x'xs| (k , k<|x'xs|)
...
where
x'xs = x' ∷ xs
...
----------------------------------------------------

Agda 2.6.0-05e8112 reports

-----------------
Termination checking failed for the following functions:
lemma'
Problematic calls:
lemma' y (x'xs y x x' xs x₁ k 1+k<|xx'xs|)
(0<|x'xs| y x x' xs x₁ k 1+k<|xx'xs|)
(k , k<|x'xs| y x x' xs x₁ k 1+k<|xx'xs|)
...
------------------

First, the print-out of the lemma' call in the message differs greatly
from the source code. Blanks inserted into identifiers, `∷' skipped etc.

Second, with expanding x'xs to (x' ∷ xs) in the recursive call, Agda
sees termination.
Many users will not guess to do this expansion and will spend effort
trying to provide a wise termination proof.
If it is problematic to fix the feature, may be, Agda could issue some
hints after the message about termination - ?

Regards,

------
Sergei

[Jason -Zhong Sheng- Hu]

I guess a rule of thumb is to provide a clear indication of the decreasing structure syntactically in order to please termination checker. There aren't many reasons why such check fails, so I personally don't find it's too bad. Though, I do wish I can specify what is the decreasing structure in some occasions.

Sincerely Yours,

Jason Hu
________________________________
From: Agda <agda-***@lists.chalmers.se> on behalf of Sergei Meshveliani <***@botik.ru>
Sent: September 24, 2018 8:50 AM
To: ***@lists.chalmers.se
Subject: [Agda] two questions on type checker

Dear Agda developers

I have two notes on a code of kind

----------------------------------------------------
lemma' y (x ∷ x' ∷ xs) _ i@(suc k , 1+k<|xx'xs|) =
begin
...
lookup' (x' ∷ xs) (k , k<|x'xs|)
≡⟚ lemma' y x'xs 0<|x'xs| (k , k<|x'xs|)
...
where
x'xs = x' ∷ xs
...
----------------------------------------------------

Agda 2.6.0-05e8112 reports

-----------------
Termination checking failed for the following functions:
lemma'
Problematic calls:
lemma' y (x'xs y x x' xs x₁ k 1+k<|xx'xs|)
(0<|x'xs| y x x' xs x₁ k 1+k<|xx'xs|)
(k , k<|x'xs| y x x' xs x₁ k 1+k<|xx'xs|)
...
------------------

First, the print-out of the lemma' call in the message differs greatly
from the source code. Blanks inserted into identifiers, `∷' skipped etc.

Second, with expanding x'xs to (x' ∷ xs) in the recursive call, Agda
sees termination.
Many users will not guess to do this expansion and will spend effort
trying to provide a wise termination proof.
If it is problematic to fix the feature, may be, Agda could issue some
hints after the message about termination - ?

Regards,

------
Sergei

_______________________________________________
Agda mailing list
***@lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda

[Guillaume Allais]

Note that you can use an @ pattern to bind x'xs like so:
lemma' y (x ∷ x'xs@(x' ∷ xs)) _

A let-binding (rather than a where) should also work

Post by Sergei Meshveliani
Dear Agda developers
I have two notes on a code of kind
----------------------------------------------------
begin
...
lookup' (x' ∷ xs) (k , k<|x'xs|)
≡⟚ lemma' y x'xs 0<|x'xs| (k , k<|x'xs|)
...
where
x'xs = x' ∷ xs
...
----------------------------------------------------
Agda 2.6.0-05e8112 reports
-----------------
lemma'
lemma' y (x'xs y x x' xs x₁ k 1+k<|xx'xs|)
(0<|x'xs| y x x' xs x₁ k 1+k<|xx'xs|)
(k , k<|x'xs| y x x' xs x₁ k 1+k<|xx'xs|)
...
------------------
First, the print-out of the lemma' call in the message differs greatly
from the source code. Blanks inserted into identifiers, `∷' skipped etc.
Second, with expanding x'xs to (x' ∷ xs) in the recursive call, Agda
sees termination.
Many users will not guess to do this expansion and will spend effort
trying to provide a wise termination proof.
If it is problematic to fix the feature, may be, Agda could issue some
hints after the message about termination - ?
Regards,
------
Sergei
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda