Re: [isabelle] A bug in chained proof mode



On 11.06.2014 07:03, Eddy Westbrook wrote:
> Hi,
>
> I think I have found a bug in the chained proof mode, that occurs for equality proofs if one of the proof used in the chain is a reflexive proof. As an example, the following proof fails, even though (as far as I understand the chain mode) it should succeed:
>
> lemma chain_bug: "e1 = e2 ⟹ f e1 = f e2"
>  proof -
>    assume eq1: "e1 = e2"
>    have "f e1 = f e2" by (rule arg_cong[OF eq1])
>    also
>    have "f e2 = f e2" by (simp)
>    finally
>    have "f e1 = f e2".
>  qed
This is intended behaviour (although I cannot find it in the
documentation right now):

  
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2010-September/msg00058.html

Calculational reasoning not only works with equality, but also with a
lot of other transitivity rules (see the print_trans_rules) for the
currently registered rules. An "also" (or "finally") step applies the
first applicable transitivity rule. If this does not make progress
(i.e., the chained fact before and after is the same), it backtracks and
tries the next applicable rule.

You get notified of this behaviour, if you explicitly request to use the
rule for transitivity of equality:

  assume eq1: "e1 = e2"
  have "f e1 = f e2" by (rule arg_cong[OF eq1])
  also
  have "f e2 = f e2" by (simp)
  finally (trans)
  have "f e1 = f e2".

Gives you:

  Vacuous calculation result: f e1 = f e2
  derived as projection (1) from:
      f e1 = f e2
      f e2 = f e2

at the finally step. A closer look at the output of print_trans_rules
shows the the next applicable rules are

  HOL.back_subst: ?P ?a ⟹ ?a = ?b ⟹ ?P ?b
  HOL.forw_subst: ?a = ?b ⟹ ?P ?b ⟹ ?P ?a

HOL.back_subst produces the same, vacuous result, so finally proceeds to
HOL.forw_subst which then yields "f e1 = f e1" as you observed.
> Although it may seem silly to write a proof that “f e2 = f e2”, the reason it comes up is that the proof is machine-generated, and sometimes it is easier to generate a proof that something equals itself rather than checking explicitly for that fact.

Automatically generating theory sources is fragile, in particular when
using the usual user syntax for terms. Apparently, you can use YXML
syntax for the terms instead. Also, it is possible to directly interact
with the prover using Isabelle/Scala.

  -- Lars




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.