## Three idempotent rings

Show commutativity of three idempotent rings

Auteurs: Quentin Garchery

Catégories: Mathematics

Outils: Why3

see also the index (by topic, by tool, by reference, by year)

# Three idempotent rings are commutative

Author: Quentin Garchery (LRI, Université Paris-Sud)

## Definitions

```use int.Int

clone export algebra.Ring with
axiom .

let rec ghost function mul (x : t) (n : int) : t
requires { n >= 0 }
variant { n }
=
if n = 0 then pure{zero} else let r = mul x (n-1) in pure {x + r}
```

Define multiplication by an integer recursively

```clone int.Exponentiation with type t = t,
constant one = zero, function ( * ) = (+), function power = mul,
lemma .
```

We get lemmas from the why3 library

## General results about rings

First results :

```lemma simpl_left :
forall x y z. x + y = x + z -> y = z
by (-x) + (x + y) = (-x) + (x + z)

lemma simpl_right :
forall x y z. y + x = z + x -> y = z
by y + x + (-x) = z + x + (-x)

lemma zero_star_l :
forall x. zero * x = zero

lemma zero_star_r :
forall x. x * zero = zero

lemma neg_star_r :
forall x y. x * (-y) = - (x * y)
by x * y + x * (-y) = x * y + (- (x * y))

lemma neg_star_l :
forall x y. (-x) * y = - (x * y)
by x * y + (-x) * y = x * y + (- (x * y))

lemma neg_neg :
forall x. - (- x) = x

```

Lemmas about nullable elements :

```predicate null (x : t) (n : int) = mul x n = zero

lemma null_add :
forall x x' n. 0 <= n -> null x n -> null x' n -> null (x + x') n

let rec lemma mul_star_l (x y : t) (n : int)
requires { 0 <= n }
variant { n }
ensures { mul (x * y) n = (mul x n) * y }
=
if n <> 0 then mul_star_l x y (n-1)

let rec lemma mul_star_r (x y : t) (n : int)
requires { 0 <= n }
variant { n }
ensures { mul (x * y) n = x * (mul y n) }
=
if n <> 0 then mul_star_r x y (n-1)

lemma null_star_l :
forall x y n. 0 <= n -> null x n -> null (x * y) n

lemma null_star_r :
forall x y n. 0 <= n -> null y n -> null (x * y) n

lemma null_mul_congr :
forall x k km. k > 0 -> km > 0 -> null x k -> mul x (Int.(+) km k) = mul x km

```

## ThreeIdem axiom specific results

We now add the following axiom and want to prove the commutative property :

```axiom ThreeIdem : forall x. x * x * x = x

```

Split the problem in two : one where the ring has characteritic 2 and another where the ring has characteristic 3

```lemma all_null6 :
forall x. null x 6
by (x + x) * (x + x) * (x + x) = mul (x * x * x) 8
so mul x 8 = zero + x + x /\ mul x 8 = mul x 6 + x + x
```

First show that the characteristic of the ring divides 6 ...

```lemma all_split :
forall x. (exists y z. x = y + z /\ null y 2 /\ null z 3)
by let y = mul x 3 in
let z = mul (-x) 2 in
x = y + z /\ null y 2 /\ null z 3
```

... use it to show we can split the problem in two ...

```lemma free_split :
forall x. null x 2 -> null x 3 -> x = zero
```

... and show that the two problems are independent

Show the commutative property in characteristic 2 :

```lemma null_2_idem :
forall x. null x 2 -> x * x = x
by (x + x * x) * (x + x * x) = zero
so (x + x * x) * (x + x * x) * (x + x * x) = zero
so x + x * x = zero

lemma null2_comm :
forall x y. null x 2 -> null y 2 -> x * y = y * x
by (x + y) * (x + y) = x * x + y * y + x * y + y * x
so x + y = x + y + x * y + y * x

```

Show the commutative property in characteristic 3 :

```lemma swap_equality :
forall x y. null x 3 -> null y 3 ->
y * y * x + y * x * y + x * y * y = zero
by (forall x y. y * y * x + y * x * y + x * y * y +
x * x * y + x * y * x + y * x * x = zero
by ((x + y) * (x + y) * (x + y) = x * x * x + y * y * y + y * y * x +
y * x * y + x * y * y + x * x * y + x * y * x + y * x * x
so x + y + zero = x + y + (y * y * x +
y * x * y + x * y * y + x * x * y + x * y * x + y * x * x)))
so y * y * x + y * x * y + x * y * y + x * x * y + x * y * x + y * x * x = zero
so (y * y * x + y * x * y + x * y * y +
(- (x * x * y)) + (- (x * y * x)) + (- (y * x * x)) = zero
by (-y) * (-y) * x + (-y) * x * (-y) + x * (-y) * (-y) +
x * x * (-y) + x * (-y) * x + (-y) * x * x = zero)
so mul (y * y * x) 2 + mul (y * x * y) 2 + mul (x * y * y) 2 = zero
so mul (y * y * x) 4 + mul (y * x * y) 4 + mul (x * y * y) 4 = zero

lemma null3_comm :
forall x y. null x 3 -> null y 3 -> x * y = y * x
by y * x + y * y * x * y + y * x * y * y = x * y + y * y * x * y + y * x * y * y

```

Finally, combine the previous results to show the commutative property.

```lemma commutative :
forall x y. x * y = y * x
by exists x2 x3 y2 y3. x = x2 + x3 /\ y = y2 + y3 /\ null x2 2 /\ null y2 2 /\
null x3 3 /\ null y3 3
so x2 * y3 = zero /\ y3 * x2 = zero /\ x3 * y2 = zero /\ y2 * x3 = zero

```

download ZIP archive

# Why3 Proof Results for Project "three_idem_ring"

## Theory "three_idem_ring.Top": fully verified

 Obligations Alt-Ergo 2.3.0 CVC4 1.6 CVC5 1.0.5 Z3 4.11.2 VC for mul --- 0.01 --- --- Exponentiation.Assoc --- 0.01 --- --- Exponentiation.Unit_def_l --- 0.00 --- --- Exponentiation.Unit_def_r --- 0.01 --- --- Exponentiation.Power_0 --- 0.01 --- --- Exponentiation.Power_s --- 0.01 --- --- simpl_left 0.08 --- --- --- simpl_right --- 0.01 --- --- zero_star_l 0.03 --- --- --- zero_star_r 0.05 --- --- --- neg_star_r 4.80 --- --- --- neg_star_l --- --- --- --- split_vc neg_star_l.0 --- 0.01 --- --- neg_star_l.1 --- 0.01 --- --- neg_neg --- 0.01 --- --- null_add --- 0.01 --- --- VC for mul_star_l --- 0.01 --- --- VC for mul_star_r --- 0.02 --- --- null_star_l --- 0.01 --- --- null_star_r --- 0.01 --- --- null_mul_congr 0.03 --- --- --- all_null6 --- --- --- --- split_vc all_null6.0 --- --- --- 0.06 all_null6.1 --- 0.03 --- --- all_null6.2 --- 0.01 --- --- all_null6.3 --- 0.01 --- --- all_split --- --- --- --- split_vc all_split.0 --- 0.02 --- --- all_split.1 --- 0.01 --- --- all_split.2 --- 0.01 --- --- all_split.3 --- 0.02 --- --- free_split --- 0.01 --- --- null_2_idem --- --- 0.31 --- null2_comm --- 0.25 --- --- swap_equality --- --- --- --- split_vc swap_equality.0 --- --- --- 3.66 swap_equality.1 --- 0.10 --- --- swap_equality.2 --- 0.01 --- --- swap_equality.3 --- 0.02 --- --- swap_equality.4 --- 0.01 --- --- swap_equality.5 --- 3.59 --- --- swap_equality.6 --- --- --- 1.14 swap_equality.7 --- 0.09 --- --- swap_equality.8 --- 0.15 --- --- null3_comm --- --- --- --- split_vc null3_comm.0 --- 0.04 --- --- null3_comm.1 --- 0.02 --- --- commutative --- --- --- --- split_vc commutative.0 0.35 --- --- --- commutative.1 --- 0.09 --- --- commutative.2 --- 0.09 --- --- commutative.3 --- 0.08 --- --- commutative.4 --- 0.09 --- --- commutative.5 --- 0.06 --- ---