# Zulip Chat Archive

## Stream: new members

### Topic: Rec_on arguments

#### ROCKY KAMEN-RUBIO (Apr 10 2020 at 07:18):

I'm confused about the behavior of `rec_on`

. Specifically, in the example below, I'm trying to prove something is true for both instances of my inductive definition `mult_3`

, which only has two cases, but I'm getting three new goal states. In term mode, I understand that `rec_on`

takes in three args, but isn't the goal state here the "first" of those three? The first goal I get when I do this looks identical to the original goal state as well, which doesn't seem right.

import data.nat.basic import data.set open nat inductive mult_3 : set ℕ | mult_3_O : mult_3 0 | mult_3_SSS : ∀ n, mult_3 n → mult_3 (n + 3) example (n k : ℕ) : n = 3*k → mult_3 n := begin intro h, cases h with k hk, apply mult_3.rec_on, end

#### Kenny Lau (Apr 10 2020 at 07:19):

don't use `rec_on`

in tactic mode. Instead, use `induction`

#### Kenny Lau (Apr 10 2020 at 07:20):

if you want to keep the orders of the arguments when using `apply`

, use `fapply`

#### Kenny Lau (Apr 10 2020 at 07:20):

also try minimize the number of lines by using `apply mult_3.rec_on hk`

instead

#### Kenny Lau (Apr 10 2020 at 07:20):

but preferably use `induction hk`

#### ROCKY KAMEN-RUBIO (Apr 10 2020 at 07:29):

It seems like `induction`

defaults to the type of the variable I apply it to. Is there a way to tell `induction`

that I want it to work on the cases of `mult_3`

instead of the cases of `nat`

, even though everything in `hk`

is a `nat`

?

#### Donald Sebastian Leung (Apr 10 2020 at 07:35):

If you have some `hyp : mult_3 n`

then `induction hyp`

should perform structural induction on `mult_3`

instead of ordinary induction on `n`

.

#### Kenny Lau (Apr 10 2020 at 07:43):

it looks like I misread the whole thing. The instance of `mult_3`

is in your goal, not your hypothesis.

#### Kenny Lau (Apr 10 2020 at 07:45):

so 1. `mult_3.rec_on`

will never work because it is used for destructing an instance of `mult_3`

in your hypothesis, and 2. you should induct on `k`

instead

#### ROCKY KAMEN-RUBIO (Apr 10 2020 at 07:45):

Donald Sebastian Leung said:

If you have some

`hyp : mult_3 n`

then`induction hyp`

should perform structural induction on`mult_3`

instead of ordinary induction on`n`

.

Interesting. That makes sense, and seems to be working for me, but it feels weird to have to make something of that type just to tell induction to act on it.

Kenny Lau said:

it looks like I misread the whole thing. The instance of

`mult_3`

is in your goal, not your hypothesis.

Yeah I'm trying to show `mult_3 n `

.

#### ROCKY KAMEN-RUBIO (Apr 10 2020 at 08:01):

Kenny Lau said:

so 1.

`mult_3.rec_on`

will never work because it is used for destructing an instance of`mult_3`

in your hypothesis, and 2. you should induct on`k`

instead

I tried inducting on k and got stuck here. My thinking was that this was tricky because I should have been exploiting the structure of mult_3 more directly, but maybe there's a way forward I'm not seeing?

example (n k : ℕ) : n = 3*k → mult_3 n := begin intro h, induction k with l hl, rw mul_zero at h, rw h, apply mult_3.mult_3_O, rw succ_eq_add_one at h, end

Edit: copied the wrong code initially and had to modify.

#### Kevin Buzzard (Apr 10 2020 at 08:04):

This is no good -- your induction hypothesis is useless.

#### Kevin Buzzard (Apr 10 2020 at 08:04):

You need to do induction before the intro. You need to think carefully about precisely which statement you need to prove by induction.

#### Kenny Lau (Apr 10 2020 at 08:05):

actually, rewrite, and then induct on `k`

to prove `mult_3 (3 * k)`

#### Kevin Buzzard (Apr 10 2020 at 08:05):

Even better.

#### ROCKY KAMEN-RUBIO (Apr 10 2020 at 08:15):

Kenny Lau said:

actually, rewrite, and then induct on

`k`

to prove`mult_3 (3 * k)`

This seems a lot better but I'm still getting stuck at the end with my index off by one.

example (n k : ℕ) : n = 3*k → mult_3 n := begin intro h, rw h, induction k with l hl, rw mul_zero, apply mult_3.mult_3_O, rw succ_eq_add_one, rw succ_eq_add_one at h, rw mul_add at h, rw mul_one at h, rw mul_add, apply mult_3.mult_3_SSS, apply hl, end

#### Mario Carneiro (Apr 10 2020 at 08:18):

you need to delete hypothesis `h`

before the induction, or else it will get automatically pulled into the induction hypothesis making it useless

#### Mario Carneiro (Apr 10 2020 at 08:18):

alternatively you can use `induction k with l hl generalizing n`

, but the variable `n`

is already useless by that point so there is no reason to

#### Kevin Buzzard (Apr 10 2020 at 08:19):

The formalisation of the question itself is bad

#### Kevin Buzzard (Apr 10 2020 at 08:19):

n plays no role and is now screwing you up

#### Kevin Buzzard (Apr 10 2020 at 08:19):

Just prove mult_3 (3*k) and drop the n

#### Kevin Buzzard (Apr 10 2020 at 08:21):

You don't want a function which demands n as an input and then immediately demands a proof that it's equal to something else

#### ROCKY KAMEN-RUBIO (Apr 10 2020 at 08:25):

Kevin Buzzard said:

Just prove mult_3 (3*k) and drop the n

So the larger proof I'm trying to write uses `def div3 (n:ℕ) := ∃ (k : ℕ), n = 3*k`

, and the question would be stated as `div n \r mult_3 n`

but I felt like that would have cluttered this example. I agree this formalism is bad.

#### Mario Carneiro (Apr 10 2020 at 08:26):

You can do the small amount of logical glue to connect `mult_3 (3*k)`

to `3 \| n -> mult_3 n`

in the proof of the latter

#### ROCKY KAMEN-RUBIO (Apr 11 2020 at 02:00):

This is how I was ultimately able to do it. I kept get stuck not generalizing my n properly at the end with the induction on k, but induction on `hyp : mult_3 n`

worked. Maybe I'm missing something.

import data.nat.basic import data.set open nat inductive mult_3 : set ℕ | mult_3_O : mult_3 0 | mult_3_SSS : ∀ n, mult_3 n → mult_3 (n + 3) def div3 (n:ℕ) := ∃ (k : ℕ), n = 3*k lemma p0 : mult_3 0 := mult_3.mult_3_O lemma div3_imp_p (n:ℕ) {hyp : mult_3 n}: div3 n → mult_3 n := begin rw div3, induction hyp, intro h, exact p0, intro h, apply mult_3.mult_3_SSS, exact hyp_a, end

#### Mario Carneiro (Apr 11 2020 at 02:31):

The statement of `div3_imp_p`

is nonsense; you can prove it by `exact hyp`

on the first line

#### Mario Carneiro (Apr 11 2020 at 02:32):

you've assumed what you wanted to prove

#### Mario Carneiro (Apr 11 2020 at 02:37):

This is a totally unfair proof since you probably haven't seen most of these tricks but fwiw

lemma div3_imp_p (n:ℕ) : div3 n → mult_3 n := begin rintro ⟨k, rfl⟩, induction k; constructor, assumption, end

#### Mario Carneiro (Apr 11 2020 at 02:40):

or the one liner version

lemma div3_imp_p : ∀ {n}, div3 n → mult_3 n | _ ⟨k, rfl⟩ := by induction k; constructor; assumption

#### ROCKY KAMEN-RUBIO (Apr 11 2020 at 02:59):

Cool! Yeah I'm not too familiar with most of those tactics so I'll read up some more.

#### Mario Carneiro (Apr 11 2020 at 03:06):

Here is the same proof but being more explicit about the changes

lemma div3_imp_p {n} (h : div3 n) : mult_3 n := begin unfold div3 at h, cases h with k e, subst e, induction k with k IH, { rw mul_zero, exact mult_3.mult_3_O }, { change 3 * succ k with 3 * k + 3, apply mult_3.mult_3_SSS, exact IH } end

#### Mario Carneiro (Apr 11 2020 at 03:07):

The `unfold`

, `rw mul_zero`

and `change`

steps are optional because they make definitionally equal changes to the goal

#### Kenny Lau (Apr 11 2020 at 04:14):

@Mario Carneiro feel free to post your short solutions here

Last updated: May 08 2021 at 11:09 UTC