Re: [isabelle] "apply auto" transforms provable statement to something false?
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
On 01/25/2016 06:28 AM, Andreas Lochbihler wrote:
> 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.
> On 25/01/16 12:02, Eugene W. Stark wrote:
>> 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
This archive was generated by a fusion of
Pipermail (Mailman edition) and