feat(rules): add implication normalisation rules

Adds the following normalisation rules for implication:

  + Contrapositive `!p -> !q ~~> q->p    where p,q are safe`

  + Negation `!(p -> q) ~~> p/\ !q    where p->q is safe`

  + Left distributivity: `(r->p) -> (r->q) ~~> (r -> (p ~> q))`

  + Import-export / uncurrying: `p -> (q->r) ~~> (p/\q) -> r`

Import-export has a lower priority of 8400 to allow distributivity to
apply first.

For example, we want to do:

```
((r -> p) -> (r -> q)) ~> (r -> (p -> q))  [left-distributivity]
(r -> (p -> q)) ~> (r/\p) ~> q [uncurry]
```

not

```
((r->p) -> (r->q)) ~> ((r->p) /\ r) -> q) ~> [uncurry]
```

conjure_oxide/tests/integration/basic/implies/04-needs-normalising/input-expected-rule-trace-human.txt

@@ -1,59 +1,106 @@
 Model before rewriting:
 
+find a: bool
+find b: bool
+find c: bool
+find d: bool
+find e: bool
+find f: bool
+find g: bool
+find h: bool
 find x: bool
 find y: bool
 
 such that
 
-Not((Not(x)) -> (Not(y)))
+Not((Not(x)) -> (Not(y))),
+(Not(a)) -> (Not(b)),
+(c) -> ((d) -> (e)),
+((h) -> (f)) -> ((h) -> (g))
 
 --
 
 Not((Not(x)) -> (Not(y))), 
-   ~~> flatten_generic ([("Minion", 4200)]) 
-Not(__0) 
-new variables:
-  __0: bool
-new constraints:
-  __0 =aux (Not(x)) -> (Not(y))
+   ~~> normalise_implies_negation ([("Base", 8800)]) 
+And([Not(x), Not(Not(y))]) 
+
 --
 
-__0 =aux (Not(x)) -> (Not(y)), 
-   ~~> bool_eq_to_reify ([("Minion", 4400)]) 
-Reify((Not(x)) -> (Not(y)), __0) 
+(Not(a)) -> (Not(b)), 
+   ~~> normalise_implies_contrapositive ([("Base", 8800)]) 
+(b) -> (a) 
+
+--
+
+((h) -> (f)) -> ((h) -> (g)), 
+   ~~> normalise_implies_left_distributivity ([("Base", 8800)]) 
+(h) -> ((f) -> (g)) 
+
+--
+
+Not(Not(y)), 
+   ~~> remove_double_negation ([("Base", 8400)]) 
+y 
+
+--
+
+(c) -> ((d) -> (e)), 
+   ~~> normalise_implies_uncurry ([("Base", 8400)]) 
+(And([c, d])) -> (e) 
+
+--
+
+(h) -> ((f) -> (g)), 
+   ~~> normalise_implies_uncurry ([("Base", 8400)]) 
+(And([h, f])) -> (g) 
 
 --
 
-(Not(x)) -> (Not(y)), 
+(b) -> (a), 
+   ~~> introduce_reifyimply_ineq_from_imply ([("Minion", 4400)]) 
+Ineq(b, a, 0) 
+
+--
+
+(And([c, d])) -> (e), 
    ~~> flatten_imply ([("Minion", 4200)]) 
-(__1) -> (Not(y)) 
+(__0) -> (e) 
 new variables:
-  __1: bool
+  __0: bool
 new constraints:
-  __1 =aux Not(x)
+  __0 =aux And([c, d])
 --
 
-(__1) -> (Not(y)), 
+(__0) -> (e), 
    ~~> introduce_reifyimply_ineq_from_imply ([("Minion", 4400)]) 
-ReifyImply(Not(y), __1) 
+Ineq(__0, e, 0) 
 
 --
 
-__1 =aux Not(x), 
+__0 =aux And([c, d]), 
    ~~> bool_eq_to_reify ([("Minion", 4400)]) 
-Reify(Not(x), __1) 
+Reify(And([c, d]), __0) 
 
 --
 
-Not(__0), 
-   ~~> not_literal_to_wliteral ([("Minion", 4100)]) 
-WatchedLiteral(__0,false) 
+(And([h, f])) -> (g), 
+   ~~> flatten_imply ([("Minion", 4200)]) 
+(__1) -> (g) 
+new variables:
+  __1: bool
+new constraints:
+  __1 =aux And([h, f])
+--
+
+(__1) -> (g), 
+   ~~> introduce_reifyimply_ineq_from_imply ([("Minion", 4400)]) 
+Ineq(__1, g, 0) 
 
 --
 
-Not(y), 
-   ~~> not_literal_to_wliteral ([("Minion", 4100)]) 
-WatchedLiteral(y,false) 
+__1 =aux And([h, f]), 
+   ~~> bool_eq_to_reify ([("Minion", 4400)]) 
+Reify(And([h, f]), __1) 
 
 --
 
@@ -65,14 +112,25 @@ WatchedLiteral(x,false)
 
 Final model:
 
+find a: bool
+find b: bool
+find c: bool
+find d: bool
+find e: bool
+find f: bool
+find g: bool
+find h: bool
 find x: bool
 find y: bool
 find __0: bool
 find __1: bool
 
 such that
 
-WatchedLiteral(__0,false),
-Reify(ReifyImply(WatchedLiteral(y,false), __1), __0),
-Reify(WatchedLiteral(x,false), __1)
+And([WatchedLiteral(x,false), y]),
+Ineq(b, a, 0),
+Ineq(__0, e, 0),
+Ineq(__1, g, 0),
+Reify(And([c, d]), __0),
+Reify(And([h, f]), __1)