How to use induction in Idris 1.3.2?

Question

I'm learning Idris, and in particular I would like to learn how to prove statements.

The stupidest of all exercises is, of course, associativity of the sum of natural numbers, and I'm comfortable with the theory and with what style of proof I shall use (induction on the first argument and rewriting), but I'm stuck because of some possible incompatibility between the Idris version used in tutorials and mine (1.3.2).

This is my code:

module SumAssoc

plusAssoc : (l, c, r : Nat) -> (l + (c + r) = (l + c) + r)
plusAssoc Z c r = Refl
plusAssoc (S k) c r = rewrite plusAssoc k c r in Refl

-- ↑
-- this proof works well.
-- now for an inductive proof with tactics...

plusAssoc' : (l, c, r : Nat) -> (l + (c + r) = (l + c) + r)
plusAssoc' l c r = ?hole

When I attempt to prove it using the tactic

intros
induction l
...

I get stuck and receive the following error message:

Prover error:
  |
  | induction l
  | ^
unexpected "induction l":
expected tactic

This has to do, of course, with the fact that the :prove environment is now deprecated. But I don't know how to address the issue, as all my attempts failed:

:elab hole doesn't seem to work better (mostly because I have nowhere to learn the syntax and logic of the library)
Using pruviloj fails as well.

plusAssoc' : (l, c, r : Nat) -> (l + (c + r) = (l + c) + r)
plusAssoc' Z c r = Refl
plusAssoc' (S k) c r = ?hole_2

---------- Proofs ----------

SumAssoc.hole_2 = proof
  intros
  rewrite plusAssoc' k c r
  trivial

EDIT: This works, but it's also deprecated. And, understandably, I would like to manage how to prove things by induction.

EDIT 2: I managed to go on a little bit with this series of commands in :elab hole:

plusAssoc'' : (l, c, r : Nat) -> (l + (c + r) = (l + c) + r)
plusAssoc'' l c r = ?hole_3

don't ask which dark Grimoire I had to consult in order to learn that this was the correct syntax:

:elab hole_3
intro `{{l}}
induction (Var `{{l}})
compute

At this point, this is the result I see in the terminal

{S_147}
----------              Assumptions:              ----------
 l : Nat
----------                 Goal:                  ----------
{Z_146} : (c : Nat) -> (r : Nat) -> plus c r = plus c r

It would be very nice to conclude the base of the induction using reflexivity, but...

The goal is not an equality, so Pruviloj.Core.reflexivity is not applicable.

It would be very nice to introduce the remaining variables, but...

INTERNAL ERROR: Can't introduce here.
This is probably a bug, or a missing error message.
Please consider reporting at https://github.com/idris-lang/Idris-dev/issues

Alexander Gryzlov Alexander Gryzlov · Accepted Answer · 2019-08-20T15:51:00

You need to compute and attack before introducing new variables, though I'm not exactly sure why :) Here's the full tactic script that works:

plusAssoc' : (l, c, r : Nat) -> (l + (c + r) = (l + c) + r)
plusAssoc' = %runElab tac 
  where 
  tac : Elab ()
  tac = do [l,c,r] <- intros
           [z,s] <- induction (Var l)

           focus z
           compute
           reflexivity

           focus s 
           compute
           attack
           [n, prf] <- intros
           rewriteWith (Var prf)
           reflexivity
           solve

How to use induction in Idris 1.3.2?

1 Answers