Idris mush tactic

Question

So I was reading this paper on elaborator reflection (https://eb.host.cs.st-andrews.ac.uk/drafts/elab-reflection.pdf) and decided I wanted to try this this tactic out (found in section 5.2):

mush : Elab ()
mush =
   do attack
      x <- gensym "x"
      intro x
      try intros
      induction (Var x) `andThen` auto
      solve

Supposedly this tactic could prove associativity of addition:

plusAssoc : (j, k, l : Nat) -> plus (plus j k) l = plus j (plus k l)
plusAssoc = %runElab mush

however when trying to typecheck mush I get the following error:

error: not a terminator, expected: "$", "&&", ")", "", ">", "+", "++", "-", "->", ".", "/", "/=", "::", ";", "<", "", "<", "<>", "<+>", "<<", "<=", "<|>", "=", "==", ">", ">=", ">>", ">>=", "\\", "`", "in", "||", "~=~", ambiguous use of a left-associative operator, ambiguous use of a non-associative operator, ambiguous use of a right-associative operator, end of input, matching application expression, where block x <- gensym "x" ^

I do not understand what is wrong, is the mush-tactic not correct or is there something I need to add to my file?

Anton Trunov Anton Trunov · Accepted Answer · 2016-10-14T09:08:46

First of all, you need to add some imports:

import Language.Reflection
import Pruviloj.Core
import Pruviloj.Induction

auto : Elab ()
auto =
  do compute
     attack
     try intros
     hs <- map fst <$> getEnv
     for_ hs $
       \ih => try (rewriteWith (Var ih))
     hypothesis <|> search
     solve

mush : Elab ()
mush =
   do attack
      x <- gensym "x"
      intro x
      try intros
      induction (Var x) `andThen` auto
      solve

plusAssoc : (j, k, l : Nat) -> plus (plus j k) l = plus j (plus k l)
plusAssoc = %runElab mush

Then you need to tell Idris to use the package Pruviloj:

idris -p pruviloj <fileName.idr>

That typechecks and works, but I wasn't able to reproduce your error message.

Idris mush tactic

1 Answers