# Translating My Z3 Tutorial to Coq

I had a fun time giving a Z3 tutorial at Formal Methods for the Informal Engineer (FMIE) https://fmie2021.github.io/ (videos coming soon hopefully!). I got to be kind of the "fun dad" with the Z3 tutorial https://github.com/philzook58/z3_tutorial , while at times it felt a bit like Cody's Coq tutorial https://github.com/codyroux/broad-coq-tutorial was trying to feed the kids their vegetables. It was a fantastic tutorial (maybe the best I've seen?), but it was tough love. He knew it was going to be like this from the outset and had a fun little analogy of me downhill skiing while he was about to go on an uphill mountaineering slog.

There are a number of factors to lead to this:

- I could use Z3’s python bindings giving an air of familiarity, whereas everything was incredibly foreign in Coq.
- Z3 can actually be used to declaratively state problems and pushbutton calculate solutions to them with very little user help, which gives it a lot more "Wow" factor.
- Coq is a tool that requires significantly more background to even comprehend what the hell it is. I still think many aspects of it are totally bizarre. But Coq users, this is just the water they swim in. For example, defining an inductive predicate as a datatype is still a bizarre notion to me, but it is Coq 101. I say this to Coq users and they look at me like I’m nuts. “What could even be the problem?”

Anyway, a fun exercise for me was to take the examples from my tutorial and try to translate them into Coq. For the most part I think it isn't that hard and rather educational.

It's interesting the things that show up. Because the Z3 tutorial was designed for automation, the more automated tactics in MicroOmega and Ring are super useful.

https://coq.inria.fr/refman/addendum/micromega.html

The thing is that the sort of proofs that show up here are fine and all, but they aren't going to teach you to fish for yourself. When you step out of this super automatable fragment you're sunk if you don't know other techniques, like the ones Cody was teaching. There may be a better balance of fun and education to be found.

I think there is a hole in the educational content out there on Coq. Software Foundations focuses on the rudiments, CPDT and FRAP kind of takes it a little hardcore, and the Mathematical Components stuff makes you buy in on ssreflect style and some hardcore math topics, both of which are nuts I have not cracked. Also, all of them are really long and initimidating. Seems like there should be something a little more breezy, a little more automatic. It is demoralizing as a beginner to either not know how to prove obvious trivial facts, or even to struggle to do so at great length.

This was also a nice opportunity to take Alectryon by Clément Pit-Claudel out for a spin https://github.com/cpitclaudel/alectryon Alectryon allows you to see the proof state on hover over in your browser. It's a super important part of the Coq. It was pretty easy to put in my blog. Just copy and paste the gnarly html output into a Jekyll post and make sure to link in the CSS files in an assets folder, because they are where the magic happens.

The gist for this post is here https://gist.github.com/philzook58/acd204b4895c41f9e85618f0f6b30a58

# Intro Stuff

The very first problem in the tutorial was

```
(** python
x = Int('x')
y = Int('y')
solve(x > 2, y < 10, x + 2*y == 7)
*)
```

which Z3 returns the solution [y = 0, x = 7].

It isn't so obvious how to get coq to find this solution in a low effort way. However, it is easy to get Coq to confirm the validity of this solution given that you know about the [lia] tactic. Otherwise it may be kind of annoying. In general, it may be a good approach to use external tools to produce solutions and just manually place the solutions into Coq. Validating a solution is often easier than producing it.

Require Import Lia.exists x y : nat, x > 2 /\ y < 10 /\ x + 2 * y = 7lia. Qed.7 > 2 /\ 0 < 10 /\ 7 + 2 * 0 = 7

A different automated version. Giving the appropriate hint database can matter a lot. https://coq.inria.fr/refman/proofs/automatic-tactics/auto.html#hint-databases-defined-in-the-coq-standard-library

exists x y : nat, x > 2 /\ y < 10 /\ x + 2 * y = 7eauto with arith. Qed.7 > 2 /\ 0 < 10 /\ 7 + 2 * 0 = 7

It turns out, surprisingly to me, that stock eauto is sufficient to actually solve the problem without supplying the solutions. They are discovered via unification and a prolog like search. This found the different solution x = 3, y = 2

do 2 eexists. eauto with arith.exists x y : nat, x > 2 /\ y < 10 /\ x + 2 * y = 7Defined. (* A fairly manual version for comparison. Could be even worse. *)exists x y : nat, x > 2 /\ y < 10 /\ x + 2 * y = 77 > 2 /\ 0 < 10 /\ 7 + 2 * 0 = 77 > 20 < 10 /\ 7 + 2 * 0 = 77 > 22 < 72 < 73 <= 73 <= 7apply le_n.3 <= 30 < 10 /\ 7 + 2 * 0 = 70 < 107 + 2 * 0 = 70 < 10apply le_n.1 <= 17 + 2 * 0 = 7reflexivity. Qed.7 = 7

The next thing is the simplest possible tautology

```
(**python
p = Bool("p")
my_true_thm = Implies(p, p)
prove(my_true_thm)
*)
```

This is not a challenge in Coq.

forall P : Type, P -> Passumption. Qed. (* Even shorter proof *)P:TypeX:PPauto. Qed.forall P : Type, P -> P

A valid counterexample found by Z3. Here we prove the counterexample.

(**python q = Bool("q") my_false_thm = Implies(q, p) prove(my_false_thm) # counterexample # [p = False, q = True] *)~ (True -> False)(True -> False) -> FalseH:True -> FalseFalseexact I. Qed.H:True -> FalseTrue

The first exercise: Get a root of the polynomial x**3 + 3*x**2 + 4*x + 2 == 0 using z3. Can you use z3 to show this is the only solution?

Here we open up the reals. It is easy enough to confirm that the solution of x=-1 is a zero using the [ring] tactic.

Require Import Reals. Open Scope R_scope.exists x : R, x ^ 3 + 3 * x ^ 2 + 4 * x + 2 = 0ring. Qed.(-1) ^ 3 + 3 * (-1) ^ 2 + 4 * -1 + 2 = 0

Proving there is no other solution is a bit trickier. A important lemma about a polynomial factor of x^3 + 3 * x^2 + 4 * x + 2

Require Import Lra.forall x : R, x ^ 2 + 2 * x + 2 > 0nra. Qed. (* A slightly more manual proof involving completing the square.*)x:Rx ^ 2 + 2 * x + 2 > 0forall x : R, x ^ 2 + 2 * x + 2 > 0x:Rx ^ 2 + 2 * x + 2 > 0x:RH:x ^ 2 + 2 * x + 2 = (x + 1) ^ 2 + 1x ^ 2 + 2 * x + 2 > 0x:RH:x ^ 2 + 2 * x + 2 = (x + 1) ^ 2 + 1(x + 1) ^ 2 + 1 > 0x:RH:x ^ 2 + 2 * x + 2 = (x + 1) ^ 2 + 1(x + 1) ^ 2 + 1 > 0lra. Qed. (* I'm actually a little suprised [nra] sufficed here and not psatz. *)x:RH:x ^ 2 + 2 * x + 2 = (x + 1) ^ 2 + 1r:=pow2_ge_0 (x + 1):0 <= (x + 1) ^ 2(x + 1) ^ 2 + 1 > 0forall x : R, x + 1 <> 0 -> x ^ 3 + 3 * x ^ 2 + 4 * x + 2 <> 0x:RH:x + 1 <> 0x ^ 3 + 3 * x ^ 2 + 4 * x + 2 <> 0x:RH:x + 1 <> 0H0:x ^ 3 + 3 * x ^ 2 + 4 * x + 2 = (x + 1) * (x ^ 2 + 2 * x + 2)x ^ 3 + 3 * x ^ 2 + 4 * x + 2 <> 0x:RH:x + 1 <> 0H0:x ^ 3 + 3 * x ^ 2 + 4 * x + 2 = (x + 1) * (x ^ 2 + 2 * x + 2)(x + 1) * (x ^ 2 + 2 * x + 2) <> 0nra. Qed. (* A slightly more manual proof *)x:RH:x + 1 <> 0H0:x ^ 3 + 3 * x ^ 2 + 4 * x + 2 = (x + 1) * (x ^ 2 + 2 * x + 2)r:=pos_poly x:x ^ 2 + 2 * x + 2 > 0(x + 1) * (x ^ 2 + 2 * x + 2) <> 0forall x : R, x + 1 <> 0 -> x ^ 3 + 3 * x ^ 2 + 4 * x + 2 <> 0x:RH:x + 1 <> 0x ^ 3 + 3 * x ^ 2 + 4 * x + 2 <> 0x:RH:x + 1 <> 0H0:x ^ 3 + 3 * x ^ 2 + 4 * x + 2 = (x + 1) * (x ^ 2 + 2 * x + 2)x ^ 3 + 3 * x ^ 2 + 4 * x + 2 <> 0x:RH:x + 1 <> 0H0:x ^ 3 + 3 * x ^ 2 + 4 * x + 2 = (x + 1) * (x ^ 2 + 2 * x + 2)(x + 1) * (x ^ 2 + 2 * x + 2) <> 0x:RH:x + 1 <> 0H0:x ^ 3 + 3 * x ^ 2 + 4 * x + 2 = (x + 1) * (x ^ 2 + 2 * x + 2)r:=pos_poly x:x ^ 2 + 2 * x + 2 > 0(x + 1) * (x ^ 2 + 2 * x + 2) <> 0x:RH:x + 1 <> 0H0:x ^ 3 + 3 * x ^ 2 + 4 * x + 2 = (x + 1) * (x ^ 2 + 2 * x + 2)r:=pos_poly x:x ^ 2 + 2 * x + 2 > 0(x + 1) * (x ^ 2 + 2 * x + 2) <> 0x:RH:x + 1 <> 0H0:x ^ 3 + 3 * x ^ 2 + 4 * x + 2 = (x + 1) * (x ^ 2 + 2 * x + 2)r:=pos_poly x:x ^ 2 + 2 * x + 2 > 0x + 1 <> 0x:RH:x + 1 <> 0H0:x ^ 3 + 3 * x ^ 2 + 4 * x + 2 = (x + 1) * (x ^ 2 + 2 * x + 2)r:=pos_poly x:x ^ 2 + 2 * x + 2 > 0x ^ 2 + 2 * x + 2 <> 0lra. Qed. Close Scope R_scope.x:RH:x + 1 <> 0H0:x ^ 3 + 3 * x ^ 2 + 4 * x + 2 = (x + 1) * (x ^ 2 + 2 * x + 2)r:=pos_poly x:x ^ 2 + 2 * x + 2 > 0x ^ 2 + 2 * x + 2 <> 0

# The send + more = money Puzzle

There is an assignment of unique digits to letters such that the equation send + more = money holds. Find an assignment of the digits to make this true.

Here is a Z3 version:

```
(**python
digits = Ints('s e n d m o r y')
s,e,n,d,m,o,r,y = digits
send = Sum([10**(3-i) * d for i,d in enumerate([s,e,n,d])]) # convert digits of number to number
more = Sum([10**(3-i) * d for i,d in enumerate([m,o,r,e])])
money = Sum([10**(4-i) * d for i,d in enumerate([m,o,n,e,y])])
solver = Solver()
solver.add([s > 0, m > 0]) # first digits are nonzero
# Constrain all digits constrained to be 0 through 9
solver.add([ And( 0 <= d, d <= 9 ) for d in digits])
# Constrain all digits to be unique (Hint: Look at the 8-Queens constraints. Anything useful?)
solver.add(Distinct(digits))
# Constrain send + more == money
solver.add(send + more == money)
solver.check()
solver.model()
*)
```

Again we can compute in Z3 and just verify in Coq.

I basically always want lists and list notation and can never remember where to find them. I think they should be on by default.

From Coq Require Import List. Import ListNotations. (* Convert list of digits to number *) Definition decimal_list l := let fix decimal_list_aux acc l := match l with | h :: t => acc * h + decimal_list_aux (10 * acc) t | [] => 0 end in decimal_list_aux 1 (List.rev l).Fixpoint all_different (l : list nat) : Prop := match l with | h :: t => List.fold_left (fun acc x => (h <> x) /\ acc ) t (all_different t) | [] => True end.exists s e n d m o r y : nat, let digits := [s; e; n; d; m; o; r; y] in let send := decimal_list [s; e; n; d] in let more := decimal_list [m; o; r; e] in let money := decimal_list [m; o; n; e; y] in s > 0 /\ m > 0 /\ Refl.make_conj (fun x : nat => x <= 9) digits /\ all_different digits /\ send + more = moneyexists e n d m o r y : nat, let digits := [9; e; n; d; m; o; r; y] in let send := decimal_list [9; e; n; d] in let more := decimal_list [m; o; r; e] in let money := decimal_list [m; o; n; e; y] in 9 > 0 /\ m > 0 /\ Refl.make_conj (fun x : nat => x <= 9) digits /\ all_different digits /\ send + more = moneyexists n d m o r y : nat, let digits := [9; 5; n; d; m; o; r; y] in let send := decimal_list [9; 5; n; d] in let more := decimal_list [m; o; r; 5] in let money := decimal_list [m; o; n; 5; y] in 9 > 0 /\ m > 0 /\ Refl.make_conj (fun x : nat => x <= 9) digits /\ all_different digits /\ send + more = moneyexists d m o r y : nat, let digits := [9; 5; 6; d; m; o; r; y] in let send := decimal_list [9; 5; 6; d] in let more := decimal_list [m; o; r; 5] in let money := decimal_list [m; o; 6; 5; y] in 9 > 0 /\ m > 0 /\ Refl.make_conj (fun x : nat => x <= 9) digits /\ all_different digits /\ send + more = moneyexists m o r y : nat, let digits := [9; 5; 6; 7; m; o; r; y] in let send := decimal_list [9; 5; 6; 7] in let more := decimal_list [m; o; r; 5] in let money := decimal_list [m; o; 6; 5; y] in 9 > 0 /\ m > 0 /\ Refl.make_conj (fun x : nat => x <= 9) digits /\ all_different digits /\ send + more = moneyexists o r y : nat, let digits := [9; 5; 6; 7; 1; o; r; y] in let send := decimal_list [9; 5; 6; 7] in let more := decimal_list [1; o; r; 5] in let money := decimal_list [1; o; 6; 5; y] in 9 > 0 /\ 1 > 0 /\ Refl.make_conj (fun x : nat => x <= 9) digits /\ all_different digits /\ send + more = moneyexists r y : nat, let digits := [9; 5; 6; 7; 1; 0; r; y] in let send := decimal_list [9; 5; 6; 7] in let more := decimal_list [1; 0; r; 5] in let money := decimal_list [1; 0; 6; 5; y] in 9 > 0 /\ 1 > 0 /\ Refl.make_conj (fun x : nat => x <= 9) digits /\ all_different digits /\ send + more = moneyexists y : nat, let digits := [9; 5; 6; 7; 1; 0; 8; y] in let send := decimal_list [9; 5; 6; 7] in let more := decimal_list [1; 0; 8; 5] in let money := decimal_list [1; 0; 6; 5; y] in 9 > 0 /\ 1 > 0 /\ Refl.make_conj (fun x : nat => x <= 9) digits /\ all_different digits /\ send + more = moneylet digits := [9; 5; 6; 7; 1; 0; 8; 2] in let send := decimal_list [9; 5; 6; 7] in let more := decimal_list [1; 0; 8; 5] in let money := decimal_list [1; 0; 6; 5; 2] in 9 > 0 /\ 1 > 0 /\ Refl.make_conj (fun x : nat => x <= 9) digits /\ all_different digits /\ send + more = moneylia. Qed.1 <= 9 /\ 1 <= 1 /\ (9 <= 9 /\ 5 <= 9 /\ 6 <= 9 /\ 7 <= 9 /\ 1 <= 9 /\ 0 <= 9 /\ 8 <= 9 /\ 2 <= 9) /\ ((9 = 2 -> False) /\ (9 = 8 -> False) /\ (9 = 0 -> False) /\ (9 = 1 -> False) /\ (9 = 7 -> False) /\ (9 = 6 -> False) /\ (9 = 5 -> False) /\ (5 = 2 -> False) /\ (5 = 8 -> False) /\ (5 = 0 -> False) /\ (5 = 1 -> False) /\ (5 = 7 -> False) /\ (5 = 6 -> False) /\ (6 = 2 -> False) /\ (6 = 8 -> False) /\ (6 = 0 -> False) /\ (6 = 1 -> False) /\ (6 = 7 -> False) /\ (7 = 2 -> False) /\ (... -> False) /\ (...) /\ ... /\ ...) /\ 10652 = 10652

But if we want to try solving the problem in coq, here is an approach. This is a send more money solver translated fairly verbatim from Haskell. https://blog.plover.com/prog/haskell/monad-search.html It turned out that using Int63 was much much faster than using peano nat (0.5s vs 20mins), probably because of checking the addition send + more == money

This solver isn't verified, but it does give you a way of computing the puzzle without leaving coq. Interesting question: How do make a efficient toolbox of verified finite domain solvers?

Section find_money.Open Scope int63_scope. (* Convert list of digits to number *) Definition to_number l := let fix decimal_list_aux acc l := match l with | h :: t => acc * h + decimal_list_aux (10 * acc) t | [] => 0 end in decimal_list_aux 1 (List.rev l). Definition remove d l := filter (fun x => negb (existsb (eqb x) d)) l.(* Some cute do noation syntax for lists *) Notation "x <- c1 ;; c2" := (@flat_map _ _ (fun x => c2) c1) (at level 61, c1 at next level, right associativity). Definition find_solution := let digits := [0;1;2;3;4;5;6;7;8;9] in s <- remove [0] digits;; e <- remove [s] digits;; n <- remove [s;e] digits;; d <- remove [s;e;n] digits;; let send := to_number [s;e;n;d] in m <- remove [0;s;e;n;d] digits;; o <- remove [s;e;n;d;m] digits;; r <- remove [s;e;n;d;m;o] digits;; let more := to_number [m;o;r;e] in y <- remove [s;e;n;d;m;o;r] digits;; let money := to_number [m;o;n;e;y] in if ((send + more) == money) then [(s,e,n,d,m,o,r,y)] else []. (* native_compute is the fastest evaluation method *)End find_money.

# Simple Properties of the Reals

A Z3 version:

(**python x,y,z = Reals("x y z") prove( x + y == y + x) prove( (x + y) + z == x + (y + z))s prove( x*x >= 0 ) *) Open Scope R_scope.intros; ring. Qed.forall x y : R, x + y = y + xintros; ring. Qed.forall x y z : R, x + y + z = x + (y + z)forall x : R, x > 0 \/ x = 0 \/ x < 0lra. Qed.x:Rx > 0 \/ x = 0 \/ x < 0forall x : R, x ^ 2 >= 0nra. Qed.x:Rx ^ 2 >= 0

# Simple Properties of 2D Vectors

Record V2 := { x : R; y : R }. (* vector addition *) Definition vadd v w := {| x := v.(x) + w.(x); y := v.(y) + w.(y) |}. (* scalar multiplication *) Definition smul s v := {| x := s * v.(x) ; y := s * v.(y) |}. (* dot product *) Definition dot v w := v.(x) * w.(x) + v.(y) * w.(y).forall u v w : V2, vadd u (vadd v w) = vadd (vadd u v) wu, v, w:V2vadd u (vadd v w) = vadd (vadd u v) wx0, y0, x1, y1, x2, y2:Rvadd {| x := x0; y := y0 |} (vadd {| x := x1; y := y1 |} {| x := x2; y := y2 |}) = vadd (vadd {| x := x0; y := y0 |} {| x := x1; y := y1 |}) {| x := x2; y := y2 |}f_equal; ring. Qed.x0, y0, x1, y1, x2, y2:R{| x := x0 + (x1 + x2); y := y0 + (y1 + y2) |} = {| x := x0 + x1 + x2; y := y0 + y1 + y2 |}forall u v : V2, vadd u v = vadd v uu, v:V2vadd u v = vadd v ux0, y0, x1, y1:Rvadd {| x := x0; y := y0 |} {| x := x1; y := y1 |} = vadd {| x := x1; y := y1 |} {| x := x0; y := y0 |}f_equal; ring. Qed. (* We can notice a pattern in the proofs here that we can abstract *) Ltac v2_tac := intros; repeat match goal with | [ u : V2 |- _ ] => destruct u end; cbv ; f_equal; ring.x0, y0, x1, y1:R{| x := x0 + x1; y := y0 + y1 |} = {| x := x1 + x0; y := y1 + y0 |}v2_tac. Qed. Require Import Psatz.forall (s : R) (u v : V2), smul s (vadd u v) = vadd (smul s u) (smul s v)forall u v : V2, dot u v ^ 2 <= dot v v * dot u uu, v:V2dot u v ^ 2 <= dot v v * dot u ux0, y0, x1, y1:Rdot {| x := x0; y := y0 |} {| x := x1; y := y1 |} ^ 2 <= dot {| x := x1; y := y1 |} {| x := x1; y := y1 |} * dot {| x := x0; y := y0 |} {| x := x0; y := y0 |}x0, y0, x1, y1:R(x {| x := x0; y := y0 |} * x {| x := x1; y := y1 |} + y {| x := x0; y := y0 |} * y {| x := x1; y := y1 |}) ^ 2 <= (x {| x := x1; y := y1 |} * x {| x := x1; y := y1 |} + y {| x := x1; y := y1 |} * y {| x := x1; y := y1 |}) * (x {| x := x0; y := y0 |} * x {| x := x0; y := y0 |} + y {| x := x0; y := y0 |} * y {| x := x0; y := y0 |})Abort. (* psatz R. Qed. *) (* Alectryon doesn't like this one for some reason, but it passes when run manually. *) (* We can define matrix multiplication *) Record M2 := { a : R; b : R; c : R; d : R }. Definition mmul m v := {| x := m.(a) * v.(x) + m.(b) * v.(y); y := m.(c) * v.(x) + m.(d) * v.(y) |}.x0, y0, x1, y1:R(x0 * x1 + y0 * y1) * ((x0 * x1 + y0 * y1) * 1) <= (x1 * x1 + y1 * y1) * (x0 * x0 + y0 * y0)forall (m : M2) (s : R) (v : V2), mmul m (smul s v) = smul s (mmul m v)m:M2s:Rv:V2mmul m (smul s v) = smul s (mmul m v)a0, b0, c0, d0, s, x0, y0:Rmmul {| a := a0; b := b0; c := c0; d := d0 |} (smul s {| x := x0; y := y0 |}) = smul s (mmul {| a := a0; b := b0; c := c0; d := d0 |} {| x := x0; y := y0 |})f_equal; ring. Qed. (* Update our tactic slightly to destruct the matrices also. *) Ltac m2_tac := intros; repeat match goal with | [ u : V2 |- _ ] => destruct u | [ m : M2 |- _ ] => destruct m end; cbv ; f_equal; ring.a0, b0, c0, d0, s, x0, y0:R{| x := a0 * (s * x0) + b0 * (s * y0); y := c0 * (s * x0) + d0 * (s * y0) |} = {| x := s * (a0 * x0 + b0 * y0); y := s * (c0 * x0 + d0 * y0) |}m2_tac. Qed. Close Scope R_scope.forall (m : M2) (u v : V2), mmul m (vadd u v) = vadd (mmul m u) (mmul m v)

# Summing N

Proving a closed form of the sum of 1 to n.

Fixpoint sumn n := match n with | O => O | S n' => n + sumn n' end.forall n : nat, 2 * sumn n = n * (n + 1)n:nat2 * sumn n = n * (n + 1)2 * sumn 0 = 0 * (0 + 1)n:natIHn:2 * sumn n = n * (n + 1)2 * sumn (S n) = S n * (S n + 1)n:natIHn:2 * sumn n = n * (n + 1)2 * sumn (S n) = S n * (S n + 1)ring [IHn]. Qed.n:natIHn:2 * sumn n = n * (n + 1)S (n + sumn n + S (n + sumn n + 0)) = S (n + 1 + n * S (n + 1))

# Two Sort

I like two_sort as an example. It's a sorting function that does not require induction, so for a beginner, I feel like its a nice pedagogical thing to talk about. You can find more complicated sorts proved in Vol 3 of Software Foundations https://softwarefoundations.cis.upenn.edu/vfa-current/toc.html

Definition two_sort x y := if (le_dec x y) then (x, y) else (y, x).forall x y : nat, let (x', y') := two_sort x y in x' <= y' /\ (x = x' /\ y = y' \/ y = x' /\ x = y')x, y:natlet (x', y') := two_sort x y in x' <= y' /\ (x = x' /\ y = y' \/ y = x' /\ x = y')x, y:natlet (x', y') := if le_dec x y then (x, y) else (y, x) in x' <= y' /\ (x = x' /\ y = y' \/ y = x' /\ x = y')x, y:natl:x <= yx <= y /\ (x = x /\ y = y \/ y = x /\ x = y)x, y:natn:~ x <= yy <= x /\ (x = y /\ y = x \/ y = y /\ x = x)lia. Qed.x, y:natn:~ x <= yy <= x /\ (x = y /\ y = x \/ y = y /\ x = x)