absurd/void in elaboration

[r k]

If I have some proof of absurdity in coq tactic, i can do

  case proof_of_False

In idris, i can use void/absurd like :

f : (a:Nat) -> (b:Nat) -> (k: (Z = (S Z)) -> (a=b)
f _ _ k = absurd k

How can I write the above function via elaboration

f = %runElab (do
  intro'
  intro'
  intro'
  -- ...
  )

[Melvar Chen]

I would expect you’d just apply absurd again, just building the term with Elab this time.

[r k]

After lots of tries, i was able to get absurd to run, though it requires building the whole term providing every implicit argument, both to absurd and (=)

fill `((absurd {a=((=) {A=Nat} {B=Nat} ~(Var $ UN "a") ~(Var $ UN "b"))} {t=((=) {A=Nat} {B=Nat} Z (S Z))} ~(Var $ UN "k")))

I was hoping if there is some better way to achieve this.

[Melvar Chen]

I wouldn’t even expect that to work since it’s missing the Uninhabited instance. I meant something like this:

make_f : TTName -> Elab ()
make_f f = do
  intro'
  intro'
  k <- gensym "k"
  intro k
  [_, _, impl, hole_k] <- apply (Var `{absurd}) [True, True, False, False]
  solve
  focus hole_k
  fill (Var k)
  solve
  focus impl
  resolveTC f

f : (a, b : Nat) -> (k: Z = S Z) -> (a = b)
f = %runElab (make_f `{f})

[r k]

Thanks, this solves my issue. Though I dont fully understand the resolveTC yet. Few things which I missed was that the constraint (Uninhabited t) is a parameter for absurd (at first i was puzzled by 4 args, :doc only shows 3).

[David Christiansen]

On 26/11/16 06:52, r k wrote:
> After lots of tries, i was able to get absurd to run, though it requires

> building the whole term providing every implicit argument, both to *absurd*
> and *(=)*

>
> fill `((absurd {a=((=) {A=Nat} {B=Nat} ~(Var $ UN "a") ~(Var $ UN "b"))}
> {t=((=) {A=Nat} {B=Nat} Z (S Z))} ~(Var $ UN "k")))
>
> I was hoping if there is some better way to achieve this.

Yes, there is a better way. Here's a general-purpose tactic for
resolving any goal that has an absurdity in its context, so long as
there's an Uninhabited instance for the type that's absurd.

If you need help understanding part of it, please let me know.

/David

module Contradiction

import Language.Reflection.Utils

%default covering

||| Given an absurdity, resolve the current goal. Otherwise, fail.
covering
absurdity : Raw -> Elab ()
absurdity oops =
do [aH, tH, dict, arg] <- apply (Var `{absurd}) [True, True, False,
False]
| _ => fail [TextPart "Bug in tactic definition! Wrong number
of holes."]
solve
focus arg
fill oops ; solve
focus dict
resolveTC `{absurdity}


||| If the current context contains an uninhabited type, solve the
current goal.
export
contradiction : Elab ()
contradiction =
do env <- map fst <$> getEnv
contraIn env
where contraIn : List TTName -> Elab ()
contraIn [] =
fail [TextPart "No absurdities in scope."]
contraIn (n :: ns) =
absurdity (Var n) <|> contraIn ns



foo : Int -> Nat -> Void -> List Integer -> String
foo x k y xs = %runElab contradiction

bar : String -> (String -> ()) -> Z = S Z -> ()
bar x f prf = %runElab contradiction

[David Christiansen]

If you're using elab reflection, I'd highly recommend using the Emacs
mode for Idris, because I spent a fair bit of time adding features to it
that are useful for debugging Elab scripts.

In particular, because elaborator reflection works with TT, it can be
very useful to see the TT representation of a type signature. In Emacs,
this is done by right-clicking the type signature and picking "Show
core" from the menu. If you don't have a mouse, then C-c C-SPC provides
the same menu from the keyboard, or C-c C-m c for this particular command.

This also works in REPL expressions and in error messages. As far as I
know, nobody has yet implemented these features for other editors,
unfortunately.

The docstring for resolveTC says:
Language.Reflection.Elab.Tactics.resolveTC : (fn : TTName) -> Elab ()
Attempt to solve the current goal with an interface dictionary
Arguments:
fn : TTName -- the name of the definition being elaborated (to
prevent Idris
from looping)

This means that, if the current goal is an interface (such as
Uninhabited (S Z = Z) or Uninhabited Void or Functor List), it can be
dispatched using "resolveTC" which does the interface dictionary
resolution that Idris normally does when you call a function like "map"
or "absurd". In Coq, this is called type class resolution and it happens
as part of the unification procedure, if I've understood correctly.

The name that's a parameter to resolveTC is a way of breaking cycles
when defining interface dictionaries. Just pass whatever you're
currently elaborating or building as the name there.

/David

[r k]

Nice, that was precisely I was looking for. Thanks a lot !

Considering the pervasive usage of "case proof_of_False" in a Coq tutorial I gone through (by Mike Nahas), I initially thought something like this must be in library which I probably missed, but couldnt find anywhere (including any code samples or examples on internet or in various research papers).

Thanks again for pointing out Emacs, I was doing it on terminal and one major initial trip (as an absolute beginner, who never formally studied dep. types or any related theory) was that by default it doesnt show the term (which later i figured out can be seen by :term or debug). The part in the docs and research papers which said "use attack if necessary" made no sense but was clear after looking at term.