Email Gateway (Aug 18 2022 at 12:14): Email Gateway (Aug 18 2022 at 12:14):From: Duncan Higgins <mail@duncan-higgins.co.uk>
This is my first post to the list, so firstly, a big thank you to Larry,
Tobias and everyone else involved for producing such a powerful, useful and
openly available tool.
At the moment, I'm having trouble understanding a particular aspect of
Isabelle's behaviour. I've managed to reduce the problem down to this
trivial example.
Suppose I define the following type:
datatype t = T;
What I don't understand is that I am able to prove the following lemma using
case_tac:
lemma hd_t_list_equals_T : "hd xs = T"
by ( case_tac "hd xs", simp )
With this lemma I can then go on to prove things like:
lemma "hd [] = T"
by ( simp add : hd_t_list_equals_T )
As far as I know, this behaviour only occurs with case expressions and
functions defined using pattern matching, that don't provide an exhaustive
list of matches, or functions that explicitly use the 'arbitrary' constant
as a result. This behaviour allows me to generate Standard ML code that I
think I have proved to be correct, but which actually results in a Match
exception when run.
I guess what I was expecting to see was something like:
lemma hd_t_list_equals_T : "hd xs = T";
apply ( case_tac "hd xs",simp );
proof (prove): step 0
goal (1 subgoal):
which would then be unsolvable.
If anyone is able to give me some guidance on this, I'd very much appreciate
it.
Duncan.
Email Gateway (Aug 18 2022 at 12:15):From: Makarius <makarius@sketis.net>
Since datatype t is singleton, every expression of that type is
mathematically equal to T. It does not matter how other functions, even
seemingly ``partial'' ones get involved.
Just two side notes on proofs by cases/simp:
- case_tac (and any other foo_tac) is only needed when referring
implicitly to hidden parameters of the goal state; when eliminating
expressions that are visible in the proof text you can use plain
"cases" instead
- The Isar command 'by' takes two method arguments: an initial method to
split up the problem, and an (optional) terminal method to solve the
remaining situation.
So the canonical Isar one-liner for the above reasoning looks like this:
lemma "x = T" by (cases x) simp
To solve several goals in the terminal step, methods "simp_all" and "auto"
are quite handy. In this particular case, the terminal step is by
assumption, which is already implicit in the structure of Isar proofs, so
you can actually write it without the terminal method:
lemma "x = T" by (cases x)
Makarius
Email Gateway (Aug 18 2022 at 12:15):From: Amine Chaieb <chaieb@in.tum.de>
Hi Duncan,
Duncan Higgins wrote:
I don't see why this behaviour should
be expected. You perform case distinction on "hd xs" which is of type t,
then the cases you get should only involve the constructors of type t,
i.e. only the case T. Probably you meant to perform case distinction on
xs (empty list, or consed list).
The last goal is provable in this case, since any element of type t is
HOL-equal to T and hence hd (x#xsa) = x = T.
Amine.
Email Gateway (Aug 18 2022 at 12:15):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Duncan,
Note that code generation only guarantees partial correctness. So, if
(!) under code generation a term t evaluates to t', "t = t'" is
derivable in the logic. Raising a Match exception is still "correct"
and that sense though somehow unsatisfactory.
Hope this helps
Florian
florian.haftmann.vcf
signature.asc
Last updated: May 03 2024 at 12:27 UTC