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.
> Best,
> Andreas
> 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 MHonArc.