Re: [isabelle] "apply auto" transforms provable statement to something false?

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 MHonArc.