Salvatore Francesco Rossetta (Feb 12 2024 at 21:57): Salvatore Francesco Rossetta (Feb 12 2024 at 21:57):Hi, I am writing a proof by induction with a list.
fun calc_votes :: "'b list ⇒ 'b Profile ⇒'b Votes ⇒ 'b Votes" where
"calc_votes [ ] prof votes = votes" |
"calc_votes (party # parties) prof votes =
calc_votes parties prof (cnt_votes party prof empty_v 0)"
lemma calc_votes_permutation:
fixes
p1 :: "'b Parties" and
p2 ::"'b Parties" and
profl ::"'b Profile" and
votes::"'b Votes"
assumes "p1 <~~> p2"
shows "calc_votes p1 profl votes = calc_votes p2 profl votes"
proof (induction p1)
case Nil
then have "p2 = []" using assms perm_empty_imp by simp
then show ?case by simp
next
case (Cons a p1)
have "calc_votes (a # p1) profl votes =
calc_votes p1 profl (cnt_votes a profl empty_v 0)" by simp
then have "calc_votes (a # p2) profl votes =
calc_votes p2 profl (cnt_votes a profl empty_v 0)" by simp
then obtain v' where "v' = (cnt_votes a profl empty_v 0)" by simp
then have "calc_votes p1 profl v' =
calc_votes p2 profl v'" using assms by simp
then have "calc_votes (a # p1) profl votes =
calc_votes (a # p2) profl votes" by simp
then show ?case by simp
qed
First: Nil case should be trivial but even "p1 = [ ]" using assms by simp does not work. How is this possible if Nil itself is "[ ]" as I read in the documentation?
Second: in Cons, I am stuck on the step where I use v' (I introduced it to make it clearer). I know the induction proof is assuming as true that "calc_votes p1 profl v = calc_votes p2 profl v" , while in the step I have v', which is different. The only solution I could think of brings me to useless unrolling of the recursion. How do I solve this? TIA
Yong Kiam (Feb 13 2024 at 05:52):I don't know for sure without more context, however, your induction doesn't look like it is set up correctly. you probably want the following :
...
using assms
proof (induction p1 arbitrary: p2)
...
which means to use the assumptions p1 <~~> p2 when as part of the predicate instantiating the induction theorem and also to generalize over p2
Mathias Fleury (Feb 13 2024 at 05:55):I really think (also after https://isabelle.zulipchat.com/#narrow/stream/238552-Beginner-Questions/topic/Foldr.20invariant.20on.20permutations/near/419800146) that you should start with an Isabelle tutorial like the prog-prove.
Salvatore Francesco Rossetta (Feb 13 2024 at 07:11):Yong Kiam said:
I don't know for sure without more context, however, your induction doesn't look like it is set up correctly. you probably want the following :
... using assms proof (induction p1 arbitrary: p2) ...which means to use the assumptions
p1 <~~> p2when as part of the predicate instantiating the induction theorem and also to generalize over p2
Thanks, but I had already tried and it did not work.
Mathias Fleury (Feb 13 2024 at 07:14):You are missing the "using assms" before the proof induction
Mathias Fleury (Feb 13 2024 at 07:15):Isabelle's induction method does not work by assuming "p1 = []" but by replacing p1 by [] at all occurrences
Mathias Fleury (Feb 13 2024 at 07:16):and if you forget some occurrences (like not putting the assms), then you cannot prove anything
Salvatore Francesco Rossetta (Feb 13 2024 at 07:17):Mathias Fleury said:
I really think (also after https://isabelle.zulipchat.com/#narrow/stream/238552-Beginner-Questions/topic/Foldr.20invariant.20on.20permutations/near/419800146) that you should start with an Isabelle tutorial like the prog-prove.
I already read the prog-prove but I will try to do some exercises from here, thanks.
Salvatore Francesco Rossetta (Feb 13 2024 at 07:19):Mathias Fleury said:
You are missing the "using assms" before the proof induction
You mean like the example provided by @Yong Kiam , right? I put it, still it does not work.
Mathias Fleury (Feb 13 2024 at 07:20):and what does not work? can you provide an error message?
Mathias Fleury (Feb 13 2024 at 07:25):and if the problem is calc_votes p1 profl v = calc_votes p2 profl v: you have told Isabelle that you want to use the IH at this point
Salvatore Francesco Rossetta (Feb 13 2024 at 07:36):Mathias Fleury said:
and what does not work? can you provide an error message?
Nevermind, I fixed it, thanks
Salvatore Francesco Rossetta (Feb 13 2024 at 07:45):Mathias Fleury said:
and if the problem is
calc_votes p1 profl v = calc_votes p2 profl v: you have told Isabelle that you want to use the IH at this point
It's not working because I am inducting on p1, having (a # p1) but since I am not inducting on p2 I have p2 and not what I actually would need, which is (a # p2). So my induction proof is proving calc_votes (a # p1) ... = calc_votes p2 ... , while I should prove calc_votes (a # p1) ... = calc_votes (a # p2) ... . Maybe I should use some obtain ? I hope I was clear.
Salvatore Francesco Rossetta (Feb 13 2024 at 07:46):Also, I will look in the doc to check if there is some similar case/example.
Yong Kiam (Feb 13 2024 at 08:15):in the inductive case, you will probably need to unfold the assumption a # p_1 <~~> p_2 a little in order to apply the inductive hypothesis
Mathias Fleury (Feb 13 2024 at 08:57):you need to obtain a p_2' such that mset p_2 = mset (a # p_2') yeas
Salvatore Francesco Rossetta (Feb 13 2024 at 12:25):Mathias Fleury said:
you need to obtain a p_2' such that mset p_2 = mset (a # p_2') yeas
Actually p_2 is a list, not a multiset (also because I use permutation operator). Maybe you meant p_2' = mset (a # p_2) and then proving the inductive case on (a # p1) and p_2' (indeed, a # p_2)?
Mathias Fleury (Feb 13 2024 at 12:29):You are getting the induction wrong. You have a p_2 (the list). From this list you could remove the element a. This yields the p_2' I was writing about
Salvatore Francesco Rossetta (Feb 13 2024 at 12:49):Mathias Fleury said:
You are getting the induction wrong. You have a p_2 (the list). From this list you could remove the element a. This yields the p_2' I was writing about
I understand, you mean something like this right?
obtain p2' where "p2 <~~> (a # p2')" using assms by (metis Cons.prems)
Mathias Fleury (Feb 13 2024 at 12:51):I would have written it directly as obtain p2' where "a # p1 <~~> (a # p2')", but yes (this is one transitivity step away from your version)
Yong Kiam (Feb 13 2024 at 13:03):BTW, I'm not sure induction on lists is the best way to prove your goal (as it involves permutation), perhaps you may have better luck with induction on permutations (I don't have Isabelle open at the moment to see what the permutation induction is called)
Mathias Fleury (Feb 13 2024 at 13:14):Or using multisets directly…
Salvatore Francesco Rossetta (Feb 13 2024 at 13:32):I already tried to wrote it with Multisets with fold_mset but I found it a bit hard for my case. I'll try again today then
Mathias Fleury (Feb 13 2024 at 13:39):You can also continue with the current approach… you are not far away from proving this theorem
Mathias Fleury (Feb 13 2024 at 13:39):The real question is probably what comes next
Mathias Fleury (Feb 13 2024 at 13:41):In general, the more complicated your structures are, the more proof you will require. For example, lists are multisets + order on the elements. So it is more complicated. Like here: the p_2' would be remove1 a p_2 compared to p_1 - {#a#}
Salvatore Francesco Rossetta (Feb 13 2024 at 19:46):Mathias Fleury said:
You can also continue with the current approach… you are not far away from proving this theorem
I continued, I got to this point in the proving:
case (Cons a p1)
obtain p2' where "p2 <~~> (a # p2')" using assms by (metis Cons.prems)
then have "(a # p1) <~~> (a # p2')" using assms Cons.prems by auto
then have "calc_votes (a # p1) profl votes =
calc_votes p1 profl (cnt_votes a profl empty_v 0)" using assms by simp
then have "… =
calc_votes p2' profl (cnt_votes a profl empty_v 0)" using assms
by (metis Cons.IH Cons.prems ‹mset p2 = mset (a # p2')› calc_votes.simps(2) cons_perm_imp_perm list.exhaust mset_zero_iff_right)
then have "... = calc_votes (a # p2') profl votes" using assms by simp
then have "... = calc_votes p2 profl votes" by simp
then show ?case by simp
qed
but I cannot do the last step, since p2 is not equal to (a # p2') but it's a permutation. So to do this step I would require exactly the lemma i am proving and I don't know how to do this otherwise.
Yong Kiam (Feb 14 2024 at 01:06):you may need to prove a helper lemma (e.g., something saying you can pull an element from within a list to the front)
alternatively, go for mset or an induction principle for permutations
Salvatore Francesco Rossetta (Feb 14 2024 at 07:07):Yong Kiam said:
you may need to prove a helper lemma (e.g., something saying you can pull an element from within a list to the front)
alternatively, go for
msetor an induction principle for permutations
I don't understand, how would the helper lemma you wrote help my case?
for mset you mean to write the function itself with Multisets? alternatively, do you know where I can find infos about induction on permutations?
Yong Kiam (Feb 14 2024 at 07:16):I'm actually not sure what the appropriate induction is called in Isabelle, maybe someone else could chime in, but this is the induction principle that's used in HOL4:
[PERM_IND] Theorem
⊢ ∀P. P [] [] ∧ (∀x l1 l2. P l1 l2 ⇒ P (x::l1) (x::l2)) ∧
(∀x y l1 l2. P l1 l2 ⇒ P (x::y::l1) (y::x::l2)) ∧
(∀l1 l2 l3. P l1 l2 ∧ P l2 l3 ⇒ P l1 l3) ⇒
∀l1 l2. PERM l1 l2 ⇒ P l1 l2
going for mset as @Mathias Fleury suggested seems like the right way to go to me.
concretely: define another function that works over multisets, prove that your list version is equivalent to the mset version in some adequate way, then the permutation results follow for free
Yutaka Nagashima (Feb 14 2024 at 23:30):Hi @Salvatore Francesco Rossetta .
I am building an induction prover inside Isabelle.
(This might be a bit confusing, but in the video, I refer to it as 'abduction prover' because of the search algorithm I use within the prover. However, it is primarily designed for solving inductive problems.)
https://youtu.be/rXU-lJxP_GI
It might be able to find a proof for you if you're lucky.
You can get the induction prover for Isabelle here: https://github.com/data61/PSL
The tool may not handle the use of assumes very well.
So, it might prefer
prove "(p1 <~~> p2) ==> calc_votes p1 profl votes = calc_votes p2 profl votes"
rather than
assumes "p1 <~~> p2"
prove "calc_votes p1 profl votes = calc_votes p2 profl votes"
Also, please note that it takes a while for this tool to find a proof. Once, I waited for more than 30 minutes before it delivered a proof to me.
Mathias Fleury (Feb 15 2024 at 19:50):Yong Kiam said:
I'm actually not sure what the appropriate induction is called in Isabelle, maybe someone else could chime in, but this is the induction principle that's used in HOL4:
[PERM_IND] Theorem ⊢ ∀P. P [] [] ∧ (∀x l1 l2. P l1 l2 ⇒ P (x::l1) (x::l2)) ∧ (∀x y l1 l2. P l1 l2 ⇒ P (x::y::l1) (y::x::l2)) ∧ (∀l1 l2 l3. P l1 l2 ∧ P l2 l3 ⇒ P l1 l3) ⇒ ∀l1 l2. PERM l1 l2 ⇒ P l1 l2going for
msetas Mathias Fleury suggested seems like the right way to go to me.
concretely: define another function that works over multisets, prove that your list version is equivalent to themsetversion in some adequate way, then the permutation results follow for free
wait actually permutations are defined as multiset equality. I forgot that.
src/HOL/Combinatorics/List_Permutation.thy:abbreviation (input) perm :: \<open>'a list \<Rightarrow> 'a list \<Rightarrow> bool\<close> (infixr \<open><~~>\<close> 50)
src/HOL/Combinatorics/List_Permutation.thy: where \<open>xs <~~> ys \<equiv> mset xs = mset ys\<close>
So we do not have a permutation induction (at least no a builtin one).
Mathias Fleury (Feb 15 2024 at 19:53):Salvatore Francesco Rossetta said:
Mathias Fleury said:
You can also continue with the current approach… you are not far away from proving this theorem
I continued, I got to this point in the proving:
case (Cons a p1) obtain p2' where "p2 <~~> (a # p2')" using assms by (metis Cons.prems) then have "(a # p1) <~~> (a # p2')" using assms Cons.prems by auto then have "calc_votes (a # p1) profl votes = calc_votes p1 profl (cnt_votes a profl empty_v 0)" using assms by simp then have "… = calc_votes p2' profl (cnt_votes a profl empty_v 0)" using assms by (metis Cons.IH Cons.prems ‹mset p2 = mset (a # p2')› calc_votes.simps(2) cons_perm_imp_perm list.exhaust mset_zero_iff_right) then have "... = calc_votes (a # p2') profl votes" using assms by simp then have "... = calc_votes p2 profl votes" by simp then show ?case by simp qedbut I cannot do the last step, since p2 is not equal to (a # p2') but it's a permutation. So to do this step I would require exactly the lemma i am proving and I don't know how to do this otherwise.
Right, so this would mean that you have to generalize your assumptions somehow and change your induction principle. Maybe actually induction on the length of l1?
Mathias Fleury (Feb 15 2024 at 19:54):(BTW I would still like to get the full theory with all the definitions)
Yong Kiam (Feb 16 2024 at 04:16):Mathias Fleury said:
Yong Kiam said:
I'm actually not sure what the appropriate induction is called in Isabelle, maybe someone else could chime in, but this is the induction principle that's used in HOL4:
[PERM_IND] Theorem ⊢ ∀P. P [] [] ∧ (∀x l1 l2. P l1 l2 ⇒ P (x::l1) (x::l2)) ∧ (∀x y l1 l2. P l1 l2 ⇒ P (x::y::l1) (y::x::l2)) ∧ (∀l1 l2 l3. P l1 l2 ∧ P l2 l3 ⇒ P l1 l3) ⇒ ∀l1 l2. PERM l1 l2 ⇒ P l1 l2going for
msetas Mathias Fleury suggested seems like the right way to go to me.
concretely: define another function that works over multisets, prove that your list version is equivalent to themsetversion in some adequate way, then the permutation results follow for freewait actually permutations are defined as multiset equality. I forgot that.
src/HOL/Combinatorics/List_Permutation.thy:abbreviation (input) perm :: \<open>'a list \<Rightarrow> 'a list \<Rightarrow> bool\<close> (infixr \<open><~~>\<close> 50) src/HOL/Combinatorics/List_Permutation.thy: where \<open>xs <~~> ys \<equiv> mset xs = mset ys\<close>So we do not have a permutation induction (at least no a builtin one).
lemma perm_induct:
assumes "P [] []"
assumes "⋀x xs ys. P (x # xs) (x # ys)"
assumes "⋀x y xs ys. P (x # y # xs) (y # x # ys)"
assumes "⋀xs ys zs. P xs ys ⟹ P ys zs ⟹ P xs zs"
shows "mset xs = mset ys ⟹ P xs ys"
proof (induction xs arbitrary: ys)
case Nil
then show ?case
using assms by auto
next
case (Cons x xs)
then show ?case
using assms
by (metis neq_Nil_conv perm_empty2)
qed
Mathias Fleury said:
Right, so this would mean that you have to generalize your assumptions somehow and change your induction principle. Maybe actually induction on the length of
l1?
At this point, if the problem is that my p2 is p2 <~~> a # p2', can't i define it simply as p2 =a # p2' so I can do the last step?
Yong Kiam (Feb 16 2024 at 07:52):I don't get what you mean here, but the point is that p2 does not necessarily start with a, it's a permutation of a # p_1
Yong Kiam (Feb 16 2024 at 07:54):if you want to assume something stronger about p_2, you'll have to use induction on a different (more general) statement, or use a different induction principle, as Mathias mentioned
Mathias Fleury (Feb 16 2024 at 08:19):Salvatore Francesco Rossetta said:
Mathias Fleury said:
Right, so this would mean that you have to generalize your assumptions somehow and change your induction principle. Maybe actually induction on the length of
l1?At this point, if the problem is that my p2 is p2 <~~> a # p2', can't i define it simply as p2 =a # p2' so I can do the last step?
You are doing an induction. You are not allowed to define anything. You get variables and you have to work with them.
Salvatore Francesco Rossetta (Feb 16 2024 at 08:37):Yong Kiam said:
if you want to assume something stronger about
p_2, you'll have to use induction on a different (more general) statement, or use a different induction principle, as Mathias mentioned
Now I get it, to say that p2= a # p2' means this would be proved only with p2 having a as a first element, while I want the more general case, right?
So on a general level, as an idea, I should do induction on length of p1 and in the ≠0 case do some obtain like p1' <~~> a # p1 and same with p2 right? I don't know if I was clear
Yong Kiam (Feb 16 2024 at 10:23):you can do something like this, but I'm not sure it will help you in this case, what about trying to use perm_induct which I wrote above?
Last updated: Apr 28 2024 at 01:11 UTC