Commit b4b79ae2 authored by Quentin Garchery's avatar Quentin Garchery

ThreeIdem is only in the logic

parent f982defa
......@@ -6,29 +6,24 @@
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 ( *) = ( *),
clone export algebra.Ring with
axiom .
(** Define multiplication by an integer recursively *)
let rec function mul (x : t) (n : int) : t
let rec ghost function mul (x : t) (n : int) : t
requires { n >= 0 }
variant { n }
=
if n = 0 then zero else x + mul x (n-1)
if n = 0 then pure{zero} else let r = mul x (n-1) in pure {x + r}
(** 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 .
clone int.Exponentiation with type t = t,
constant one = zero, function ( * ) = (+), function power = mul,
lemma .
(** {2 General results about unitary rings} *)
(** {2 General results about rings} *)
(** First results : *)
......
......@@ -13,19 +13,19 @@
<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">
<goal name="Exponentiation.Assoc" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="Mul.Unit_def_l" proved="true">
<goal name="Exponentiation.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">
<goal name="Exponentiation.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">
<goal name="Exponentiation.Power_0" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="Mul.Power_s" proved="true">
<goal name="Exponentiation.Power_s" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="simpl_left" proved="true">
......@@ -67,11 +67,9 @@
<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="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="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="null_star_l" proved="true">
......@@ -143,14 +141,14 @@
<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>
<proof prover="0"><result status="valid" time="0.42"/></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="0"><result status="valid" time="2.30"/></proof>
</goal>
<goal name="swap_equality.1" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
......@@ -171,7 +169,7 @@
<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>
<proof prover="0"><result status="valid" time="0.42"/></proof>
</goal>
<goal name="swap_equality.8" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
......
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