[Agda] Absurd question

[Guillaume Brunerie]

One possible reason is the following: when you write

y : Y
y = \()

I think that Agda replaces it by something like:

y : Y
y = fresh where
  fresh : Y
  fresh ()

In other words, the primitive notion is the notion of definition by
absurd pattern and when you write an absurd lambda \(), Agda will
replace it by a fresh name which is a function defined by an absurd
pattern.
A consequence of that is that \() is not definitionally equal to \(),
or more generally you don’t have

let x = \() in M   definitionally equal to    M[\() / x]

because in the first case only one new function will be generated, and
in the second case one new function will be generated for each
occurrence of x in M.

In your case, you can maybe work around this issue by defining a
function Fin0-elim which proves anything given an element of Fin 0
(this function is defined by an absurd pattern or absurd lambda), and
then only use Fin0-elim instead of absurd lambdas.

Guillaume

2013/5/23 Martin Escardo <m.escardo at cs.bham.ac.uk>:
> I have a problem with absurdity in Agda, which I can solve in an undesirable
> way, which forces me to change several definitions.
>
> I would like to both understand what the problem is, and why the desirable
> way doesn't work.
>
> I have three types X,Y,Z, whose definition I omit here. I can define, using
> absurd patterns,
>
> x : X
> x = \a ()
>
> y : Y
> y : \()
>
> z : Z
> z : \()
>
> These are types which have a parameter n:N that happens to be zero and so
> they trivialize in this special case, as they have occurrences of Fin n in
> their definitions.
>
> Now I have three holes in a definition (of a fourth type), reported to have
> types X,Y,Z. I can fill the holes with x,y,z, and the definition
> type-checks.
>
> But if I instead fill the holes with \a (), \(), and \(), expanding the
> definitions of x,y,z, then type-checking fails.
>
> Moreover, if just one of the three holes is filled with the corresponding
> term, type checking still fails.
>
> Additionally, if I ask the emacs interface to fill the wholes with ctrl-c-a,
> this succeeds, with expressions containing the string "absurd". But then the
> resulting expression doesn't type check.
>
> And there is a more annoying fact. I have previous definition of something
> else that uses \() and does type check. However, when I use it, things fail.
> I instead need to use the same definition with replaced \() by y.
>
> This is very mysterious to me.
>
> I didn't manage to distil a simple instance of this to reproduce here. But
> if you are brave enough, you can search for "AGDA PROBLEM" in any of the two
> following links:
>
> http://www.cs.bham.ac.uk/~mhe/dialogue/dialogue-lambda.html
> http://www.cs.bham.ac.uk/~mhe/dialogue/dialogue-lambda.lagda
>
> Help is appreciated.
>
> Martin
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda