how to induction...? ;w;

Stream: new members

[Lawrence Lin]

https://leanprover.github.io/logic_and_proof/the_natural_numbers_and_induction_in_lean.html#induction-and-recursion-in-lean
so i was reading through this link above earlier, but... i tried recreating some induction proofs on my own.

import tactic

def fib : ℕ -> ℤ
| 0 := 1
| 1 := 1
| (x+2) := fib (x+1) + fib (x)

example (n : ℕ) : fib(n) * fib(n+2) - fib(n+1)^2 = (-1)^n :=
begin
  nat.rec_on n
  sorry,
end

but lean got upset at my use of nat.rec_on, and broke there. what does nat.rec_on actually do?

[Sky Wilshaw]

nat.rec_on is a built-in recursor that can be used for writing recursive definitions and recursive proofs in term mode. Since you're writing a proof in tactic mode, you should probably try to use tactics such as induction n.

[Sky Wilshaw]

In this case, using induction n should give you two goals:

• prove your statement for n = 0
• prove your statement for n + 1, assuming it's true for n (this should be a hypothesis called something like ih, "inductive hypothesis")

[Lawrence Lin]

thank you!!

[Lawrence Lin]

okay, bit of a silly question this time around but
after using

example (n : ℕ) : fib(n) * fib(n+2) - fib(n+1)^2 = (-1)^n :=
begin
  induction n
  (show fib(0) * fib(0+2) - fib(0+1)^2 = (-1)^0, from calc
        fib(0) * fib(2) - fib(1)^2 = (-1)^0 : by rw zero_add
        fib(0) * fib(2) - fib(1)^2 = 1      : by rw pow_zero)

  sorry,
end

i'm getting the error

function expected at
  n
term has type
  ℕ

... any idea what's happening here? (also the induction proof for case n = 0 isn't done yet)

[Sky Wilshaw]

The proofs from the link you sent are all term-mode proofs, but you're in tactic mode.

[Sky Wilshaw]

You can do similar things, but the syntax is a bit different.

[Sky Wilshaw]

Your example might look like:

[Sky Wilshaw]

example (n : ℕ) : fib(n) * fib(n+2) - fib(n+1)^2 = (-1)^n :=
begin
  induction n,
  { calc
        fib(0) * fib(2) - fib(1)^2 = (-1)^0 : by rw zero_add
        fib(0) * fib(2) - fib(1)^2 = 1      : by rw pow_zero
  },
  sorry,
end

[Sky Wilshaw]

But I haven't tested it so it might not work.

[Lawrence Lin]

oh hmm... let me try again. what's the difference between term mode and tactic mode?

[Sky Wilshaw]

You don't actually need to use calc here, it might be easier to write

induction n,
{ rw zero_add,
  rw pow_zero },

[Sky Wilshaw]

Term mode is what you might be familiar with from other programming languages. You basically write down explicit function applications and things to construct a term of a particular type.

[Lawrence Lin]

hmm

[Sky Wilshaw]

Tactic mode is started with begin and ended with end. It's an interactive mode, where lean tells you the current "goal" (the |- looking thing) and all of your hypotheses, and you tell it some instructions (tactics) to get yourself gradually closer to solving the goal.

[Lawrence Lin]

right, makes sense

[Sky Wilshaw]

induction n is a tactic that tells lean to try to get closer to solving the goal by applying induction on variable n.

[Sky Wilshaw]

Once you solve a goal in term mode, lean will convert it into a term that basically contains the result of all your instructions. In the link you sent, the proofs provided were written "manually" in term mode, but we often write them in a more readable way using tactics.

[Sky Wilshaw]

(Recall under the propositions as types correspondence, terms of types are proofs of propositions)

[Lawrence Lin]

hmm i see