[Agda] what is happening here?

[Ulf Norell]

Hi Thorsten,

The constraints you get are

  ?l + (?m + ?n) = l + (m + n) : ℕ
  ?l + ?m + ?n = l + m + n : ℕ

You are right that ?l := l, ?m := m, ?n := n is the only solution, but this
requires some non-trivial reasoning. For instance, the first constraint
can be satisfied by

  ?l := 0, ?m := l, ?n := (m + n)

so Agda would need to look at both constraints together to rule out this
solution.

/ Ulf

On Sun, Mar 8, 2020 at 7:26 PM Thorsten Altenkirch <
Thorsten.Altenkirch at nottingham.ac.uk> wrote:

> I define
>
>
>
> record isMonoid {A : Set}(e : A)(_•_ : A → A → A) : Prp where
>
>   field
>
>     lneutr : {x : A} → e • x ≡ x
>
>     rneutr : {x : A} → x • e ≡ x
>
>     assoc : {x y z : A} → (x • y) • z ≡ x • (y • z)
>
>
>
> and I have shown all 3 properties, in particular:
>
>
>
> assoc+ : {l m n : ℕ} → (l + m) + n ≡ l + (m + n)
>
>
>
> but when I try
>
>
>
> isMonoid : isMonoid zero _+_
>
> +isMonoid = record {
>
>   lneutr = lneutr+ ;
>
>   rneutr = rneutr+ ;
>
>   assoc = assoc+ }
>
>
>
> I get some unsolved constraints, even though my proof and the goal are
> alpha-equivalent! Ok I can fix this by eta expanding:
>
>
>
>   assoc = λ {x}{y}{z} → assoc+ {x}{y}{z}
>
>
>
> But this shouldn’t be necessary.
>
>
>
>
>
>
>
> 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 contact the sender and delete the email and
> attachment.
>
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored
> where permitted by law.
>
>
>
>
> _______________________________________________
> Agda mailing list
> 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/20200308/d1c7b1a1/attachment.html>