rw with inductive types

Stream: new members

[ROCKY KAMEN-RUBIO]

I'm trying to prove some identities using Lucas and Fibonacci numbers on natural numbers and integers. I have defined both inductively, but am finding that rewrites that work on the nat case fail for ints. The error message I get is pretty minimal and unhelpful.

import data.nat.basic
import data.nat.fib
import data.int.basic
import data.list.basic
import tactic

@[reducible]
def fib_Z : ℤ → ℤ
| (int.of_nat n) := int.of_nat (nat.fib n)
| - (int.of_nat (n+1)) := if n%2 = 0 then - (int.of_nat (nat.fib (n+1))) else int.of_nat (nat.fib (n+1))

@[reducible]
def luc_N : ℕ → ℕ
| 0 := 2
| 1 := 1
| (n+2) := luc_N n + luc_N (n+1)

@[reducible]
def luc_Z : ℤ → ℤ
| (int.of_nat n) := int.of_nat (luc_N n)
| - (int.of_nat (n+1)) := if n%2 = 0 then - (int.of_nat (luc_N (n+1))) else int.of_nat (luc_N (n+1))

--Minimal working examples
example : luc_Z 0 = int.of_nat (nat.fib 1 + nat.fib 1) :=
begin
rw luc_Z,
simp,
end

example : luc_N 0 = (nat.fib 1 + nat.fib 1) :=
begin
rw luc_N,
simp,
end

--a little more context
lemma l0 {n : ℤ} : luc_Z n = fib_Z (n-1) + fib_Z (n+1) :=
begin
cases n with n,
cases n with n,
simp,
rw fib_Z,
rw luc_Z,
sorry,
end

[Kevin Buzzard]

The rw tactic takes a hypothesis h of the form X = Y and replaces all X's by Y's in the goal. The error failed means "I have no idea what you're talking about".

[Alex J. Best]

For your first two proofs simp, refl works for me. Your second has a subgoal luc_Z 0 = fib_Z (-1) + fib_Z 1 which isn't true, the LHS is 2 and the RHS is 0, its true with nat subtraction 0-1=0 but not for ints.

[ROCKY KAMEN-RUBIO]

Kevin Buzzard said:

The rw tactic takes a hypothesis h of the form X = Y and replaces all X's by Y's in the goal. The error failed means "I have no idea what you're talking about".

I see. There were other times where I could get away with things like rw nat.fib but I guess I shouldn't count on rw know that when I give it luc_Z I actually mean "see that the argument I gave this thing is one of its constructors and give me that value"?

Alex J. Best said:

For your first two proofs simp, refl works for me. Your second has a subgoal luc_Z 0 = fib_Z (-1) + fib_Z 1 which isn't true, the LHS is 2 and the RHS is 0, its true with nat subtraction 0-1=0 but not for ints.

Right, I keep forgetting about nat subtraction. Would the solution be to re-index so that when I do cases on my int I don't end up with a negative nat?

[ROCKY KAMEN-RUBIO]

Alex J. Best Here's an example where just doing simp, refl doesn't work.

lemma fZn1 : fib_Z (-1) = 1 :=
begin
simp,
refl,
end

I think I might be misunderstanding the way ints work in lean; when I do #reduce fib_Z (-1) I get -[1+ 0] instead of just -1. Would this be affecting my pattern matching?

[Mario Carneiro]

int has two constructors, int.of_nat and int.neg_succ_of_nat, representing the functions n : nat => n and n : nat => -n-1 respectively (in order to keep the ranges disjoint)

[Mario Carneiro]

the latter function is pretty printed as -[1+ n] but keep in mind that all of those are not separate bits of syntax; -[1+ is one token

[Mario Carneiro]

You probably shouldn't be pattern matching on int though, this is a kind of implementation detail

[Mario Carneiro]

Oh I see, you wrote - int.of_nat (n+1) as your pattern, which would almost never work in other cases but happens to work here because that is defeq to -[1+n]

[Mario Carneiro]

however, it will affect the statements of the equations, so you will have an equation saying fib_Z (- int.of_nat (n+1)) = ... and not fib_Z -[1+ n] = ..., which causes a problem when you use induction since it will use -[1+ n] to write the second case

[Mario Carneiro]

Your first example can be solved by rfl, and the second would be solved by rfl except that it is false:

#eval to_bool (luc_Z 0 = fib_Z (-1) + fib_Z 1) -- ff

[ROCKY KAMEN-RUBIO]

Mario Carneiro said:

You probably shouldn't be pattern matching on int though, this is a kind of implementation detail

Should I do it using if ... then ... else ... statements then to define fib_Z?

Mario Carneiro said:

Oh I see, you wrote - int.of_nat (n+1) as your pattern, which would almost never work in other cases but happens to work here because that is defeq to -[1+n]

I'm not too committed to this implementation so I could change my references to these definitions. I'm not fully understanding why this would behave differently though if it's defeq?

[Mario Carneiro]

it affects rw, which does pattern matching only up to syntactic equality

[Mario Carneiro]

It doesn't fix the issue with rewriting fib_Z 0 because this is not written using the constructor either. Luckily you can usually rfl the zero case of the theorem

[Mario Carneiro]

For this particular case, defining it using pattern matching on int is not unreasonable, since you are defining the int version of a nat definition. You could do it without if or case splits using (-1)^int.to_nat (-n) * fib (int.nat_abs n) or thereabouts.

[ROCKY KAMEN-RUBIO]

Mario Carneiro said:

it affects rw, which does pattern matching only up to syntactic equality

Oh I see. That makes sense. My intuition for how smart this tactics are is still forming.

Mario Carneiro said:

Your first example can be solved by rfl, and the second would be solved by rfl except that it is false:

#eval to_bool (luc_Z 0 = fib_Z (-1) + fib_Z 1) -- ff

Wouldn't this reduce to 2 = 1 + 1? OH! I SEE! When I defined fib_N I should have done my parity check n%2 on n+1 instead of n. That's why fib_Z (-1) was returning -1 instead of 1.