Commit b27a12d1 authored by POLLIEN Baptiste's avatar POLLIEN Baptiste
Browse files

Update coq script

parent b158ffaa
......@@ -95,194 +95,6 @@ Axiom cdiv_closed_remainder :
(0%Z <= (b - a)%Z)%Z /\ ((b - a)%Z < n)%Z ->
((ZArith.BinInt.Z.rem a n) = (ZArith.BinInt.Z.rem b n)) -> (a = b).
(* Why3 assumption *)
Inductive S12_RealRMat_s :=
| S12_RealRMat_s1 : Reals.Rdefinitions.R -> Reals.Rdefinitions.R ->
Reals.Rdefinitions.R -> Reals.Rdefinitions.R -> Reals.Rdefinitions.R ->
Reals.Rdefinitions.R -> Reals.Rdefinitions.R -> Reals.Rdefinitions.R ->
Reals.Rdefinitions.R -> S12_RealRMat_s.
Axiom S12_RealRMat_s_WhyType : WhyType S12_RealRMat_s.
Existing Instance S12_RealRMat_s_WhyType.
(* Why3 assumption *)
Definition F12_RealRMat_s_a22 (v:S12_RealRMat_s) : Reals.Rdefinitions.R :=
match v with
| S12_RealRMat_s1 x x1 x2 x3 x4 x5 x6 x7 x8 => x8
end.
(* Why3 assumption *)
Definition F12_RealRMat_s_a21 (v:S12_RealRMat_s) : Reals.Rdefinitions.R :=
match v with
| S12_RealRMat_s1 x x1 x2 x3 x4 x5 x6 x7 x8 => x7
end.
(* Why3 assumption *)
Definition F12_RealRMat_s_a20 (v:S12_RealRMat_s) : Reals.Rdefinitions.R :=
match v with
| S12_RealRMat_s1 x x1 x2 x3 x4 x5 x6 x7 x8 => x6
end.
(* Why3 assumption *)
Definition F12_RealRMat_s_a12 (v:S12_RealRMat_s) : Reals.Rdefinitions.R :=
match v with
| S12_RealRMat_s1 x x1 x2 x3 x4 x5 x6 x7 x8 => x5
end.
(* Why3 assumption *)
Definition F12_RealRMat_s_a11 (v:S12_RealRMat_s) : Reals.Rdefinitions.R :=
match v with
| S12_RealRMat_s1 x x1 x2 x3 x4 x5 x6 x7 x8 => x4
end.
(* Why3 assumption *)
Definition F12_RealRMat_s_a10 (v:S12_RealRMat_s) : Reals.Rdefinitions.R :=
match v with
| S12_RealRMat_s1 x x1 x2 x3 x4 x5 x6 x7 x8 => x3
end.
(* Why3 assumption *)
Definition F12_RealRMat_s_a02 (v:S12_RealRMat_s) : Reals.Rdefinitions.R :=
match v with
| S12_RealRMat_s1 x x1 x2 x3 x4 x5 x6 x7 x8 => x2
end.
(* Why3 assumption *)
Definition F12_RealRMat_s_a01 (v:S12_RealRMat_s) : Reals.Rdefinitions.R :=
match v with
| S12_RealRMat_s1 x x1 x2 x3 x4 x5 x6 x7 x8 => x1
end.
(* Why3 assumption *)
Definition F12_RealRMat_s_a00 (v:S12_RealRMat_s) : Reals.Rdefinitions.R :=
match v with
| S12_RealRMat_s1 x x1 x2 x3 x4 x5 x6 x7 x8 => x
end.
(* Why3 assumption *)
Definition EqS12_RealRMat_s (S:S12_RealRMat_s) (S1:S12_RealRMat_s) : Prop :=
(((((((((F12_RealRMat_s_a00 S1) = (F12_RealRMat_s_a00 S)) /\
((F12_RealRMat_s_a01 S1) = (F12_RealRMat_s_a01 S))) /\
((F12_RealRMat_s_a02 S1) = (F12_RealRMat_s_a02 S))) /\
((F12_RealRMat_s_a10 S1) = (F12_RealRMat_s_a10 S))) /\
((F12_RealRMat_s_a11 S1) = (F12_RealRMat_s_a11 S))) /\
((F12_RealRMat_s_a12 S1) = (F12_RealRMat_s_a12 S))) /\
((F12_RealRMat_s_a20 S1) = (F12_RealRMat_s_a20 S))) /\
((F12_RealRMat_s_a21 S1) = (F12_RealRMat_s_a21 S))) /\
((F12_RealRMat_s_a22 S1) = (F12_RealRMat_s_a22 S)).
(* Why3 assumption *)
Inductive S13_RealQuat_s :=
| S13_RealQuat_s1 : Reals.Rdefinitions.R -> Reals.Rdefinitions.R ->
Reals.Rdefinitions.R -> Reals.Rdefinitions.R -> S13_RealQuat_s.
Axiom S13_RealQuat_s_WhyType : WhyType S13_RealQuat_s.
Existing Instance S13_RealQuat_s_WhyType.
(* Why3 assumption *)
Definition F13_RealQuat_s_qz (v:S13_RealQuat_s) : Reals.Rdefinitions.R :=
match v with
| S13_RealQuat_s1 x x1 x2 x3 => x3
end.
(* Why3 assumption *)
Definition F13_RealQuat_s_qy (v:S13_RealQuat_s) : Reals.Rdefinitions.R :=
match v with
| S13_RealQuat_s1 x x1 x2 x3 => x2
end.
(* Why3 assumption *)
Definition F13_RealQuat_s_qx (v:S13_RealQuat_s) : Reals.Rdefinitions.R :=
match v with
| S13_RealQuat_s1 x x1 x2 x3 => x1
end.
(* Why3 assumption *)
Definition F13_RealQuat_s_qi (v:S13_RealQuat_s) : Reals.Rdefinitions.R :=
match v with
| S13_RealQuat_s1 x x1 x2 x3 => x
end.
(* Why3 assumption *)
Definition EqS13_RealQuat_s (S:S13_RealQuat_s) (S1:S13_RealQuat_s) : Prop :=
((((F13_RealQuat_s_qi S1) = (F13_RealQuat_s_qi S)) /\
((F13_RealQuat_s_qx S1) = (F13_RealQuat_s_qx S))) /\
((F13_RealQuat_s_qy S1) = (F13_RealQuat_s_qy S))) /\
((F13_RealQuat_s_qz S1) = (F13_RealQuat_s_qz S)).
Axiom abs_def :
forall (x:Numbers.BinNums.Z),
((0%Z <= x)%Z -> ((ZArith.BinInt.Z.abs x) = x)) /\
(~ (0%Z <= x)%Z -> ((ZArith.BinInt.Z.abs x) = (-x)%Z)).
Axiom sqrt_lin1 :
forall (x:Reals.Rdefinitions.R), (1%R < x)%R ->
((Reals.R_sqrt.sqrt x) < x)%R.
Axiom sqrt_lin0 :
forall (x:Reals.Rdefinitions.R), (0%R < x)%R /\ (x < 1%R)%R ->
(x < (Reals.R_sqrt.sqrt x))%R.
Axiom sqrt_0 : ((Reals.R_sqrt.sqrt 0%R) = 0%R).
Axiom sqrt_1 : ((Reals.R_sqrt.sqrt 1%R) = 1%R).
(* Why3 assumption *)
Definition L_trace_1_ (rmat:S12_RealRMat_s) : Reals.Rdefinitions.R :=
(((F12_RealRMat_s_a00 rmat) + (F12_RealRMat_s_a11 rmat))%R +
(F12_RealRMat_s_a22 rmat))%R.
(* Why3 assumption *)
Definition L_l_FloatQuat_of_RMat_trace_pos_1_ (rmat:S12_RealRMat_s) :
S13_RealQuat_s :=
let r :=
((1%R / 2%R)%R / (Reals.R_sqrt.sqrt (1%R + (L_trace_1_ rmat))%R))%R in
S13_RealQuat_s1 ((1%R / 4%R)%R / r)%R
((((-1%R)%R * (F12_RealRMat_s_a12 rmat))%R + (F12_RealRMat_s_a21 rmat))%R *
r)%R
((((-1%R)%R * (F12_RealRMat_s_a20 rmat))%R + (F12_RealRMat_s_a02 rmat))%R *
r)%R
((((-1%R)%R * (F12_RealRMat_s_a01 rmat))%R + (F12_RealRMat_s_a10 rmat))%R *
r)%R.
(* Why3 assumption *)
Definition P_unary_quaternion_2_ (q:S13_RealQuat_s) : Prop :=
let r := F13_RealQuat_s_qi q in
let r1 := F13_RealQuat_s_qx q in
let r2 := F13_RealQuat_s_qy q in
let r3 := F13_RealQuat_s_qz q in
(((((r * r)%R + (r1 * r1)%R)%R + (r2 * r2)%R)%R + (r3 * r3)%R)%R = 1%R).
(* Why3 assumption *)
Definition L_l_RMat_of_FloatQuat_2_ (q:S13_RealQuat_s) : S12_RealRMat_s :=
let r := F13_RealQuat_s_qy q in
let r1 := (r * r)%R in
let r2 := ((-1%R)%R * r1)%R in
let r3 := F13_RealQuat_s_qz q in
let r4 := (r3 * r3)%R in
let r5 := ((-1%R)%R * r4)%R in
let r6 := F13_RealQuat_s_qi q in
let r7 := (r6 * r6)%R in
let r8 := F13_RealQuat_s_qx q in
let r9 := (r8 * r8)%R in
let r10 := (r6 * r3)%R in
let r11 := (r8 * r)%R in
let r12 := (r6 * r)%R in
let r13 := (r8 * r3)%R in
let r14 := ((-1%R)%R * r9)%R in
let r15 := (r6 * r8)%R in
let r16 := (r * r3)%R in
S12_RealRMat_s1 (((r2 + r5)%R + r7)%R + r9)%R
(2%R * (((-1%R)%R * r10)%R + r11)%R)%R (2%R * (r12 + r13)%R)%R
(2%R * (r10 + r11)%R)%R (((r14 + r5)%R + r7)%R + r1)%R
(2%R * (((-1%R)%R * r15)%R + r16)%R)%R
(2%R * (((-1%R)%R * r12)%R + r13)%R)%R (2%R * (r15 + r16)%R)%R
(((r14 + r2)%R + r7)%R + r4)%R.
Axiom Q_impl_quat_rmat :
forall (rm:S12_RealRMat_s) (q:S13_RealQuat_s),
((L_l_FloatQuat_of_RMat_trace_pos_1_ rm) = q) ->
(0%R <= (F13_RealQuat_s_qi q))%R -> (0%R < (L_trace_1_ rm))%R ->
P_unary_quaternion_2_ q -> EqS12_RealRMat_s rm (L_l_RMat_of_FloatQuat_2_ q).
(* Why3 assumption *)
Inductive addr :=
| addr'mk : Numbers.BinNums.Z -> Numbers.BinNums.Z -> addr.
......@@ -517,6 +329,81 @@ Definition P_unary_quaternion_1_ (Mf32:addr -> Reals.Rdefinitions.R)
let r3 := Mf32 (shift q 3%Z) in
(((((r * r)%R + (r1 * r1)%R)%R + (r2 * r2)%R)%R + (r3 * r3)%R)%R = 1%R).
(* Why3 assumption *)
Inductive S12_RealRMat_s :=
| S12_RealRMat_s1 : Reals.Rdefinitions.R -> Reals.Rdefinitions.R ->
Reals.Rdefinitions.R -> Reals.Rdefinitions.R -> Reals.Rdefinitions.R ->
Reals.Rdefinitions.R -> Reals.Rdefinitions.R -> Reals.Rdefinitions.R ->
Reals.Rdefinitions.R -> S12_RealRMat_s.
Axiom S12_RealRMat_s_WhyType : WhyType S12_RealRMat_s.
Existing Instance S12_RealRMat_s_WhyType.
(* Why3 assumption *)
Definition F12_RealRMat_s_a22 (v:S12_RealRMat_s) : Reals.Rdefinitions.R :=
match v with
| S12_RealRMat_s1 x x1 x2 x3 x4 x5 x6 x7 x8 => x8
end.
(* Why3 assumption *)
Definition F12_RealRMat_s_a21 (v:S12_RealRMat_s) : Reals.Rdefinitions.R :=
match v with
| S12_RealRMat_s1 x x1 x2 x3 x4 x5 x6 x7 x8 => x7
end.
(* Why3 assumption *)
Definition F12_RealRMat_s_a20 (v:S12_RealRMat_s) : Reals.Rdefinitions.R :=
match v with
| S12_RealRMat_s1 x x1 x2 x3 x4 x5 x6 x7 x8 => x6
end.
(* Why3 assumption *)
Definition F12_RealRMat_s_a12 (v:S12_RealRMat_s) : Reals.Rdefinitions.R :=
match v with
| S12_RealRMat_s1 x x1 x2 x3 x4 x5 x6 x7 x8 => x5
end.
(* Why3 assumption *)
Definition F12_RealRMat_s_a11 (v:S12_RealRMat_s) : Reals.Rdefinitions.R :=
match v with
| S12_RealRMat_s1 x x1 x2 x3 x4 x5 x6 x7 x8 => x4
end.
(* Why3 assumption *)
Definition F12_RealRMat_s_a10 (v:S12_RealRMat_s) : Reals.Rdefinitions.R :=
match v with
| S12_RealRMat_s1 x x1 x2 x3 x4 x5 x6 x7 x8 => x3
end.
(* Why3 assumption *)
Definition F12_RealRMat_s_a02 (v:S12_RealRMat_s) : Reals.Rdefinitions.R :=
match v with
| S12_RealRMat_s1 x x1 x2 x3 x4 x5 x6 x7 x8 => x2
end.
(* Why3 assumption *)
Definition F12_RealRMat_s_a01 (v:S12_RealRMat_s) : Reals.Rdefinitions.R :=
match v with
| S12_RealRMat_s1 x x1 x2 x3 x4 x5 x6 x7 x8 => x1
end.
(* Why3 assumption *)
Definition F12_RealRMat_s_a00 (v:S12_RealRMat_s) : Reals.Rdefinitions.R :=
match v with
| S12_RealRMat_s1 x x1 x2 x3 x4 x5 x6 x7 x8 => x
end.
(* Why3 assumption *)
Definition EqS12_RealRMat_s (S:S12_RealRMat_s) (S1:S12_RealRMat_s) : Prop :=
(((((((((F12_RealRMat_s_a00 S1) = (F12_RealRMat_s_a00 S)) /\
((F12_RealRMat_s_a01 S1) = (F12_RealRMat_s_a01 S))) /\
((F12_RealRMat_s_a02 S1) = (F12_RealRMat_s_a02 S))) /\
((F12_RealRMat_s_a10 S1) = (F12_RealRMat_s_a10 S))) /\
((F12_RealRMat_s_a11 S1) = (F12_RealRMat_s_a11 S))) /\
((F12_RealRMat_s_a12 S1) = (F12_RealRMat_s_a12 S))) /\
((F12_RealRMat_s_a20 S1) = (F12_RealRMat_s_a20 S))) /\
((F12_RealRMat_s_a21 S1) = (F12_RealRMat_s_a21 S))) /\
((F12_RealRMat_s_a22 S1) = (F12_RealRMat_s_a22 S)).
(* Why3 assumption *)
Definition L_mult_RealRMat (rmat1:S12_RealRMat_s) (rmat2:S12_RealRMat_s) :
S12_RealRMat_s :=
......@@ -627,6 +514,70 @@ Axiom Q_quat_of_rmat_ortho :
P_unary_quaternion_1_ Mf32 q ->
P_rotation_matrix (L_l_RMat_of_FloatQuat_1_ Mf32 q).
(* Why3 assumption *)
Inductive S13_RealQuat_s :=
| S13_RealQuat_s1 : Reals.Rdefinitions.R -> Reals.Rdefinitions.R ->
Reals.Rdefinitions.R -> Reals.Rdefinitions.R -> S13_RealQuat_s.
Axiom S13_RealQuat_s_WhyType : WhyType S13_RealQuat_s.
Existing Instance S13_RealQuat_s_WhyType.
(* Why3 assumption *)
Definition F13_RealQuat_s_qz (v:S13_RealQuat_s) : Reals.Rdefinitions.R :=
match v with
| S13_RealQuat_s1 x x1 x2 x3 => x3
end.
(* Why3 assumption *)
Definition F13_RealQuat_s_qy (v:S13_RealQuat_s) : Reals.Rdefinitions.R :=
match v with
| S13_RealQuat_s1 x x1 x2 x3 => x2
end.
(* Why3 assumption *)
Definition F13_RealQuat_s_qx (v:S13_RealQuat_s) : Reals.Rdefinitions.R :=
match v with
| S13_RealQuat_s1 x x1 x2 x3 => x1
end.
(* Why3 assumption *)
Definition F13_RealQuat_s_qi (v:S13_RealQuat_s) : Reals.Rdefinitions.R :=
match v with
| S13_RealQuat_s1 x x1 x2 x3 => x
end.
(* Why3 assumption *)
Definition EqS13_RealQuat_s (S:S13_RealQuat_s) (S1:S13_RealQuat_s) : Prop :=
((((F13_RealQuat_s_qi S1) = (F13_RealQuat_s_qi S)) /\
((F13_RealQuat_s_qx S1) = (F13_RealQuat_s_qx S))) /\
((F13_RealQuat_s_qy S1) = (F13_RealQuat_s_qy S))) /\
((F13_RealQuat_s_qz S1) = (F13_RealQuat_s_qz S)).
(* Why3 assumption *)
Definition L_l_RMat_of_FloatQuat_2_ (q:S13_RealQuat_s) : S12_RealRMat_s :=
let r := F13_RealQuat_s_qy q in
let r1 := (r * r)%R in
let r2 := ((-1%R)%R * r1)%R in
let r3 := F13_RealQuat_s_qz q in
let r4 := (r3 * r3)%R in
let r5 := ((-1%R)%R * r4)%R in
let r6 := F13_RealQuat_s_qi q in
let r7 := (r6 * r6)%R in
let r8 := F13_RealQuat_s_qx q in
let r9 := (r8 * r8)%R in
let r10 := (r6 * r3)%R in
let r11 := (r8 * r)%R in
let r12 := (r6 * r)%R in
let r13 := (r8 * r3)%R in
let r14 := ((-1%R)%R * r9)%R in
let r15 := (r6 * r8)%R in
let r16 := (r * r3)%R in
S12_RealRMat_s1 (((r2 + r5)%R + r7)%R + r9)%R
(2%R * (((-1%R)%R * r10)%R + r11)%R)%R (2%R * (r12 + r13)%R)%R
(2%R * (r10 + r11)%R)%R (((r14 + r5)%R + r7)%R + r1)%R
(2%R * (((-1%R)%R * r15)%R + r16)%R)%R
(2%R * (((-1%R)%R * r12)%R + r13)%R)%R (2%R * (r15 + r16)%R)%R
(((r14 + r2)%R + r7)%R + r4)%R.
(* Why3 assumption *)
Definition L_l_Quat_of_FloatQuat (Mf32:addr -> Reals.Rdefinitions.R)
(q:addr) : S13_RealQuat_s :=
......@@ -703,11 +654,36 @@ Axiom Q_mutliple_def_rmat_of_quat_1 :
EqS12_RealRMat_s (L_l_RMat_of_FloatQuat_1_ Mf32 q)
(L_l_RMat_of_FloatQuat_bis_1 Mf32 q).
(* Why3 assumption *)
Definition P_unary_quaternion_2_ (q:S13_RealQuat_s) : Prop :=
let r := F13_RealQuat_s_qi q in
let r1 := F13_RealQuat_s_qx q in
let r2 := F13_RealQuat_s_qy q in
let r3 := F13_RealQuat_s_qz q in
(((((r * r)%R + (r1 * r1)%R)%R + (r2 * r2)%R)%R + (r3 * r3)%R)%R = 1%R).
Axiom Q_equivalence_unary_pred :
forall (Mf32:addr -> Reals.Rdefinitions.R) (q:addr),
P_unary_quaternion_2_ (L_l_Quat_of_FloatQuat Mf32 q) <->
P_unary_quaternion_1_ Mf32 q.
Axiom abs_def :
forall (x:Numbers.BinNums.Z),
((0%Z <= x)%Z -> ((ZArith.BinInt.Z.abs x) = x)) /\
(~ (0%Z <= x)%Z -> ((ZArith.BinInt.Z.abs x) = (-x)%Z)).
Axiom sqrt_lin1 :
forall (x:Reals.Rdefinitions.R), (1%R < x)%R ->
((Reals.R_sqrt.sqrt x) < x)%R.
Axiom sqrt_lin0 :
forall (x:Reals.Rdefinitions.R), (0%R < x)%R /\ (x < 1%R)%R ->
(x < (Reals.R_sqrt.sqrt x))%R.
Axiom sqrt_0 : ((Reals.R_sqrt.sqrt 0%R) = 0%R).
Axiom sqrt_1 : ((Reals.R_sqrt.sqrt 1%R) = 1%R).
Axiom Q_mul_sqrt_4 :
forall (x:Reals.Rdefinitions.R), (0%R <= x)%R ->
((2%R * x)%R = (Reals.R_sqrt.sqrt ((4%R * x)%R * x)%R)).
......@@ -716,6 +692,24 @@ Axiom Q_mul_sqrt_float :
forall (x:Reals.Rdefinitions.R),
let r := Reals.R_sqrt.sqrt x in (0%R <= x)%R -> ((r * r)%R = x).
(* Why3 assumption *)
Definition L_trace_1_ (rmat:S12_RealRMat_s) : Reals.Rdefinitions.R :=
(((F12_RealRMat_s_a00 rmat) + (F12_RealRMat_s_a11 rmat))%R +
(F12_RealRMat_s_a22 rmat))%R.
(* Why3 assumption *)
Definition L_l_FloatQuat_of_RMat_trace_pos_1_ (rmat:S12_RealRMat_s) :
S13_RealQuat_s :=
let r :=
((1%R / 2%R)%R / (Reals.R_sqrt.sqrt (1%R + (L_trace_1_ rmat))%R))%R in
S13_RealQuat_s1 ((1%R / 4%R)%R / r)%R
((((-1%R)%R * (F12_RealRMat_s_a12 rmat))%R + (F12_RealRMat_s_a21 rmat))%R *
r)%R
((((-1%R)%R * (F12_RealRMat_s_a20 rmat))%R + (F12_RealRMat_s_a02 rmat))%R *
r)%R
((((-1%R)%R * (F12_RealRMat_s_a01 rmat))%R + (F12_RealRMat_s_a10 rmat))%R *
r)%R.
(* Why3 goal *)
Theorem wp_goal :
forall (R:S12_RealRMat_s) (R1:S13_RealQuat_s),
......@@ -743,9 +737,13 @@ rewrite H.
assert (q1 <> 0)%R.
{
unfold L_trace_1_ in H; simpl in H.
assert (1 + (a0+ a4 + a8) > 0)%R . apply Rgt_trans with (a0 + a4 + a8)%R.
unfold Rgt. rewrite Rplus_comm with (r1:=1%R). apply Rlt_plus_1.
unfold Rgt. apply H3. rewrite H in H0. intro.
assert (1 + (a0+ a4 + a8) > 0)%R .
{
apply Rgt_trans with (a0 + a4 + a8)%R.
unfold Rgt. rewrite Rplus_comm with (r1:=1%R). apply Rlt_plus_1.
unfold Rgt. apply H3.
}
rewrite H in H0. intro.
rewrite H5 in H0. ring_simplify in H0. apply Rgt_irrefl in H0. auto.
}
assert ((1 / 2 / R_sqrt.sqrt (4 * q1 * q1))= 1 / (4 * q1))%R.
......
......@@ -3,9 +3,9 @@
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 1.43 } ],
"verdict": "valid", "time": 1.03 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 5.64 } ],
"verdict": "valid", "time": 4.37 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 6.45 } ],
"verdict": "valid", "time": 4.26 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
......@@ -3,9 +3,9 @@
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 6.65 } ],
"verdict": "valid", "time": 4.54 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 6.97 } ],
"verdict": "valid", "time": 6.1 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 7.4 } ],
"verdict": "valid", "time": 5.76 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
[ { "header": "Separated", "tactic": "Wp.separated", "params": {},
[ { "prover": "script", "verdict": "valid" },
{ "header": "Separated", "tactic": "Wp.separated", "params": {},
"select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0,
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "time": 22.9451,
"verdict": "valid", "time": 13.8492,
"steps": 130 } ],
"OnLeft": [ { "prover": "Z3:4.8.6:noBV",
"verdict": "timeout", "time": 10. },
{ "prover": "Z3:4.8.6:counterexamples",
"verdict": "timeout", "time": 10. },
"verdict": "timeout", "time": 15. },
{ "prover": "Z3:4.8.6", "verdict": "timeout",
"time": 10. },
"time": 15. },
{ "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout", "time": 10. },
"verdict": "timeout", "time": 15. },
{ "prover": "Alt-Ergo:2.3.3",
"verdict": "timeout", "time": 10. },
"verdict": "timeout", "time": 15. },
{ "header": "Definition",
"tactic": "Wp.unfold", "params": {},
"select": { "select": "inside-step",
"at": 3, "kind": "have",
"occur": 0,
"target": "(P_unary_quaternion Mf32_1 q_0)",
"pattern": "P_unary_quaternion$Mf32$q" },
"children": { "Unfold 'P_unary_quaternion'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"target": "(P_unary_quaternion_1_ Mf32_1 q_0)",
"pattern": "P_unary_quaternion_1_$Mf32$q" },
"children": { "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 5.34 } ] } } ],
"time": 5.93 } ] } } ],
"OnRight": [ { "prover": "Z3:4.8.6:noBV",
"verdict": "timeout", "time": 10. },
{ "prover": "Z3:4.8.6:counterexamples",
......@@ -45,10 +48,12 @@
"select": { "select": "inside-step",
"at": 3, "kind": "have",
"occur": 0,
"target": "(P_unary_quaternion Mf32_1 q_0)",
"pattern": "P_unary_quaternion$Mf32$q" },
"children": { "Unfold 'P_unary_quaternion'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"target": "(P_unary_quaternion_1_ Mf32_1 q_0)",
"pattern": "P_unary_quaternion_1_$Mf32$q" },
"children": { "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 6.66 } ] } } ],
"time": 6.06 } ] } } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
......@@ -3,9 +3,9 @@
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 6.31 } ],
"verdict": "valid", "time": 6. } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 10.62 } ],
"verdict": "valid", "time": 9.26 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 10.07 } ],
"verdict": "valid", "time": 12.66 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
[ { "prover": "script", "verdict": "valid" },
{ "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "inside-goal", "occur": 0,
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nlet r_0 = Mf32_1[(shiftfield_F7_FloatQuat_qi q_0)] in\nlet r_1 = (2*r_0*r_0) in\nlet r_2 = Mf32_1[(shiftfield_F7_FloatQuat_qx q_0)] in\nlet r_3 = Mf32_1[(shiftfield_F7_FloatQuat_qz q_0)] in\nlet r_4 = (2*r_0*r_3) in\nlet r_5 = Mf32_1[(shiftfield_F7_FloatQuat_qy q_0)] in\nlet r_6 = (2*r_2*r_5) in\nlet r_7 = (2*r_0*r_5) in\nlet r_8 = (2*r_2*r_3) in\nlet r_9 = (2*r_0*r_2) in\nlet r_10 = (2*r_5*r_3) in\n(L_transpose\n (L_l_RMat_of_FloatRMat\n Mf32_1[(shift_float32 a_0 0)->r_1+(2*r_2*r_2)-1][(shift_float32 a_0 1)\n ->r_4+r_6][(shift_float32 a_0 2)->r_8-r_7][(shift_float32 a_0 3)\n ->r_6-r_4][(shift_float32 a_0 4)->r_1+(2*r_5*r_5)-1]\n [(shift_float32 a_0 5)->r_9+r_10][(shift_float32 a_0 6)->r_7+r_8]\n [(shift_float32 a_0 7)->r_10-r_9][(shift_float32 a_0 8)\n ->r_1+(2*r_3*r_3)-1] rm_0))",
"pattern": "L_transposeL_l_RMat_of_FloatRMat" },
......@@ -24,29 +25,11 @@
"params": {},
"select": { "select": "inside-goal",
"occur": 0,
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nlet r_0 = Mf32_1[(shiftfield_F7_FloatQuat_qi q_0)] in\nlet r_1 = (2*r_0*r_0) in\nlet r_2 = Mf32_1[(shiftfield_F7_FloatQuat_qx q_0)] in\nlet r_3 = Mf32_1[(shiftfield_F7_FloatQuat_qz q_0)] in\nlet r_4 = (2*r_0*r_3) in\nlet r_5 = Mf32_1[(shiftfield_F7_FloatQuat_qy q_0)] in\nlet r_6 = (2*r_2*r_5) in\nlet r_7 = (2*r_0*r_5) in\nlet r_8 = (2*r_2*r_3) in\nlet r_9 = (2*r_0*r_2) in\nlet r_10 = (2*r_5*r_3) in\n(L_l_RMat_of_FloatQuat\n Mf32_1[(shift_float32 a_0 0)->r_1+(2*r_2*r_2)-1][(shift_float32 a_0 1)\n ->r_4+r_6][(shift_float32 a_0 2)->r_8-r_7][(shift_float32 a_0 3)\n ->r_6-r_4][(shift_float32 a_0 4)->r_1+(2*r_5*r_5)-1]\n [(shift_float32 a_0 5)->r_9+r_10][(shift_float32 a_0 6)->r_7+r_8]\n [(shift_float32 a_0 7)->r_10-r_9][(shift_float32 a_0 8)\n ->r_1+(2*r_3*r_3)-1] q_0)",