## 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,

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)

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 mul_one at h,
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 nbut 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