Commit d36d163b authored by MARCHE Claude's avatar MARCHE Claude

Merge branch 'three_idem_example' into 'master'

Add the example about three-idempotent rings

See merge request !97
parents 58c2bdbb 38d26d39
(** {1 Three idempotent rings are commutative} *)
(** {2 Definitions} *)
module ThreeIdempotentRing
use int.Int
type t
val constant zero : t
val function (+) t t : t
val function ( *) t t : t
clone import algebra.Ring as R with
type t = t, constant zero = zero, function (+) = (+), function ( *) = ( *),
axiom .
(** Define multiplication by an integer recursively *)
let rec function mul (x : t) (n : int) : t
requires { n >= 0 }
variant { n }
=
if n = 0 then zero else x + mul x (n-1)
(** We get lemmas from the why3 library *)
clone import int.Exponentiation as Mul with
type t = t, constant one = zero,
function ( *) = (+), function power = mul, lemma .
(** {2 General results about unitary 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
(** {2 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 *)
(** First show that the characteristic of the ring divides 6 ... *)
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
(** ... use it to show we can split the problem in two ...*)
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
(** ... and show that the two problems are independent *)
lemma free_split :
forall x. null x 2 -> null x 3 -> x = zero
(** 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
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5">
<prover id="0" name="Z3" version="4.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="2.2.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Eprover" version="2.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="veriT" version="dev" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.6" timelimit="5" steplimit="0" memlimit="1000"/>
<file proved="true">
<path name=".."/>
<path name="three_idem_ring.mlw"/>
<theory name="ThreeIdempotentRing" proved="true">
<goal name="VC mul" expl="VC for mul" proved="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="Mul.Assoc" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="Mul.Unit_def_l" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="Mul.Unit_def_r" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="Mul.Power_0" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="Mul.Power_s" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="simpl_left" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="simpl_right" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="22"/></proof>
</goal>
<goal name="zero_star_l" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="zero_star_r" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="neg_star_r" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="neg_star_r.0" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="30"/></proof>
</goal>
<goal name="neg_star_r.1" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
</transf>
</goal>
<goal name="neg_star_l" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="neg_star_l.0" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="32"/></proof>
</goal>
<goal name="neg_star_l.1" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
</transf>
</goal>
<goal name="neg_neg" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="null_add" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC mul_star_l" expl="VC for mul_star_l" proved="true">
<proof prover="1"><result status="valid" time="1.02" steps="108"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC mul_star_r" expl="VC for mul_star_r" proved="true">
<proof prover="1"><result status="valid" time="3.46" steps="124"/></proof>
<proof prover="3"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="null_star_l" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="24"/></proof>
</goal>
<goal name="null_star_r" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="28"/></proof>
</goal>
<goal name="null_mul_congr" proved="true">
<proof prover="1" timelimit="1"><result status="valid" time="0.05" steps="20"/></proof>
</goal>
<goal name="all_null6" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="all_null6.0" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="all_null6.1" proved="true">
<proof prover="1"><result status="valid" time="0.04" steps="4"/></proof>
</goal>
<goal name="all_null6.2" proved="true">
<proof prover="1"><result status="valid" time="0.17" steps="4"/></proof>
</goal>
<goal name="all_null6.3" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
</transf>
</goal>
<goal name="all_split" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="all_split.0" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="all_split.1" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="all_split.2" proved="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="all_split.3" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
<goal name="free_split" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="null_2_idem" proved="true">
<transf name="split_vc" proved="true" >
<goal name="null_2_idem.0" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="null_2_idem.1" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="null_2_idem.2" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="null_2_idem.3" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
<goal name="null2_comm" proved="true">
<transf name="split_vc" proved="true" >
<goal name="null2_comm.0" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="null2_comm.1" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="null2_comm.2" proved="true">
<proof prover="0"><result status="valid" time="0.22"/></proof>
</goal>
</transf>
</goal>
<goal name="swap_equality" proved="true">
<transf name="split_vc" proved="true" >
<goal name="swap_equality.0" proved="true">
<proof prover="0"><result status="valid" time="1.57"/></proof>
<proof prover="3"><result status="valid" time="0.55"/></proof>
</goal>
<goal name="swap_equality.1" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="swap_equality.2" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="swap_equality.3" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="swap_equality.4" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="swap_equality.5" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="swap_equality.6" proved="true">
<proof prover="0"><result status="valid" time="0.35"/></proof>
</goal>
<goal name="swap_equality.7" proved="true">
<proof prover="0"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="swap_equality.8" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="null3_comm" proved="true">
<transf name="split_vc" proved="true" >
<goal name="null3_comm.0" proved="true">
<proof prover="0"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="null3_comm.1" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
<goal name="commutative" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="commutative.0" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="commutative.1" proved="true">
<proof prover="0"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="commutative.2" proved="true">
<proof prover="0"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="commutative.3" proved="true">
<proof prover="0"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="commutative.4" proved="true">
<proof prover="0"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="commutative.5" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment