# Zulip Chat Archive

## Stream: new members

### Topic: rw with inductive types

#### ROCKY KAMEN-RUBIO (Apr 28 2020 at 19:33):

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 `int`

s. 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 (Apr 28 2020 at 21:28):

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 (Apr 28 2020 at 22:05):

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 (May 01 2020 at 02:02):

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 (May 01 2020 at 02:22):

**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 `int`

s 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 (May 01 2020 at 02:32):

`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 (May 01 2020 at 02:33):

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 (May 01 2020 at 02:35):

You probably shouldn't be pattern matching on `int`

though, this is a kind of implementation detail

#### Mario Carneiro (May 01 2020 at 02:36):

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 (May 01 2020 at 02:37):

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 (May 01 2020 at 02:41):

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 (May 01 2020 at 02:48):

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 (May 01 2020 at 02:49):

it affects `rw`

, which does pattern matching only up to syntactic equality

#### Mario Carneiro (May 01 2020 at 02:50):

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 (May 01 2020 at 02:56):

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 (May 01 2020 at 02:56):

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 ~~ OH! I SEE! When I defined `2 = 1 + 1`

? `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`

.

Last updated: Dec 20 2023 at 11:08 UTC