Clever Geek Handbook

Rewriting with non-equality equivalent relations using Isabelle simplification

I would like to use simplification to replace subterms that are not equalities. Instead of a general definition of my problem, I will illustrate this with an example:

Let's say that I have a simple programming language and Hoare logic. Let's say that if, while and sequence operation. Moreover, we have denotation

which gives the designation of the program and hoare P c Q

. Below is an example of a signature in Isabelle / HOL:

(* A simple language and Hoare logic *)
typedecl program
typedecl memory
consts
  seq :: "program β‡’ program β‡’ program" (infixl ";" 10) (* c;d: run c, then run d *)
  ifthen :: "(memory β‡’ bool) β‡’ program β‡’ program" (* ifthen e c: run c if e(current_mem)=true *)
  while :: "(memory β‡’ bool) β‡’ program β‡’ program" (* while e c: run c while e(current_mem)=true *)
  denotation :: "program β‡’ memory β‡’ memory"  (* denotation c m: memory after running c, when starting with memory m *)
  hoare :: "(memory β‡’ bool) β‡’ program β‡’ (memory β‡’ bool) β‡’ bool" 
      (* hoare P c Q: if P(current_mem), then after running c, we have Q(current_mem) *)

Now it is not true that (a;b);c = a;(b;c)

(these are different programs), but he believes that they are denotationally equivalent, i.e. denotation ((a;b);c)) = denotation (a;(b;c))

...

This means that I have to rewrite a;(b;c)

in the (a;b);c

Hoare triplets inside. For example, I would like to be able to prove

lemma "hoare P (while e (a;b;c)) Q ==> hoare P (while e (a;(b;c))) Q"

just using the simplifier ( by simp

), given the appropriate simplification rules.

Logically, the relevant rules would be the following:

lemma "denotation (a;(b;c)) = denotation ((a;b);c)"
lemma "denotation a = denotation b ==> hoare P a Q = hoare P b Q"
lemma "denotation a = denotation b ==> denotation (while e a) = denotation (while e b)"
lemma "denotation a = denotation b ==> denotation (ifthen e a) = denotation (ifthen e b)"
lemma "denotation a = denotation a' ==> denotation b = denotation b' ==> denotation (a;b) = denotation (a';b')"

Unfortunately, there seems to be no easy way to communicate these rules to the simplifier. (More generally, we would like to say a simplifier in the congruence rule that the rewriting below must have some equivalence relation, denotational equivalence in this example.)

I found a partial solution to this problem (see my own answer below), but the solution seems to be a hack (and I don't know how stable it is) and I'm wondering if there is a good way to do this.

I don't mind using any ML code in this process (like writing simproc), but I would like to avoid re-completing the whole overwrite simplification inside Hoare tuples.

+3


source to share


3 answers


Isabella Simplifier does not support rewriting with respect to arbitrary equivalence relations. Luckily, your rewrites look pretty straightforward, so it might make sense to implement the rewrites in simproc. Here's the idea:

Write simproc that runs on form conditions hoare P c Q

. When called, it sets the purpose of the form hoare P c Q == ?rhs

and enforces the rule that it %c. hoare P c Q

only cares about the equivalence class of its argument, not a specific element. Then apply the rewrite rules as introduction rules until the stated goal is achieved. This was to create an instance ?rhs

on the form hoare P c' Q

. Check if c

and c'

alpha beta eta ... are equivalent. If so, simproc fails with NONE

, otherwise it returns the validated equation.

Here are a bunch of lemmas that I would use as a start:

definition fun_equiv :: "('a β‡’ 'b) β‡’ 'a β‡’ 'a β‡’ bool"
where "fun_equiv f x y ⟷ f x = f y"

lemma fun_equiv_refl: "fun_equiv f x x" by(simp add: fun_equiv_def)

lemma hoare_cong_start: (* start rule *)
  "fun_equiv denotation c c' ⟹ hoare P c Q == hoare P' c' Q'"
sorry

lemma while_cong: "fun_equiv denotation c c' ⟹ fun_equiv denotation (while b c) (while b c')" sorry

lemma seq_cong: "⟦ fun_equiv denotation a a'; fun_equiv denotation b b' ⟧ ⟹ fun_equiv denotation (a ; b) (a' ; b')" sorry

lemma if_cong: "fun_equiv denotation c c' ⟹ fun_equiv denotation (ifthen b c) (ifthen b c')" sorry

lemma seq_assoc: "fun_equiv denotation (a ; (b ; c)) (a; b; c)" sorry

lemma ifthen_true: "fun_equiv denotation (ifthen (Ξ»m. True) c) c" sorry

lemmas hoare_intros =
  -- β€Ήrewrites come first, congruences later, reflexivity lastβ€Ί
  ifthen_true seq_assoc
  while_cong if_cong seq_cong
  fun_equiv_refl

Since this is a simproc inside a simplification, you can assume that the command in the call is already in wrt simset normal form. In your example, the test is %m. m = m

already simplified to %_. True

. So simproc can only focus on implementing rewrites for hoare rules.



One step of calling simproc is to do something like the following Isar snippet:

schematic_lemma "hoare (Ξ»m. P x) (while P (c;(d;e);ifthen (Ξ»m. True) (f;g;c))) (Ξ»m. True) == ?c"
by(rule hoare_cong_start)(rule hoare_intros)+

Since the simplifier iterates over simproc until it runs no longer, you should really get a normal form.

If you want to support the conditional rules for rewriting wrt denotational equivalence, you rule hoare_intros

should replace with something that checks the format of the subcell. If it is not a form fun_equiv denotation _ _

, then simproc should invoke simplification recursively (or any other proof method of your choice) rather than trying to apply a different rule hoare_intros

.

+2


source


For a way that seems to work fine see the attached Isabel / HOL theory. The idea is to use conditional sim rules to simulate cong rules.

For example, the congruence rule

lemma l1 [cong]: "f a = f b ==> g a = g b"

is also a valid simp conditional rule

lemma l2 [simp]: "f a = f b ==> g a = g b"

and when Isabelle applies the simp rule, b will be replaced with a conditional variable, and the simplifier will rewrite "fa = f? b", which instantiates b to simplify b.



However, the lemma l2

will make a simplification loop because it can be applied to it with its own rhs. So instead we can write the rule

lemma l3 [simp]: "f_simp a = f_done b ==> g_simp a = g_done b"

where g_simp

and are g_done

defined as equal g

, but will not allow the simplifier to apply the rules in a loop.

A complete working example of this idea is contained in the theory file below.

Problems: This is a hack. I don't know in what situations it might break or be incompatible with other things - it apply simp

might overwrite partially, so you need to call it again to complete the rewrite. (See the last lemma in theory.)

theory Test
imports Main
begin

section "Minimal Hoare logic"

(* A simple language and Hoare logic *)
typedecl program
typedecl memory
consts
  seq :: "program β‡’ program β‡’ program" (infixl ";" 10) (* c;d: run c, then run d *)
  ifthen :: "(memory β‡’ bool) β‡’ program β‡’ program" (* ifthen e c: run c if e(current_mem)=true *)
  while :: "(memory β‡’ bool) β‡’ program β‡’ program" (* while e c: run c while e(current_mem)=true *)
  denotation :: "program β‡’ memory β‡’ memory"  (* denotation c m: memory after running c, when starting with memory m *)
  hoare :: "(memory β‡’ bool) β‡’ program β‡’ (memory β‡’ bool) β‡’ bool" 
  (* hoare P c Q: if P(current_mem), then after running c, we have Q(current_mem) *)

(* seq is associative modulo denotational equivalence.
  Thus we should be able to rewrite "a;(b;c)" to "a;b;c"
  within a hoare triple. E.g., the following should be solved with simp: *)
lemma
  assumes "hoare P (while e (a;b;c)) Q"
  shows "hoare P (while e (a;(b;c))) Q"
using assms
oops (* by simp *)

section "A failed attempt"

experiment begin
(* Here a natural approach first which, however, fails. *)

(* A congruence rule for the simplifier. 
   To rewrite a hoare triple "hoare P c Q", 
   we need to rewrite "denotation c". *)

lemma enter [cong]:
  assumes "P==P'" and "Q==Q'"
  assumes "denotation c == denotation c'"
  shows "hoare P c Q == hoare P' c' Q'"
sorry

(* To descend further into subterms, we need a congruence-rule for while. *)
lemma while [cong]: 
  assumes "e=e'"
  and "denotation c == denotation c'"
  shows "denotation (while e c) ≑ denotation (while e' c')"
sorry

(* And we give a simplification rule for the associativity of seq *)
lemma assoc [simp]:
  "denotation (a;(b;c)) = denotation (a;b;c)"
sorry

(* Now we can simplify the lemma from above *)
lemma
  assumes "hoare P (while e (a;b;c)) Q"
  shows "hoare P (while e (a;(b;c))) Q"
using assms by simp

(* Unfortunately, this does not work any more once we add more congruence rules. *)
(* To descend further into subterms, we need a congruence-rule for while. *)
lemma ifthen [cong]: 
  assumes "e=e'"
  and "denotation c == denotation c'"
  shows "denotation (ifthen e c) ≑ denotation (ifthen e' c')"
sorry
(* Warning: Overwriting congruence rule for "Test.denotation" *)

(* Simplifier doesn't work any more because the congruence rule for while was overwritten *)
lemma
  assumes "hoare P (while e (a;b;c)) Q"
  shows "hoare P (while e (a;(b;c))) Q"
using assms 
oops (* by simp *)

end

section {* A working attempt *}

(* Define copies of the denotation-constant, to control the simplifier *)
definition "denotation_simp == denotation"
definition "denotation_done == denotation"

(* A congruence rule for the simplifier. 
   To rewrite a hoare triple "hoare P c Q", 
   we need to rewrite "denotation c".

   This means, the congruence rule should have an assumption
   "denotation c == denotation c'"

   However, to avoid infinite loops with the rewrite rules below,
   we use the logically equivalent assumption
   "denotation_simp c == denotation_done c'"

   This means that we need to configure the rules below rewrite
   "denotation_simp c" into "denotation_done c'" where c' is 
   the simplication of c (module denotational equivalence).
 *)
lemma enter [cong]:
  assumes "P==P'" and "Q==Q'"
  assumes "denotation_simp c == denotation_done c'"
  shows "hoare P c Q == hoare P' c' Q'"
sorry

(* A similar congruence rule for simplifying expressions
  of the form "denotation c". *)
lemma denot [cong]:
  assumes "denotation_simp c == denotation_done c'"
  shows "denotation c == denotation c'"
sorry

(* Now we add a congruence-rule for while.
  Since we saw above that we cannot use several congruence-rules
  with "denotation" as their head,
  we simulate a congruence rule using a simp-rule.

  To rewrite "denotation_simp (while e c)", we need to rewrite
  "denotation_simp c".

  We put denotation_done on the rhs instead of denotation_simp 
  to avoid infinite loops.
*)
lemma while [simp]: 
  assumes "e=e'"
  and "denotation_simp c == denotation_done c'"
  shows "denotation_simp (while e c) ≑ denotation_done (while e' c')"
sorry

(* A pseudo-congruence rule for ifthen *)
lemma ifthen [simp]:
  assumes "e=e'"
  and "denotation_simp c == denotation_done c'"
  shows "denotation_simp (ifthen e c) == denotation_done (ifthen e' c')"
sorry

(* A pseudo-congruence rule for seq *)
lemma seq [simp]:
  assumes "denotation_simp c == denotation_done c'"
  and "denotation_simp d == denotation_done d'"
  shows "denotation_simp (c;d) == denotation_done (c';d')"
sorry

(* Finally, we can state associativity of seq. *)
lemma assoc [simp]:
  "denotation_simp (a;(b;c)) = denotation_simp (a;b;c)"
sorry

(* Finally, since our congruence-rules expect the rewriting to rewrite
  "denotation_simp c" into "denotation_done c'", 
  we need to translate any non-rewritten "denotation_simp" into
  "denotation_done".

  However, a rule "denotation_simp c == denotation_done c" does not work,
  because it could be triggered too early, and block the pseudo-congruence rules above.

  So we only trigger the rule when the current term would not match
  any of the pseudo congruence rules *)
lemma finish [simp]: 
  assumes "NO_MATCH (while e1 c1) a"
  assumes "NO_MATCH (ifthen e2 c2) a"
  assumes "NO_MATCH (c3;d3) a"
  shows "denotation_simp a = denotation_done a"
sorry

(* Testing the simplifier rules *)
lemma
  assumes "hoare P (while e (a;b;c)) Q"
  shows "hoare P (while e (a;(b;c))) Q"
using assms 
by simp


(* Some more complex test *)
lemma iftrue [simp]: "denotation_simp (ifthen (Ξ»m. True) c) == denotation_simp c" sorry
lemma
  assumes "β‹€x. Q x"
  assumes "hoare (λm. P x ∧ Q x) (while P (c;(d;e);(f;g);c)) (λm. m=m)"
  shows "hoare (Ξ»m. P x) (while P (c;(d;e);ifthen (Ξ»m. m=m) (f;g;c))) (Ξ»m. True)"
using assms
apply simp (* Hmm. Only partially simplified... The assoc rule is not applied to the result of the iftrue rule *)
by simp (* Rerunning simp solves the goal *)
(* By the way: "using assms by auto" solves the goal in one go *)

end
0


source


Below is my implementation of Andreas Lochbeeler's suggestions . The first part is a generic implementation (suitable for other equivalents than denotational equivalence), and below it is created for my example of Hoare logic.

(* Written by Dominique Unruh *)
theory Test2
imports Main
begin

section "Implementation of modulo-simplifier"


definition fun_equiv :: "('a β‡’ 'b) β‡’ 'a β‡’ 'a β‡’ bool" where "fun_equiv f x y == f x = f y"
lemma fun_equiv_refl: "fun_equiv f x x" by(simp add: fun_equiv_def)

ML {*
(* Call as: hoare_simproc_tac (simplifications@congruences) context/simpset *)
fun fun_equiv_simproc_tac intros ctxt =
  SUBGOAL (fn (goal,i) =>
    case goal of
      Const(@{const_name Trueprop},_) $ (Const(@{const_name fun_equiv},_)$_$_$_) => 
        (resolve0_tac intros THEN_ALL_NEW fun_equiv_simproc_tac intros ctxt) i
        ORELSE (rtac @{thm fun_equiv_refl} i)
    | _ => 
        SOLVED' (simp_tac ctxt) i)

fun fun_equiv_simproc start intros _ ctxt (t:cterm) = 
  let val fresh_var = Var(("x",Term.maxidx_of_term (Thm.term_of t)+1),Thm.typ_of_cterm t)
      val goal = Logic.mk_equals (Thm.term_of t,fresh_var)
      val thm = Goal.prove ctxt [] [] goal 
                (fn {context,...} => resolve0_tac start 1 THEN ALLGOALS (fun_equiv_simproc_tac intros context))
  in 
    if (Thm.rhs_of thm) aconvc t then NONE else SOME thm
  end
  handle ERROR msg => (warning ("fun_equiv_simproc failed\nTerm was:\n"^(@{make_string} t)^"\nError: "^msg); NONE)

fun fun_equiv_simproc_named start cong simp morph ctxt =
  fun_equiv_simproc (Named_Theorems.get ctxt start) (Named_Theorems.get ctxt simp @ Named_Theorems.get ctxt cong) morph ctxt
*}

section "Minimal Hoare logic"

(* A simple language and Hoare logic *)
typedecl program
typedecl memory
consts
  seq :: "program β‡’ program β‡’ program" (infixl ";" 100) (* c;d: run c, then run d *)
  ifthen :: "(memory β‡’ bool) β‡’ program β‡’ program" (* ifthen e c: run c if e(current_mem)=true *)
  while :: "(memory β‡’ bool) β‡’ program β‡’ program" (* while e c: run c while e(current_mem)=true *)
  denotation :: "program β‡’ memory β‡’ memory"  (* denotation c m: memory after running c, when starting with memory m *)
  hoare :: "(memory β‡’ bool) β‡’ program β‡’ (memory β‡’ bool) β‡’ bool" 
      (* hoare P c Q: if P(current_mem), then after running c, we have Q(current_mem) *)

section "Instantiating the simplifier"

named_theorems denot_simp_start
named_theorems denot_simp
named_theorems denot_cong

lemma hoare_cong_start [denot_simp_start]: "fun_equiv denotation c c' ⟹ hoare P c Q == hoare P c' Q" sorry
lemma while_cong [denot_cong]: "fun_equiv denotation c c' ⟹ fun_equiv denotation (while b c) (while b c')" sorry
lemma seq_cong [denot_cong]: "fun_equiv denotation a a' ⟹ fun_equiv denotation b b' ⟹ fun_equiv denotation (a ; b) (a' ; b')" sorry
lemma if_cong [denot_cong]: "fun_equiv denotation c c' ⟹ fun_equiv denotation (ifthen b c) (ifthen b c')" sorry
lemma seq_assoc [denot_simp]: "fun_equiv denotation (a ; (b ; c)) (a; b; c)" sorry
lemma ifthen_true [denot_simp]: "(β‹€m. e m) ⟹ fun_equiv denotation (ifthen e c) c" sorry
lemma double_while [denot_simp]: "(β‹€m. e m = e' m) ⟹ fun_equiv denotation c d ⟹ fun_equiv denotation (seq (while e c) (while e' d)) (while e c)" sorry

(* -- "If the set of simplification theorems is fixed, we can use the following setup"
  lemmas hoare_congruences = while_cong if_cong seq_cong
  lemmas hoare_simps = ifthen_true seq_assoc double_while
  simproc_setup hoare_simproc ("hoare P c Q") = {* fun_equiv_simproc @{thms hoare_cong_start} @{thms hoare_simps hoare_congruences} *}
*)


(* To make use of dynamic lists of theorems, we use the following setup *)
simproc_setup hoare_simproc ("hoare P c Q") = {* 
  fun_equiv_simproc_named @{named_theorems denot_simp_start}
                          @{named_theorems denot_cong}
                          @{named_theorems denot_simp}
*}

section "Tests"

(* Testing the simplifier rules *)
lemma
  assumes "hoare P (while e (a;b;c)) Q"
  shows "hoare P (while e (a;(b;c))) Q ∧ True"
using assms 
by simp

lemma 
  assumes "hoare P (while P (c;d;e)) Q"
  assumes "β‹€x. P x = R x"
  shows "hoare P ((while P (c;(d;e))); (while R ((c;d);e))) Q"
using assms by simp

lemma
  assumes "β‹€x. Q x"
  assumes "hoare (λm. P x ∧ Q x) (while P (c;(d;e);(f;g);c)) (λm. m=m)"
  shows "hoare (Ξ»m. P x) (while P (c;(d;e);ifthen (Ξ»m. m=m) (f;g;c))) (Ξ»m. True)"
using assms by simp

(* Test: Disabling the simproc *)
lemma
  assumes "hoare P (a;(b;c)) Q"
  shows   "hoare P (a;(b;c)) Q ∧ True"
using[[simproc del: hoare_simproc]] -- "Without this, proof fails"
apply simp
by (fact assms)
end
0


source






More articles:


All Articles