Stream: Beginner Questions

Topic: how to adjust inductive hypothesis

ee (Apr 17 2024 at 10:06):

This is all going to sound very vague but I am using a lot of functions and definitions I defined that are hard for others to make sense of, so I'll try my best to abstract the situation.
I'm trying to prove that given 2 lists that are finite,

P l1 l2 ==> Q l1 l2

using a lemma that states

lemma1 : P [h1] [h2] ==> Q l1 l2

by doing induction on the structure of the lists(using the regular list induction doesn't work so I defined my own induction hypothesis. The problem is that, Q is an existential quantifier, so when I use the lemma, I obtain two new lists, say n1 n2, on which I'd like to use my induction hypothesis on , but my induction hypothesis is constrained to using l1 l2 only. Ideally I'd like to use lemma1 to show Q for all elements of l1 l2, then obtain the lists for those, use my induction hypothesis on all those as well and so on and so forth. I'm not sure if I can do this or if I should find a totally new approach or what.
TIA

Yong Kiam (Apr 18 2024 at 02:17):

in lemma1 what's the relationship of h1 h2 to l1 l2 ?

did you mean P [h1] [h2] ==> Q [h1] [h2] ? if so, if looks like you are defining something that should use list_all2?

also, maybe adding arbitrary: l1 l2 to your induction would help?

Mathias Fleury (Apr 18 2024 at 05:58):

or using list_all2_induct

Mathias Fleury (Apr 18 2024 at 06:01):

From your description, this sounds like you are trying to prove:

lemma
  assumes ‹list_all2 P x y› ‹Q [] [] []›
    ‹⋀a b x y c d. Q [x] a b ⟹ Q y c d ⟹ Q (x#y) c d›
  assumes ‹⋀x y. P x y ⟹ ∃a b. Q [x] a b›
  shows ‹∃a b. Q x a b›
  using assms
  by (induction rule: list_all2_induct)
    fastforce+

Mathias Fleury (Apr 18 2024 at 06:02):

But: I totally fail to see what you tried and that did not work.

Mathias Fleury (Apr 18 2024 at 06:02):

Even if you do not know list_all2_induct, a bit of isar + induction on x + arbitrary: y should be enough…

Mathias Fleury (Apr 18 2024 at 06:04):

I do enjoy receiving ideas for homework for my students however…

ee (Apr 19 2024 at 13:16):

Yong Kiam said:

in lemma1 what's the relationship of h1 h2 to l1 l2 ?

did you mean P [h1] [h2] ==> Q [h1] [h2] ? if so, if looks like you are defining something that should use list_all2?

also, maybe adding arbitrary: l1 l2 to your induction would help?

sorry about the late response. P [h1] [h2] ==> Q [h1] [h2] is what I meant indeed.
Question about the arbitraries, when I do arbitrary: l1 l2 and do the induction, I lose the structure of the list in the induction, what I'm trying to say is

  proof(induct l1 arbitrary: l1 l2 rule: ind1)
    case (sing x)
    then show ?case sorry
  next
    case (trip x f y)
    have "P l1 l2" sorry

I do this, but it forgets that in this case l1 = trip x f y and then I can't have "P (trip x f y ) l2 ", which I need to do the proof properly(actually doing "arbitrary: l1 l2" enables me to rpove anything w/o using any of the lemmas I want to use :upside_down:) .But if I only do " proof(induct l1 arbitrary: l2 rule: ind1)", the induction hypothesis is too tight for me to use with the new lists I obtain from the existential quantification

ee (Apr 19 2024 at 13:30):

Mathias Fleury said:

But: I totally fail to see what you tried and that did not work.

This is my main problem, I think. I tried defining a few other induction theorems yet they either never work from the beginning or run into similar issues.
https://isabelle.zulipchat.com/#narrow/stream/238552-Beginner-Questions/topic/how.20to.20adjust.20inductive.20hypothesis/near/434360661

Also, if you have a class teaching Isabelle, or uses it heavily and it's open to participation by others, I'm super interested :eyes:

Mathias Fleury (Apr 19 2024 at 13:51):

ee said:

Yong Kiam said:

in lemma1 what's the relationship of h1 h2 to l1 l2 ?

did you mean P [h1] [h2] ==> Q [h1] [h2] ? if so, if looks like you are defining something that should use list_all2?

also, maybe adding arbitrary: l1 l2 to your induction would help?

sorry about the late response. P [h1] [h2] ==> Q [h1] [h2] is what I meant indeed.
Question about the arbitraries, when I do arbitrary: l1 l2 and do the induction, I lose the structure of the list in the induction, what I'm trying to say is

  proof(induct l1 arbitrary: l1 l2 rule: ind1)
    case (sing x)
    then show ?case sorry
  next
    case (trip x f y)
    have "P l1 l2" sorry

I do this, but it forgets that in this case l1 = trip x f y and then I can't have "P (trip x f y ) l2 ", which I need to do the proof properly(actually doing "arbitrary: l1 l2" enables me to rpove anything w/o using any of the lemmas I want to use :upside_down:) .But if I only do " proof(induct l1 arbitrary: l2 rule: ind1)", the induction hypothesis is too tight for me to use with the new lists I obtain from the existential quantification

do not do induction on a variable and have that variable as arbitrary at the same time…

Mathias Fleury (Apr 19 2024 at 13:53):

(it makes not much sense from a logical point of view)

Mathias Fleury (Apr 19 2024 at 13:57):

without the actual definition it is very hard to see what is going wrong… If the proof is simply "for each element, we pick the corresponding one given by the existential in Q", then it is easy.

Mathias Fleury (Apr 19 2024 at 13:58):

As you are describing it, "use with the new lists I obtain from the existential quantification" does not apply since you are doing induction over the arguments of P and the existencial is only for Q…

Last updated: May 07 2024 at 01:07 UTC