First stab at handling permutative rewrite rules

[msaaltink]

Giuliano and I have been working on some proofs that would be much easier if the rewriter could handle permutative rules. This small modification to the rewriter allows for associative and commutative functions to be handled, whether curried or not. It is a bit inefficient, adding about 3% to the proof time for a rewrite-intensive proof suite that does not use permuting at all, and could be optimized if that's a problem.

A rule is 'permutative' if the left and right sides are instances of one another. An ordering relation is then used to decide whether to apply the rule or not. I'm not sure what a general ordering rule would be for higher-order logic, and the ordering I implemented here works OK for association-type laws but is not as general as I would like. The ordering looks at the "fringe" of arguments in possibly-nested calls to a function. Possibly LRPO would be a better choice, but I would need to understand the saw-core term structure better to implement that.

Other than the 3% cost of this feature I think there is no downside; the rules it applies to would have looped in the existing rewriter and so whatever I am doing in no worse.

The code happens to recognize when a single rule could loop and could easily be adapted to block the application of such a rule. This would still not prevent loops involving more than one rule, but is a start.

I have a small test suite for this, but in saw-script rather than in Haskell, so I do not know how I could add it to the tests here.

[brianhuffman]

To avoid the performance hit, we should not evaluate rulePermutes repeatedly during simplification; instead, let's evaluate it once and cache the permutes bit alongside each rule in the simpset. We can probably just add a new Bool field to the RewriteRule type.

[brianhuffman]

Comment from @msaaltink:

My main reason NOT to add a bit the the record field is that to test for permuting, I use the sc matcher, which is in the IO monad, and that's going to mess up a lot of other existing functions signatures. e.g., things dealing with simpsets. But perhaps I can just use the first-order matcher instead. I'll give that a try.

[brianhuffman]

If first_order_match works, then it's probably easiest to use it to compute the permutative flag as each RewriteRule is created. Another possibility, if you don't want to put all the Simpset operations in the IO monad, is to traverse the Simpset at the entry point to rewriteSharedTerm, so that you call rulePermutes only once per rule in the simpset.

[msaaltink]

I think first-order matching will be fine. I'm not really sure what a reasonable higher-order permutative rewrite rule would look like anyway.

[msaaltink]

This now checks for permutativity when a RewriteRule is created. This is not as much as an improvement as one might have hoped, but appears to be slightly more efficient than the original.

[msaaltink]

In case it is helpful, here's a file of things I use to test the rewriter mods:

// With curried functions

let {{ f x (y:Integer) = x + y
       g x (y:Integer) = x*y
       h x = g 3 x }};

fc <- prove_print z3 {{ \ a b -> f a b == f b a }}; // f is commutative

// fa <- prove_print z3 {{ \ a b c -> f a (f b c) == f (f a b) c}}; // f is left-associative 
fa <- prove_print z3 {{ \ a b c -> f (f a  b) c == f a (f b c)}}; 

// fp <- prove_print z3 {{ \ a b c -> f (f a b) c  == f (f a c) b}}; // extra rule needed for full sorting
fp <- prove_print z3 {{ \ a b c -> f a (f b c) == f b (f a c) }};

let f_rules = addsimps [fc, fa, fp] empty_ss;

// let go = prove_print do {simplify f_rules; print_goal; w4_unint_z3 ["f", "g", "h"]; };
let go t = do {
  print ("Trying", t);
  prove_print do {simplify f_rules; print_goal; w4_unint_z3 ["f", "g", "h"]; } t;
  };

go {{ \ x y s t -> f (f x s)(f t y) == f (f s t) (f y x) }};

go {{ \ x y s t -> f (f (g x x) s)(f t y) == f (f s t) (f y (g x x)) }};

go {{ \ x -> f 0 (f 1 x) == f (f x 1) 0 }};

go {{ \ x -> f (h 0) (f (h 1) x) == f (f x (h 1)) (h 0) }};

f0_l <- prove_print z3 {{ \ a -> f 0 a == a }};
f0_r <- prove_print z3 {{ \ a -> f a 0 == a }};

gc <- prove_print z3 {{ \ a b -> g a b == g b a }};
ga <- prove_print z3 {{ \ a b c -> g a (g b c) == g (g a b) c}};
gp <- prove_print z3 {{ \ a b c -> g (g a b) c  == g (g a c) b}};
g0_l <- prove_print z3 {{ \ a -> g 0 a == 0 }};
g0_r <- prove_print z3 {{ \ a -> g a 0 == 0 }};
g1_l <- prove_print z3 {{ \ a -> g 1 a == a }};
g1_r <- prove_print z3 {{ \ a -> g a 1 == a }};
g_dist_l <- prove_print z3 {{ \ a b c -> g (f a b) c == f (g a c) (g b c) }};
g_dist_r <- prove_print z3 {{ \ a b c -> g a (f b c) == f (g a b) (g a c) }};

let fg_rules = addsimps [ f0_l, f0_r, fc, fa, fp
                        , f0_l, g0_r, g1_l, g1_r, gc, ga, gp
                        , g_dist_l, g_dist_r
                        ] empty_ss;

let go' = prove_print do {simplify fg_rules; print_goal; w4_unint_z3 ["f", "g", "h"]; };

go' {{ \ x y -> f x (g y x) == g (f 1 y) x }}; // x + yx == (1+y)*x
go' {{ \ x y -> (g (f x y) (f y x)) == f (g x x) (f (g x y) (f (g x y) (g y y))) }};
  // (x+y)*(x+y) == ...
go' {{ \ a b c -> f (g a b) (g b c) == g (f a c) b }};

print "Now with rule hr added";

hr <- prove_print z3 {{ \x -> h x == f (f x x) x }};

let go_h = prove_print do {simplify (addsimp hr f_rules); print_goal; w4_unint_z3 ["f", "g", "h"]; };

go_h {{ \ x -> f 0 (f 1 x) == f (f x 1) 0 }};

fails (go_h {{ h 0 == 0 }});

go_h {{ \a b c -> f (h c) (f (h a) b) == f a (f a (f a (f b (f c (f c  c))))) }}; 

/// Now with tupled functions

print "*** TUPLING ***";

let {{ add (x:[8], y) = x + y
       mul (x:[8], y) = x * y
       neg (x:[8]) = - x }};

add_c <- prove_print z3 {{ \ x y -> add (x,y) == add (y, x) }};
add_a <- prove_print z3 {{ \ x y z -> add (add (x, y), z) == add (x, add (y,z)) }}; // right-associative
add_p <- prove_print z3 {{ \ x y z -> add (x, add (y, z)) == add (y, add (x,z)) }};

mul_c <- prove_print z3 {{ \ x y -> mul (x,y) == mul (y, x) }};
mul_a <- prove_print z3 {{ \ x y z -> mul (mul (x, y), z) == mul (x, mul (y,z)) }};
mul_p <- prove_print z3 {{ \ x y z -> mul (x, mul (y, z)) == mul (y, mul (x,z)) }};

mul_dist_1 <- prove_print z3  {{ \ x y z -> mul (add (x,y), z) == add (mul (x, z), mul (y,z)) }};
mul_dist_2 <- prove_print z3  {{ \ x y z -> mul (z, add (x,y)) == add (mul (z, x), mul (z,y)) }};

alg_ss <- addsimps [add_c, add_a, add_p, mul_c, mul_a, mul_p, mul_dist_1, mul_dist_2] empty_ss;

let test = prove_print do { unfolding ["curry"]; simplify alg_ss; w4_unint_z3 ["add", "mul", "neg"]; } ;

s <- fresh_symbolic "s" {| [8] |};
t <- fresh_symbolic "t" {| [8] |};
u <- fresh_symbolic "u" {| [8] |};

test {{ \ x y -> mul (x,y) == mul (y,x) }};
test {{ add (s, t) == add (t,s) }};
test {{ \x -> mul (mul (x, s), mul (x, s)) == mul (mul (mul (s, s), x), x) }};
test {{ mul (add (s,t), add (t, s)) == add (mul(s,s), add (mul (s, t), add (mul (s, t), mul (t, t)))) }};

test {{ \ x y z -> (x*x) * (y*z) == z*y*x*x where (*) = curry mul }};
test {{ \ x y z -> (x*x) * ((neg (y+z))*z) == z*(neg (z+y))*x*x where (*) = curry mul; (+) = curry add }};

print "Functions from records";

let {{
  type Ring = { a: Integer -> Integer -> Integer
              , m: Integer -> Integer -> Integer }
  R: Ring
  R = { a = (+), m = (*) }
  }};

R0 <- prove_print z3 {{ \ a -> R.m a 0 == 0 }};
R0' <- prove_print z3 {{ \ a -> R.m 0 a == 0 }};
Rc <- prove_print z3 {{ \ a b -> R.m a b == R.m b a }}; // R.m is commutative
Ra <- prove_print z3 {{ \ a b c -> R.m (R.m a  b) c == R.m a (R.m b c)}}; 
Rp <- prove_print z3 {{ \ a b c -> R.m a (R.m b c) == R.m b (R.m a c) }};

let R_rules = addsimps [R0, R0', Rc, Ra, Rp] empty_ss;

prove_print do {simplify R_rules; w4_unint_z3 ["R"]; } {{ \x y -> R.m x (R.m y x) == R.m (R.m x x) y }};

[brianhuffman]

This looks reasonable. One remaining uncertainty is about the design of the term ordering. If this term ordering works well enough for your current use case, then you're welcome to go ahead and merge this PR. But in any case, in the longer term, we should probably make a well-informed deliberate choice about the right term ordering to use. (Some example term orderings used in the Isabelle simplifier can be seen here: https://github.com/isabelle-prover/mirror-isabelle/blob/master/src/Pure/term_ord.ML)

If you don't want to address the term ordering right away, that's fine, but we should open a ticket so that we don't forget to revisit the issue.

[msaaltink]

I am in complete agreement about the term ordering. I had also looked at the term orderings used by ACL2 (a strange and very detailed ordering) and by the old EVES system (which used LRPO). The Isabelle term orderings are also worth looking at, thanks. A problem I had was in maintaining compatibility with the existing rewrite system, so that non-permuting rules are always applied. This can interact with well-founded term orderings in a bad way. So the current rule is a compromise, that works in the cases Giuliano and I want right now. But I agree, a ticket is appropriate, and some more careful design needed.

As well, after this is merged the SAW documentation ought to be revised to describe this as, I suppose, an "experimental and subject to change" handling of looping rules.