Email Gateway (Oct 11 2021 at 05:55): Email Gateway (Oct 11 2021 at 05:55):From: "Isaac@ecs.vuw.ac.nz" <Isaac@ecs.vuw.ac.nz>
Hello,
I seem to have a fund a bug with induction, but I couldn't work out where I should report this;
Bassically, if I put a function inside a context like this:
context fixes par :: bool begin
function foo :: ‹bool ⇒ bool› where
‹foo True = (∀ j :: bool. par ∧ (par ⟶ foo False))› |
‹foo False = True›
by(auto) termination by(relation ‹measure (λb . if b then 1 else 0)›, auto)
end
The generated "thm foo.induct" is as expected:
((⋀x. ?par ⟹ ?P False) ⟹ ?P True) ⟹ ?P False ⟹ ?P ?a0.0
However if I try and use it with the "induction" method, it breaks:
lemma assumes ‹par› shows ‹foo par val› proof(induction val rule: foo.induct)
This suggests the proof text:
case 1
then show ?case sorry
next
case 2
then show ?case sorry
qed
But that text reports an error on the first "case 1":
proof (state)
goal (2 subgoals):
1. (⋀x. ?par ⟹ foo par False) ⟹ foo par True
2. foo par False
Illegal schematic variable(s) in case "1"⌂
A simple workaround is to use "proof(induction val rule: foo.induct[of par])", and everything works as expected:
proof (state)
goal (2 subgoals):
1. (⋀x. par ⟹ foo par False) ⟹ foo par True
2. foo par False
And the proof goes through (after replacing "sorry" with "by (auto)")
As an asside, the reason I have my function in a context to begin with is so that it dosen't put "⋀par" arround each case, which would break my proof, because each step dosn't hold for each "par", but rather the specific one i've assumed to be true!
Email Gateway (Oct 11 2021 at 09:35):From: Thomas Sewell <tals4@cam.ac.uk>
It's not a bug, in that sense. The theorem you're trying to use isn't the usual shape for an induction rule, and it's reporting that as best it can.
Exporting a theorem out of a context, in general, changes its shape, although typically not much. There's no guarantee that induction-shaped rules are exported to induction-shaped rules, etc. Since you've now left an anonymous context and there's no way to return, or get access to foo.induct by any other name, it might seem confusing that foo.induct is not an induction rule, but it's just a consequence of the steps that have been taken.
You've written a postscript in which you explain your reasoning for using a context, which looks like it boils down to saying that some other approach wasn't working. I suspect you should rewind and try other fixes to your original induction problem.
Good luck with it,
Thomas.
Email Gateway (Oct 11 2021 at 16:11):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Hi Isaac,
The generated induction rule depends on the context parameter ?par and you have to tell
the induction method how it is supposed to be instantiated. That's what the "taking"
option is good for:
proof(induction val taking: par rule: foo.induct)
This is typical for definitions inside a context, be them fun(ction) or (co)inductive(_set).
As an asside, the reason I have my function in a context to begin with is so that it
dosen't put "⋀par" arround each case, which would break my proof, because each step dosn't
hold for each "par", but rather the specific one i've assumed to be true!
Right. That's the reason why I often put a function definition into an anonymous context.
There's also an alternative where you explicitly specify the desired instantiation upon
each induction call:
function foo :: ‹bool ⇒ bool ⇒ bool› where
‹foo par True = (∀ j :: bool. par ∧ (par ⟶ foo par False))› |
‹foo par False = True›
by(auto) termination by(relation ‹measure (λ(_, b). if b then 1 else 0)›, auto)
lemma assumes ‹par› shows ‹foo par val›
proof(induction par'≡"par" val rule: foo.induct)
For induction, the usability is about the same. The difference comes with the .cases
rule where you don't have to instantiate "par" in the version with the context.
Hope this helps,
Andreas
Last updated: Jul 15 2022 at 23:21 UTC