Email Gateway (Aug 18 2022 at 20:27): Email Gateway (Aug 18 2022 at 20:27):From: Patrick Michel <uni@pbmichel.de>
Hi!
I am working with a five-way mutual recursive set of datatypes, that have a combined count of 27 constructors. For induction proofs over these datatypes this means proving 27 cases at minimum, sometimes more, as I often have multiple properties to prove for one of the types at once.
Many of these proofs can be done "by (induct v and p and d and r and l) auto", provided I have good lemmas and auto doesn't choke.
In other proofs I cam fine with listing all the cases and doing the "proof (induct v and p and d and r and l)", as many cases need different tactics.
What I am worried about are the cases in between. Sometimes there really are only three interesting cases, the rest works "by auto". If auto doesn't choke on these three, I can do the proofs in apply style of course, but I try to avoid apply proofs. So with "proof" these proofs look like this:
proof (induct v and p and d and r and l)
case A: … next
case B: … next
case C: … next
case rest1 thus ?case by auto next
case rest2 thus ?case by auto next
case rest3 thus ?case by auto next
…
qed
Where "restX" goes up to 27, as said, or even worse these cases can have sub cases, etc. pp.
The same situation arises with induction theorems from complex functions that match more than one parameter. The way Isabelle disambiguates the equations is to unfold all combinations. In a recent proof I had to proof the cases 1 to 7, 8_1 to 8_3 and 9_1 to 9_27. Thereof only 1 to 8_3 where interesting and were followed by 27 lines of boilerplate cases :-)
Now I know some possible ways to get out of this mess:
1) pick another induction scheme
2) if necessary, define one via a terminating function
3) in the case of the function example above: change the definition by avoiding to match another parameter (which can complicate things and in general makes the function harder to read)
4) find more lemmas so the proof works "by (induct v and p and d and r and l) auto" again, or something comparable in size
In the past weeks, however, I found myself in several situation where I could not come up with a good solution.
Which brings me to my original point :-D
I would love to just rewrite the above proof to something like:
proof (induct v and p and d and r and l)
case A: … next
case B: … next
case C: … next
remaining_cases by auto
qed
Where "remaining_cases" presents me with the exact proof state I see after the last next. I.e., I can pick all the "cherries" from the cases, proof them nicely, and dispose of the rest.
That would be incredibly useful to me.
So has this been considered? Is it easy/hard to implement? Is it already possible and I missed it?
Thanks in advance,
Patrick Michel
Software Technology Group
University of Kaiserslautern, Germany
Email Gateway (Aug 18 2022 at 20:28):From: Brian Huffman <huffman@in.tum.de>
Hi Patrick,
I believe that you are looking for the following pattern:
proof (induct v and p and d and r and l)
case A: … next
case B: … next
case C: … next
qed auto
That is, you give a final proof method after "qed" to solve the remaining cases.
Email Gateway (Aug 18 2022 at 20:28):From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear Patrick,
Then just do it :-)
proof (induct v and p and d and r and l)
case A: … next
case B: … next
case C: … next
qed auto (* solves remaining cases *)
Hope this helps,
René
Last updated: Apr 19 2024 at 16:20 UTC