Rec_on arguments

Stream: new members

[ROCKY KAMEN-RUBIO]

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]

don't use rec_on in tactic mode. Instead, use induction

[Kenny Lau]

if you want to keep the orders of the arguments when using apply, use fapply

[Kenny Lau]

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

[Kenny Lau]

but preferably use induction hk

[ROCKY KAMEN-RUBIO]

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]

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]

it looks like I misread the whole thing. The instance of mult_3 is in your goal, not your hypothesis.

[Kenny Lau]

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]

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]

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]

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

[Kevin Buzzard]

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]

actually, rewrite, and then induct on k to prove mult_3 (3 * k)

[Kevin Buzzard]

Even better.

[ROCKY KAMEN-RUBIO]

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]

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]

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]

The formalisation of the question itself is bad

[Kevin Buzzard]

n plays no role and is now screwing you up

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

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]

The statement of div3_imp_p is nonsense; you can prove it by exact hyp on the first line

[Mario Carneiro]

you've assumed what you wanted to prove

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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]

The unfold, rw mul_zero and change steps are optional because they make definitionally equal changes to the goal

[Kenny Lau]

@Mario Carneiro feel free to post your short solutions here