Email Gateway (Aug 18 2022 at 15:16): Email Gateway (Aug 18 2022 at 15:16):From: Andrei Borac <zerosum42@gmail.com>
Ok, so I have a kind of "two-dimensional" induction that I'm trying to
do. Here is a stripped-down example that illustrates the difficulty:
consts p :: "nat => nat => bool"
lemma base: "(p 0 y)"
sorry (* lemma base: p 0 ?y *)
lemma meta: "(p row col) ==> (p (row + 1) any_col)"
sorry (* lemma meta: p ?row ?col ==> p (?row + 1) ?any_col *)
lemma half: "(!!col. (p row col)) ==> (p (row + 1) any_col)"
sorry (* lemma half: (!!col. p ?row col) ==> p (?row + 1) ?any_col *)
lemma desired: "(p row col)"
The base cases and inductive steps are simply "provided" using "sorry"
to keep the example simple. meta and half are basically the same thing
except in meta "col" is a meta-whatsitcalled or maybe
schematic-whatsitcalled. Now, after 3 hours of trial and error, I have
succeeded in providing the desired lemma:
lemma helper: "!!row. (!!col. p row col) ==> p (Suc row) col"
apply(drule half[where any_col=col])
apply(simp)
done (* lemma helper: (!!col. p ?row col) ==> p (Suc ?row) ?col *)
lemma desired: "(p row col)"
apply(induct row arbitrary: col)
apply(simp add: base)
apply(simp add: helper)
done (* lemma desired: p ?row ?col *)
So, how is this kind of thing -supposed- to be done? Is there a way to
apply something in the main proof to get this done without a helper
lemma? I was thinking the obvious thing is change it to subgoal_tac,
but so far all my attempts have been unsuccessful. Plus, it seems like
there should be an even better way.
Thanks,
-Andrei
Email Gateway (Aug 18 2022 at 15:17):From: Andrei Borac <zerosum42@gmail.com>
Ok, second attempt; I have found a more accurate way to represent the
problem. Sorry that the title is incorrect (it's p(some x) from !!x.
p(x)). Anyways, here is what is actually not working:
consts f :: "nat list => nat => nat option"
consts g :: "nat list => nat => nat option"
lemma False
apply(subgoal_tac "
!!context param value.
[| !!param_any.
f context param_any = Some value
==> (case (g context param_any) of None => 0
| Some value_some => value_some) = value;
g context param = None;
f context param = Some value |]
==> value = 0")
defer
Resulting in the first subgoal:
!!context param value.
[| !!param_any.
f context param_any = Some value
==> (case g context param_any of None => 0 | Some
value_some => value_some) = value;
g context param = None; f context param = Some value |]
==> value = 0
where all variables are green. Now it seems like setting "param_any"
to "param" should work. We know that "f" produced something and that
the case of "g" is None, so we should get value = 0, as required.
However, clarsimp will not do it (and I can't seem to be able to split
the option in my apply-style proof). What will work (or why can't it
work ...)?
-Andrei
Email Gateway (Aug 18 2022 at 15:17):From: Tobias Nipkow <nipkow@in.tum.de>
This is how you ca instantiate a !! hypothesis in apply style:
apply(erule_tac x = "<term>" in meta_allE)
Not pretty and not very stable under changes, but it works. I recommend
to use it only for finding a proof but rewrite it at the end (into a
structured proof).
In your case there are alternatives: auto/fastsimp/force solve your goal
automatically; clarsimp is just too weak.
Tobias
Andrei Borac schrieb:
Last updated: Apr 26 2024 at 16:20 UTC