Re: [isabelle] BUG in conv.ML: rewr_conv and then_conv fail due to beta-normalization issue



An additional beauty of the Isabelle library is how often you get to build your own primitives because none of the existing ones do what you would expect.

I have this sitting around somewhere:

fun fix_conv conv ct = let
    val thm = conv ct
    val eq = Logic.mk_equals (term_of ct, term_of ct) |> head_of
  in if (term_of (Thm.lhs_of thm) aconv term_of ct)
    then thm
    else thm RS trivial
(Thm.mk_binop (cterm_of (theory_of_cterm ct) eq) ct (Thm.rhs_of thm)) end

That fixes the problem with rewr_conv, so fix_conv Conv.rewr_conv does what you would expect Conv.rewr_conv to do.

Yours,
    Thomas.

On 23/10/12 07:40, Lawrence Paulson wrote:
This module was written long ago for a specific, internal purpose and was never intended for general use, so it's hard to say what is a bug and what isn't. The beauty of conversions is that they are highly modular, so you can write your own primitives that do exactly what you want.

Larry Paulson


On 22 Oct 2012, at 17:45, Peter Lammich<lammich at in.tum.de>  wrote:

Hi,

my understanding of conversions is, that "conv ct" either throws an
exception or returns a theorem of the form "ct == ...". Here is a
minimal example where rewr_conv actually returns a theorem that does not
satisfy this condition, and thus, a subsequent then_conv fails
unexpectedly.


definition "I x \<equiv>  x"
definition "A f x \<equiv>  f x"


ML_val {*
  let
    open Conv

    val cv1 = fun_conv (rewr_conv @{thm I_def})
    val cv2 = rewr_conv (@{thm A_def[symmetric]})
  in
    (cv1 then_conv cv2) @{cterm "I (\<lambda>s::bool. s) True"}
  end

  (*
*** exception THM 0 raised (line 835 of "thm.ML"):
*** transitive: middle term
*** I (\<lambda>s\<Colon>bool. s) True \<equiv>  True
*** True \<equiv>  A (\<lambda>s\<Colon>bool. s) True
  *)

*}


The reason is, that the term after applying cv1 is not beta-reduced, and
cv2 returns a theorem with a beta-reduced left-hand side. The exception
is thrown when then_conv tries to put the two theorems together.

The issue can be observed when instrumenting then_conv, e.g. as attached
to the end of this mail.

I consider this a bug, because it is nowhere documented that the user of
conversions has to take care of beta-normalization manually. My proposal
for solution is as follows:
  What is the status of beta-equality within Isabelle?
    Alternative 1) beta-equivalent terms are considered equal: then_conv
should just work modulo beta-equivalence
    Alternative 2) They are not considered equal on this low-level:
rewr_conv should be forced to return an equal term.

Anyway, if none of the two alternatives is appropriate, the rules for
composing conversions should be CLEANLY documented.

Regards,
  Peter





--------------------------
ML_val {*
let
  open Conv

  (* Instrumenting then_conv to make the reason for the error visible:
*)
  fun (cv1 then_conv cv2) ct =
    let
      val eq1 = cv1 ct;
      val eq2 = cv2 (Thm.rhs_of eq1);
    in
      if Thm.is_reflexive eq1 then eq2
      else if Thm.is_reflexive eq2 then eq1
      else (
        tracing ("RHS1: "^PolyML.makestring (Thm.rhs_of eq1 |>
term_of));
        tracing ("LHS2: "^PolyML.makestring (Thm.lhs_of eq2 |>
term_of));
        Thm.transitive eq1 eq2
      )
    end;
in
  let
    val cv1 = fun_conv (rewr_conv @{thm I_def})
    val cv2 = rewr_conv (@{thm A_def[symmetric]})
  in
    (cv1 then_conv cv2) @{cterm "I (\<lambda>s::bool. s) True"}
  end
end

(* TRACE:

RHS1: Abs ("s", "bool", Bound 0) $ Const ("HOL.True", "bool")

LHS2: Const ("HOL.True", "bool")
*)

*}













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