Re: [isabelle] "Illegal schematic variable(s) in case" when using an exported induction rule



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


On 11.10.21 07:54, Isaac at ecs.vuw.ac.nz wrote:
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!




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.