[Agda] It is hard to understand the agda error message

[James Wood]

Welcome to the mailing list!

My tactic, to a first approximation, when proving in Agda, is to avoid error messages, and not really read them when they come up. This seems to be the intended way of working.

In this case, the solution avoiding errors would be to get to the point -≤-iff-< (≤-trans ? (-≤-iff'-< n<p)) and look at the type required for the hole compared to -≤-iff'-< m<n. The goal has type suc m ≤ suc n, and the expression has type suc m ≤ n. At this point, you either prove/find a new lemma to get from what you have to what you need, or do what you did and start again from the top. In the latter case, you hopefully have a bit more intuition about the problem, allowing you to plan more effectively. This is no different from writing a paper proof.

For completeness of this reply, the error is saying that the red highlighted bit was meant to have the type m ≤ X for fixed m and unknown X. But -≤-iff'-< applied to an argument synthesises a type suc Y ≤ Z, for unknowns Y and Z. In general, there is no open term Y such that m = suc Y (m could be zero), so unification fails and you get this error.

Regards,

James

On 08/09/2019 01:32, mo jia wrote:

Hi:

I am following the https://plfa.github.io/ In this exercise.

<-trans'' : ∀ {m n p : ℕ}
  → m < n
  → n < p
    -----
  → m < p
<-trans''  m<n n<p =  -≤-iff-< (≤-trans (s≤s (-≤-iff'-< (m<n))) (-≤-iff'-< n<p))

I got the error

suc _m_357 != m of type ℕ
when checking that the inferred type of an application
  suc _m_357 ≤ _n_358
matches the expected type
  m ≤ _n_356

[agda_error.png]
The error is is hard for me to figure out the real wrong place.

At the end. I find the right way:

<-trans'  m<n n<p =  -≤-iff''-< (-≤-iff-< (≤-trans (s≤s (-≤-iff'-< (m<n))) (-≤-iff'-< n<p)))

So the right answer contain my first try
`(-≤-iff-< (≤-trans (s≤s (-≤-iff'-< (m<n))) (-≤-iff'-< n<p))`
When I try to fix the problem. I always want to change `s≤s (-≤-iff'-< (m<n))`
But it don't work.

So my question is  how to understand the error message? Or is there some learning path before following the plfa book? (I suck almost 1 hour to find out the right way which need the -≤-iff''-< helper)


-------------  The help functions ----------------
-≤-iff'-< : ∀ {m n : ℕ}
  → m < n
    -------------
  → suc m ≤ n
-≤-iff'-< {zero} {suc n} s<n = s≤s z≤n -- 0 < suc n whcich suc 0 <= suc n
-≤-iff'-< {suc m} {n} (s<s m<n) = s≤s (-≤-iff'-< m<n)

-≤-iff''-< : ∀ {m n : ℕ}
  → suc m < n
    -------------
  →  m < n
-≤-iff''-< {zero} {suc n} m<n = z<s -- 0 < suc n whcich suc 0 <= suc n
-≤-iff''-< {suc m} {n} (s<s m<n) = s<s (-≤-iff''-< m<n)
-------------  The help functions ----------------
















_______________________________________________
Agda mailing list
Agda at lists.chalmers.se<mailto:Agda at lists.chalmers.se>
https://lists.chalmers.se/mailman/listinfo/agda


​
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190908/d96d4322/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: agda_error.png
Type: image/png
Size: 28603 bytes
Desc: agda_error.png
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190908/d96d4322/attachment.png>