Email Gateway (Aug 22 2022 at 12:19): Email Gateway (Aug 22 2022 at 12:19):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
I was surprised by this, and I was wondering if it is supposed to be able to happen.
I have the following lemma:
lemma bij_betw_Arr_arr:
shows "bij_betw Some (Collect Arr) (Collect C.arr)"
I can prove it in two ways:
proof (intro bij_betwI)
show "Some ∈ Collect Arr → Collect C.arr" using arr_char by auto
show "the ∈ Collect C.arr → Collect Arr" using arr_char by auto
show "⋀x. x ∈ Collect Arr ⟹ the (Some x) = x" by auto
show "⋀y. y ∈ Collect C.arr ⟹ Some (the y) = y" using arr_char by auto
qed (* Succeeds *)
using arr_char
by (smt bij_betwI' mem_Collect_eq option.collapse option.distinct(1) option.sel)
(* Succeeds *)
However, the following fails:
apply (intro bij_betwI) using arr_char apply auto (* subgoal appears false *)
try (* Nitpick produces counterexample *)
For some reason, I had in my mind that auto should not produce false subgoals from
provable goals.
By the way, the lemma occurs in a locale context, but I have elsewhere shown the
locale consistent by exhibiting a concrete interpretation. So it is not the case
that the locale assumptions are inconsistent.
- Gene Stark
Email Gateway (Aug 22 2022 at 12:19):From: Manuel Eberl <eberlm@in.tum.de>
In my experience, this is uncommon, but it does happen, and to my
knowledge, this is perfectly normal.
I did not look at your example (the definitions of Arr etc. are missing,
if I see it correctly), but my guess would be that in this case, the
problem is with schematic variables. Applying "existential" rules (like
exI) introduces schematic variable into the goals, and at some point,
you have to decide how to instantiate them. If "auto" instantiates one
of these schematic variables incorrectly, you may well end up with
something unprovable.
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 12:19):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Eugene,
It is normal behaviour that auto transforms a provable goal into something unprovable.
This happens particularly often if (1) you have declared a rule as safe (intro!, elim!,
dest!) which is actually not safe or (2) your subgoals contain schematic variables (?x).
The latter may be the reason in your case because the "intro bij_betwI" introduces the
schematic variable ?g in your goal state.
Best,
Andreas
Email Gateway (Aug 22 2022 at 12:19):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
I wouldn't be surprised if the resulting subgoal was simply unprovable.
What I am surprised about is the fact that it is false. But I suppose
that an incorrect instantiation of a schematic variable could produce
this behavior. In my limited mind's eye view of how theorem provers work,
I was assuming that the instances would be generated by unification
during resolution or something, which would not reduce true goals to
false (not merely unprovable) subgoals.
- Gene Stark
Last updated: Apr 23 2024 at 16:19 UTC