induction h : xs vs induction xs

Stream: new members

[fkefjlwejlfk]

Dear all,

I am working on a large proof and have some problems with the induction tactic.
I perform induction on a list xs which gives me two cases.

I am able to solve the first case (list.nil) if I use the notation induction h : xs because this introduces h which I can use for my proof.

I am able to solve the second case (list.cons) if I use the notation induction xs. However, if I use the induction h : xs syntax, it introduces a term in my induction hypothesis which isn't provable. But when I use induction xs, I lack the h term in the first case which makes it insolveable.

TL;DR Can I use a certain syntax so I have the behavior of induction h : xs in one case and the behavior of induction xs in the other case?

[Anne Baanen]

I'm not entirely sure in your specific case, it would help to write a #mwe. You might have success with the induction' tactic, which should be smart enough to keep your goal provable.

[Anne Baanen]

See tactic#induction'

[Anne Baanen]

See docs#tactic.interactive.induction' (apparently it hasn't been added to the mathlib tactic overview)

[fkefjlwejlfk]

Anne Baanen said:

I'm not entirely sure in your specific case, it would help to write a #mwe. You might have success with the induction' tactic, which should be smart enough to keep your goal provable.

induction' also doesn't work. Generating a #mwe will get quite extensive because a lot of functions are deeply nested resulting in a complex ih. Isn't there a way to rewrite the induction hypothesis? It seems pretty odd to me that merely introducing h will break one of the cases.

[Riccardo Brasca]

I think that what Anne is saying is that we don't really understand the problem, so it's difficult to help. If you have a working example you can post it. You can replace all proof by sorry to keep it small.

[Riccardo Brasca]

But of course you cannot sorry definitions.

[fkefjlwejlfk]

@Riccardo Brasca @Anne Baanen I have constructed a #mwe that has the same problem :

def foo (n : ℕ) : list ℕ -> option ℕ
| (x :: xs) := if x = n then some x else foo xs
| [] := none

def gen_list (n : ℕ) : list ℕ :=  [n + 2] ++ [n+1] ++ [n]

def is_foo_able (n : ℕ) : bool :=
match (foo n (gen_list n)) with
| some _ := tt
| none := ff
end


lemma foo_able (n : ℕ) : (is_foo_able n = tt) -> (foo n (gen_list n)) = some n :=
begin
  unfold is_foo_able,
  intro s,
  cases' hh : foo n (gen_list n),  -- This is the relevant line
  {finish},
  {
    induction' hh2 :  gen_list n,
    {
      finish
    },
    {
      apply (ih n),
      finish,
      finish,
      -- fails here
    }
  }
end

I have induction' hh2 : gen_list n, in the first case this introduces hh2 : gen_list n = nil which can then be used to create a contradiction. In the second case though you get hh2: gen_list n = hd :: x and ih: ∀ (n : ℕ), is_foo_able._match_1 (foo n (gen_list n)) = tt → ∀ (val : ℕ), foo n (gen_list n) = some val → gen_list n = x → some val = some n, notice the gen_list n = x term in ih, this is obviously false and makes the induction hypotheses completely useless.

However, if I change induction' hh2 : gen_list n to induction' gen_list n then in the second case get ih: ∀ (n : ℕ), is_foo_able._match_1 (foo n (gen_list n)) = tt → ∀ (val : ℕ), foo n (gen_list n) = some val → some val = some n which can be used to proof the goal. However, in the first case we no longer have hh2 : gen_list n = nil so the contradiction can't be proven anymore.

This means that with one notation I can prove one case, and with the other notation I can proof the other case. I can't proof both cases :(

[Junyan Xu]

Not sure but maybe you can try the generalize h : gen_list n = l, syntax in tactic#generalize first, then induction l

[Anne Baanen]

Thanks for the MWE, I get the issue now! However, my conclusion is that this is just not a thing that is provable through induction: gen_list n is a specific list of length 3, so what happens if you apply the inductive hypothesis four times? How should we express the relation between the list x in the inductive hypothesis and gen_list n?

[fkefjlwejlfk]

Anne Baanen said:

Thanks for the MWE, I get the issue now! However, my conclusion is that this is just not a thing that is provable through induction: gen_list n is a specific list of length 3, so what happens if you apply the inductive hypothesis four times? How should we express the relation between the list x in the inductive hypothesis and gen_list n?

The thing is, in my real world example (so not this #mwe) the list is of an arbitrary length and has this exact problem. it just seems impossible to solve both cases sadly :(

[fkefjlwejlfk]

Junyan Xu said:

Not sure but maybe you can try the generalize h : gen_list n = l, syntax in tactic#generalize first, then induction l

sadly results in the same problem..

[fkefjlwejlfk]

@Anne Baanen By the way any other way to proof this would be acceptable. I feel though like induction' would be the most natural way. In this case I could do a brute force proof but in the real problem the list is of arbitrary length.

[Floris van Doorn]

The general strategy of such proofs is to generalize the statement of what you're trying to prove so that it holds for an arbitrary list (not just the particular gen_list n) and then perform induction. The way to perform this step really depends on your actual situation, so I cannot comment on it from your MWE. Maybe an idea is to first try to understand mathematically why what you're proving is true, before writing it in Lean.

Your request to mix and match different induction principles from different induction invocations allows you to prove false things, so therefore it's not allowed.

[fkefjlwejlfk]

Floris van Doorn said:

The general strategy of such proofs is to generalize the statement of what you're trying to prove so that it holds for an arbitrary list (not just the particular gen_list n) and then perform induction. The way to perform this step really depends on your actual situation, so I cannot comment on it from your MWE. Maybe an idea is to first try to understand mathematically why what you're proving is true, before writing it in Lean.

Your request to mix and match different induction principles from different induction invocations allows you to prove false things, so therefore it's not allowed.

I still don't get this. What you are saying is if I use induction' xs instead of induction' h : xs it is no longer valid to assume that gen_list n = nil in case nil? I have trouble understanding that part as it seems very counter intuitive

[Floris van Doorn]

Exactly.
If you want an induction step where you don't want that the induction hypothesis depends on the assumption gen_list n = x, which you call "obviously false", then you also cannot assume it for the nil case. Otherwise you're doing a different induction in the nil and the cons case, and you can easily prove false if you do that.

[fkefjlwejlfk]

Floris van Doorn said:

Exactly.
If you want an induction step where you don't want that the induction hypothesis depends on the assumption gen_list n = x, which you call "obviously false", then you also cannot assume it for the nil case. Otherwise you're doing a different induction in the nil and the cons case, and you can easily prove false if you do that.

Thank you for your answer, I am sorry if my "obviously false" comment came across wrong, what I meant by this is that this would have me proof "gen_list n = x" which is "obviously false" since we have "gen_list n = hd :: x" in our environment. So I guess the induction' strategy is completely out of the window then, unless I can somehow find a way to get an arbitrary list. Is this do-able in the #mwe example? I am not completely sure when a list is considered completely arbitrary (I thought the list generated by gen_list n was considered arbitrary lol)

[Junyan Xu]

If you have both "gen_list n = x" and "gen_list n = hd :: x" in environment, you can derive a contradiction by rewriting and apply_fun list.length, and then you can derive anything, in particular your goal.

[fkefjlwejlfk]

Junyan Xu said:

If you have both "gen_list n = x" and "gen_list n = hd :: x" in environment, you can derive a contradiction by rewriting and apply_fun list.length, and then you can derive anything, in particular your goal.

I mean we have gen_list n = hd :: x in our environment but we have to proof the goal gen_list n = x

[Mario Carneiro]

@fkefjlwejlfk I can't speak to your original non-MWE, but the MWE can be proved thusly:

import data.list.basic

def foo (n : ℕ) : list ℕ -> option ℕ
| (x :: xs) := if x = n then some x else foo xs
| [] := none

def gen_list (n : ℕ) : list ℕ :=  [n + 2] ++ [n+1] ++ [n]

def is_foo_able (n : ℕ) : bool :=
match (foo n (gen_list n)) with
| some _ := tt
| none := ff
end

lemma foo_able (n : ℕ) : (is_foo_able n = tt) -> (foo n (gen_list n)) = some n :=
begin
  unfold is_foo_able,
  cases h : foo n (gen_list n); rintro ⟨⟩,
  revert h,
  simp [foo, gen_list, eq_comm],
end

[Mario Carneiro]

it's not really a proof by induction as Floris said

[Mario Carneiro]

so if this doesn't capture the spirit of the question you should either make a more elaborate MWE or try to sketch what your theorem actually is

[Kevin Buzzard]

lemma foo_able (n : ℕ) : (is_foo_able n = tt) -> (foo n (gen_list n)) = some n :=
by simp [is_foo_able, gen_list, foo]

[Mario Carneiro]

wait a minute...

lemma foo_able (n : ℕ) : foo n (gen_list n) = some n :=
by simp [gen_list, foo]

[Mario Carneiro]

fkefjlwejlfk said:

I am not completely sure when a list is considered completely arbitrary (I thought the list generated by gen_list n was considered arbitrary lol)

Generally we would say that a value is arbitrary if it is a variable in the context. So n is an "arbitrary" natural number in the sense that the theorem can be applied with any particular value of n, but gen_list n is the output of a construction, so not completely arbitrary. (In this case for example we can say that gen_list n always produces a list of length 3, which is clearly not true about every list.)