Stream: Beginner Questions

Topic: using/unfolding assms

Salvatore Francesco Rossetta (Apr 10 2024 at 15:58):

Hi, I did this question in previous thread but it got lost. I have an induction proof in which one subgoal (0) is working if i write only using assms , while the other subgoal (n) is working only for unfolding assms, both do not work if I put the other way. Is there a way I can solve this?

Yong Kiam (Apr 11 2024 at 02:15):

do you mean

using assms
proof (induction)

versus:

unfolding assms
proof (induction)

If that's the case, then I'm afraid you have to stick to one (probably the former)

otherwise I assume you may be doing something like:

apply (induction)
using/unfolding assms FOO

in that case, you can try:

apply (induction)
subgoal using assms by ...
unfolding assms ...

Mathias Fleury (Apr 11 2024 at 04:38):

using assms(6-) unfolding assms(1-5)

Mathias Fleury (Apr 11 2024 at 04:38):

using assms and unfolding assms are very different for non definition

Mathias Fleury (Apr 11 2024 at 04:40):

Consider:

lemma
   defines "q == f n"
   assumes "P n"
   shows "Q q n"

when doing induction without unfolding the assumptions, you are going to need arbitrary: q otherwise the q is fixed across the subgoals

Salvatore Francesco Rossetta (Apr 11 2024 at 05:26):

Yong Kiam said:

do you mean

using assms
proof (induction)

versus:

unfolding assms
proof (induction)

If that's the case, then I'm afraid you have to stick to one (probably the former)

otherwise I assume you may be doing something like:

apply (induction)
using/unfolding assms FOO

in that case, you can try:

apply (induction)
subgoal using assms by ...
unfolding assms ...

This is the case

  using/unfolding assms
  apply (induction rec rule:loop_o.induct)
  subgoal for r
    apply (auto split: if_splits simp del: assign_seats.simps)
    done
    apply (auto simp: Let_def split: if_splits simp del: assign_seats.simps)
    done

So I think I am in the second case you said, right? I tried this but it does not work

 apply (induction rec rule:loop_o.induct)
  subgoal for r
    unfolding assms apply (auto split: if_splits simp del: assign_seats.simps)
    done
    using assms apply (auto simp: Let_def split: if_splits simp del: assign_seats.simps)
    done

Moreover, the case not working (if I understood correctly) is this one

  "ns r = 0  ⟹ loop_o r = r"

so if I write in the assumptions P r it should work, so this subcase actually only needs one assms. But if I write
using assms(1) unfolding assms(2-) then the second case also is looking for an unfolded assms(1) (i can see it in the error message).

Yong Kiam (Apr 11 2024 at 05:30):

as @Mathias Fleury said, using and unfolding is very different, especially when you are using it BEFORE your induction

I would say that DO NOT USE THIS:

unfolding assms
proof (induction ...)

USE THIS:

using assms
proof (induction ...)

and then fix your proof as needed

(edit: this is assuming your assms are needed in the induction, you can also choose only some of them that are relevant)

Salvatore Francesco Rossetta (Apr 11 2024 at 05:39):

Yes, indeed I noticed that only one assms is really needed and creating the conflict. So it is something even simpler, because now I have

assumes  "..."
shows "..."
  using/unfolding assms(1)
  apply (induction rec rule:loop_o.induct)
  subgoal for r
    apply (auto split: if_splits simp del: assign_seats.simps)
    done
    apply (auto simp: Let_def split: if_splits simp del: assign_seats.simps)
    done

As you said, I will use using assms and not unfolding. But I do not understand, how should I fix my proof then? Can't I unfold this only assms only in the second subgoal?

Yong Kiam (Apr 11 2024 at 05:41):

it depends on what you need in the second goal, probably it should be

unfolding ... apply (...)

you will need to pick the correct name to unfold if it is from the inductive hypothesis (or use a structured proof)

Salvatore Francesco Rossetta (Apr 11 2024 at 06:03):

I tried writing unfolding ... apply (...) and I get a failed subgoal

goal (1 subgoal):
 1. 0 < ns r ⟹
    (sl (assign_seats r) ! i2
     ≤ sl (assign_seats r) ! i1 ⟹
     sl (loop_o (assign_seats r)) ! i2
     ≤ sl (loop_o (assign_seats r)) ! i1) ⟹
    sl r ! i2 ≤ sl r ! i1 ⟹
    sl (loop_o (assign_seats r)) ! i2
    ≤ sl (loop_o (assign_seats r)) ! i1

The problem is the mismatch between sl r ! i2 ≤ sl r ! i1 and sl (assign_seats r) ! i2 ≤ sl (assign_seats r) ! i1, right? But with a lemma sl r ! i2 ≤ sl r ! i1 ⟹ sl (assign_seats r) ! i2 ≤ sl (assign_seats r) ! i1 it should work?

Yong Kiam (Apr 11 2024 at 06:05):

I don't really know your problem at hand, so I don't know the answer... but you should try it I suppose..

or maybe just use sledgehammer to see if it finds anything?

edit: your proposed lemma looks reasonable for solving the goal (not sure if it is true for your definition)

Salvatore Francesco Rossetta (Apr 11 2024 at 06:13):

I have the lemma, it is

lemma a_s_c:
  fixes "..."
assumes
  /* other assms */
  "sl rec ! i1 ≥ sl rec ! i2"
shows "sl (assign_seats rec) ! i1 ≥
       sl (assign_seats rec) ! i2"

To use this lemma in my induction proof, I have to write add other assms in my first theorem, right?

Yong Kiam (Apr 11 2024 at 06:14):

it depends on what they are... you should include any necessary ones, yes, but anything you can prove within the context of your previously mentioned subgoal, no

Mathias Fleury (Apr 11 2024 at 06:28):

I would like to remind that:

lemma
  fixes n f
   defines "q == f n"
   assumes "P n"
   shows "Q q n"
  thm assms(1)
(*q = f n*)

Mathias Fleury (Apr 11 2024 at 06:31):

assms(1) is not the first assumption

Salvatore Francesco Rossetta (Apr 11 2024 at 06:38):

Mathias Fleury said:

assms(1) is not the first assumption

I know, I have no defines

Salvatore Francesco Rossetta (Apr 11 2024 at 07:17):

Yong Kiam said:

it depends on what they are... you should include any necessary ones, yes, but anything you can prove within the context of your previously mentioned subgoal, no

I added lemma and assumptions and I have

 1. 0 < ns r ⟹
    ... ⟹
    sl (loop_o (assign_seats r)) ! index (p r) party2
    ≤ sl (loop_o (assign_seats r)) ! index (p r) party1

Why (p r) is not written as (p (assign_seats r))?
Adding assms p rec = p (assign_seats rec) as @Mathias Fleury suggested actually makes things worse because then my other assumptions start to unfold "too much".

P.S: trying to cut the problem at the beginning: if I know that this parameter is never changing, putting it outside of this structure but just as a normal parameter should make the lemma work?

Salvatore Francesco Rossetta (Apr 11 2024 at 07:33):

Update: I put this parameter outside the structure, having now

shows "sl (loop_o p rec) ! i1 ≥
       sl (loop_o p rec) ! i2"

Using the rule loop_o.induct, how do I specify that the induction should be only on rec and p should be fixed?

Salvatore Francesco Rossetta (Apr 11 2024 at 08:23):

Update 2 (I am really trying): The first case, ns r > 0 seems to work and I am trying the other case ns r = 0 by hand.

  apply (induction rec rule:loop_o.induct)
  subgoal for r parties
    apply (auto simp: Let_def split: if_splits simp del: assign_seats.simps)
    done
  subgoal for r parties
    proof - have "ns r = 0" using assms by simp
    done

Why I cannot retrieve "ns r = 0" if it is the subgoal I am in?

Yong Kiam (Apr 11 2024 at 09:23):

sorry it is very hard to see what your problem is without the code or a minimal example....

what do you mean cannot retriev ns r = 0?

Salvatore Francesco Rossetta (Apr 11 2024 at 09:40):

Yong Kiam said:

sorry it is very hard to see what your problem is without the code or a minimal example....

what do you mean cannot retriev ns r = 0?

You are right, I am sorry. This is the function

function loop_o ::
  "'b list ⇒ ('a::linorder, 'b) Divisor_Module ⇒ ('a::linorder, 'b) Divisor_Module"
  where
  "ns r > 0 ⟹ loop_o p r = loop_o p (assign_seats p r)" |
  "ns r = 0  ⟹ loop_o p r = r"

The first subgoal is working, the second not. I try to do it by hand

  apply (induction rec rule:loop_o.induct)
  subgoal for r parties (working)
    apply (auto simp: Let_def split: if_splits simp del: assign_seats.simps)
    done
  subgoal for r parties <----
    proof - have "ns r = 0" using assms by simp
    done

I cannot have "ns r = 0" but why if I am in this subgoal? Is it something with variables that I am forgetting?
Because when I put the cursor on the subgoal I see

goal (1 subgoal):
 1. ns r = 0 ⟹ ....

I hope I was clear

Salvatore Francesco Rossetta (Apr 11 2024 at 09:58):

PS: if I was not clear, here's the code

Votes.thy

Yong Kiam (Apr 11 2024 at 11:02):

you should write assume "ns r = 0" ... show ... if you want to use a structured proof

Salvatore Francesco Rossetta (Apr 11 2024 at 11:16):

Yong Kiam said:

you should write assume "ns r = 0" ... show ... if you want to use a structured proof

Thank you, I wrote it but I understood that...

Salvatore Francesco Rossetta (Apr 11 2024 at 11:38):

... the problem boils down to: one subgoal needs assms to work, the other subgoal does not work with assms (but it does without). I can not tell the second case not to consider the assumption? It's weird that there is no syntax to solve this

Mathias Fleury (Apr 11 2024 at 13:40):

You can skip assumptions

Mathias Fleury (Apr 11 2024 at 13:40):

subgoal premises p for r
   using p(1,3,5,19) ...

(for Isar this is obvious)

Yong Kiam (Apr 11 2024 at 13:48):

I finally took a look at your Votes.thy the problem is this:

currently it does not have any assms before apply (induction ...)

I recommend that you look very carefully at what goals you get with and without using assms

Yong Kiam (Apr 11 2024 at 13:54):

to make sure you understand the difference, perhaps look at this simpler example:

lemma ls_induction_1:
  assumes "P xs"
  shows "Q (xs::'a list)"
  apply (induction xs)
  oops

lemma ls_induction_2:
  assumes "P xs"
  shows "Q (xs::'a list)"
  using assms
  apply (induction xs)
  oops

have a look at the difference between the two goals you get

in ls_induction_1, the P xs assumption will not help you at all in the induction because the xs is not quantified (see the parallel with your theorem)

in ls_induction_2, you get P (x # xs) as an assumption, but in return you need to prove P for an appropriate list in the IH

Yong Kiam (Apr 11 2024 at 13:57):

in other words, these are two different inductions that you are trying to do in your proof... it's not as simple as "one works with using assms" and one doesn't -- you need to know which induction you're trying to do

Salvatore Francesco Rossetta (Apr 11 2024 at 13:59):

Yong Kiam said:

in other words, these are two different inductions that you are trying to do in your proof... it's not as simple as "one works with using assms" and one doesn't -- you need to know which induction you're trying to do

Your example was clear, I think I understood. So how should I proceed?

Yong Kiam (Apr 11 2024 at 14:02):

well... you need to know what inductive argument you are making here....

at minimum, I believe every assumption that mentions parties and rec should be inside the induction i.e., you should using assms(...) where (...) refers to the assumptions involving those two

Yong Kiam (Apr 11 2024 at 14:04):

a third possibility which I should have mentioned above:

lemma ls_induction_3:
  assumes "⋀xs. P xs"
  shows "Q (xs::'a list)"
  apply (induction xs)
  oops

this is another way you might need to setup your lemma ... do you want to assume P FORALL xs or only the xs in the conclusion?

Salvatore Francesco Rossetta (Apr 11 2024 at 14:12):

Yong Kiam said:

well... you need to know what inductive argument you are making here....

at minimum, I believe every assumption that mentions parties and rec should be inside the induction i.e., you should using assms(...) where (...) refers to the assumptions involving those two

Well, my idea was induction over rec, also I I thought it was needed one assumption (the one in the file I uploaded here), just because it was giving me "no subgoals", but maybe I should add also all the assumptions from the previous lemma that I want to use during the induction?

Yong Kiam (Apr 11 2024 at 14:15):

well yes, but as you can see from ls_induction_2 adding more assumptions to the induction means that you also need to prove more things before you can apply an induction hypothesis

Salvatore Francesco Rossetta (Apr 11 2024 at 14:27):

Yong Kiam said:

well yes, but as you can see from ls_induction_2 adding more assumptions to the induction means that you also need to prove more things before you can apply an induction hypothesis

Of course, so always referencing ls_induction_2, knowing P(x # xs) I should prove P(x), so I get as implication Q(x) and therefore Q (x # xs)

Yong Kiam (Apr 11 2024 at 14:28):

yes, but you need to figure out the analogous argument for the result you want here

Salvatore Francesco Rossetta (Apr 11 2024 at 14:43):

Yong Kiam said:

yes, but you need to figure out the analogous argument for the result you want here

Well, I have a first lemma that is proving one "time" case A(x) ⟹ P(x). Then I want to prove a second lemma that is a loop, so maybe something like A (... ( A (x) ) ) ⟹ P(x)? And at this point maybe I need a quantifier on the first lemma, like ∀x. A(x) ⟹ P(x)? I don't know if what I wrote makes sense

Yong Kiam (Apr 11 2024 at 14:46):

your first lemma is already implicitly quantified over x

Yong Kiam (Apr 11 2024 at 14:46):

what I mean is that for the second lemma, you need to figure out what the induction argument looks like

Salvatore Francesco Rossetta (Apr 11 2024 at 14:52):

Yong Kiam said:

what I mean is that for the second lemma, you need to figure out what the induction argument looks like

Well, I think it makes sense to be ns r because it is a nat constantly decreasing or maybe also the list of parties but I think it would be harder

Yong Kiam (Apr 11 2024 at 14:58):

with loop_o.induct you're using the induction principle for loop_o

it's a similar idea: you need to figure out what assumptions you can/cannot add to the induction for it to go through

it's always a fine balance between finding just the right induction

Yong Kiam (Apr 11 2024 at 15:01):

one thing you can try (not sure it works), do:

using assms
apply (induction ....)

in the case that fails, figure out what goes wrong when you try to apply the induction hypothesis

Yong Kiam (Apr 11 2024 at 15:13):

and one more comment: if you want to try this above, I recommend exploring the proof in a structured way instead of using an apply-style proof... it'll be much clearer where the proof is going wrong

Salvatore Francesco Rossetta (Apr 11 2024 at 15:47):

Yong Kiam said:

and one more comment: if you want to try this above, I recommend exploring the proof in a structured way instead of using an apply-style proof... it'll be much clearer where the proof is going wrong

Yes, I just thought that being the loop a simple n times application of a function that has a property, then it would be easy to use the induction within the function itself.
So since my induction argument is decreasing, is there any way isabelle allows me to induct "in reverse"?

Yong Kiam (Apr 12 2024 at 01:18):

I'm not sure what you mean here, but this just sounds like regular induction to me... I think loop_o.induct is what you want here (which you're already using)

Last updated: May 06 2024 at 12:29 UTC