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

Update Coq script

parent b27a12d1
...@@ -16,6 +16,8 @@ Require real.FromInt. ...@@ -16,6 +16,8 @@ Require real.FromInt.
Require real.Square. Require real.Square.
Require map.Map. Require map.Map.
Local Open Scope R_scope.
Parameter eqb: Parameter eqb:
forall {a:Type} {a_WT:WhyType a}, a -> a -> Init.Datatypes.bool. forall {a:Type} {a_WT:WhyType a}, a -> a -> Init.Datatypes.bool.
...@@ -710,6 +712,10 @@ Definition L_l_FloatQuat_of_RMat_trace_pos_1_ (rmat:S12_RealRMat_s) : ...@@ -710,6 +712,10 @@ Definition L_l_FloatQuat_of_RMat_trace_pos_1_ (rmat:S12_RealRMat_s) :
((((-1%R)%R * (F12_RealRMat_s_a01 rmat))%R + (F12_RealRMat_s_a10 rmat))%R * ((((-1%R)%R * (F12_RealRMat_s_a01 rmat))%R + (F12_RealRMat_s_a10 rmat))%R *
r)%R. r)%R.
Require Import Lra.
Local Open Scope R_scope.
(* Why3 goal *) (* Why3 goal *)
Theorem wp_goal : Theorem wp_goal :
forall (R:S12_RealRMat_s) (R1:S13_RealQuat_s), forall (R:S12_RealRMat_s) (R1:S13_RealQuat_s),
...@@ -719,56 +725,35 @@ Theorem wp_goal : ...@@ -719,56 +725,35 @@ Theorem wp_goal :
(* Why3 intros R R1 h1 h2 h3 h4. *) (* Why3 intros R R1 h1 h2 h3 h4. *)
Proof. Proof.
intros Rm Q H1 H2 H3 H4. intros Rm Q H1 H2 H3 H4.
destruct Rm as [a0 a1 a2 a3 a4 a5 a6 a7 a8]. destruct Q as[q1 q2 q3 q4]. destruct Rm as [a0 a1 a2 a3 a4 a5 a6 a7 a8].
destruct Q as[q1 q2 q3 q4].
unfold L_l_RMat_of_FloatQuat_2_ in H1; simpl in H1. unfold L_l_RMat_of_FloatQuat_2_ in H1; simpl in H1.
unfold F13_RealQuat_s_qi in H2; simpl in H2. unfold F13_RealQuat_s_qi in H2; simpl in H2.
unfold L_trace_1_ in H3; simpl in H3. unfold L_trace_1_ in H3; simpl in H3.
unfold P_unary_quaternion_2_ in H4; simpl in H4. unfold P_unary_quaternion_2_ in H4; simpl in H4.
unfold L_l_FloatQuat_of_RMat_trace_pos_1_; simpl. unfold L_l_FloatQuat_of_RMat_trace_pos_1_; simpl.
assert (1 + L_trace_1_ (S12_RealRMat_s1 a0 a1 a2 a3 a4 a5 a6 a7 a8) = 4 * q1 * q1)%R. assert (1 + L_trace_1_ (S12_RealRMat_s1 a0 a1 a2 a3 a4 a5 a6 a7 a8) = 4 * q1 * q1).
{ {
unfold L_trace_1_; simpl. unfold L_trace_1_; simpl.
rewrite <- H4. rewrite <- H4.
inversion H1. inversion H1.
ring_simplify. lra.
auto.
} }
rewrite H. rewrite H.
assert (q1 <> 0)%R. assert (H0 : q1 <> 0).
{ {
unfold L_trace_1_ in H; simpl in H. unfold L_trace_1_ in H; simpl in H.
assert (1 + (a0+ a4 + a8) > 0)%R . assert (H0 : 1 + (a0+ a4 + a8) > 0) by lra.
{ intro H5.
apply Rgt_trans with (a0 + a4 + a8)%R. rewrite H, H5 in H0.
unfold Rgt. rewrite Rplus_comm with (r1:=1%R). apply Rlt_plus_1. lra.
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. assert (H5 : (1 / 2 / R_sqrt.sqrt (4 * q1 * q1))= 1 / (4 * q1)).
{ {
unfold Rdiv. rewrite <- Q_mul_sqrt_4; auto. unfold Rdiv; rewrite <- Q_mul_sqrt_4; auto.
ring_simplify. rewrite <- Rinv_mult_distr; auto. now field.
rewrite <- Rmult_assoc. assert (2 * 2 = 4); auto.
} }
rewrite H5. unfold EqS13_RealQuat_s; simpl. rewrite H5; unfold EqS13_RealQuat_s; simpl.
repeat split. now inversion H1; repeat split; field.
- rewrite Real.assoc_div_div.
* unfold Rdiv. simpl. ring_simplify. rewrite RMicromega.Rinv_1. apply Rinv_r_simpl_r.
auto.
* split; auto.
- inversion H1. ring_simplify. unfold Rdiv. ring_simplify.
rewrite Rmult_assoc. rewrite Rmult_comm with (r1:=q2). rewrite <- Rmult_assoc.
rewrite <- Rinv_r_sym. ring_simplify; auto. apply Rmult_integral_contrapositive.
auto.
- inversion H1. ring_simplify. unfold Rdiv. ring_simplify.
rewrite Rmult_assoc. rewrite Rmult_comm with (r1:=q3). rewrite <- Rmult_assoc.
rewrite <- Rinv_r_sym. ring_simplify; auto. apply Rmult_integral_contrapositive.
auto.
- inversion H1. ring_simplify. unfold Rdiv. ring_simplify.
rewrite Rmult_assoc. rewrite Rmult_comm with (r1:=q4). rewrite <- Rmult_assoc.
rewrite <- Rinv_r_sym. ring_simplify; auto. apply Rmult_integral_contrapositive.
auto.
Qed. Qed.
...@@ -89,5 +89,5 @@ ...@@ -89,5 +89,5 @@
{ "Unfold 'L_l_RMat_of_FloatRMat'": { "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "prover": "Alt-Ergo:2.3.3", [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "verdict": "valid",
"time": 1.4008, "time": 1.2982,
"steps": 989 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] "steps": 989 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
...@@ -36,5 +36,5 @@ ...@@ -36,5 +36,5 @@
{ "Unfold 'L_trace_2_'": { "Unfold 'L_trace_2_'":
[ { "prover": "Alt-Ergo:2.3.3", [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "verdict": "valid",
"time": 3.0561, "time": 2.6921,
"steps": 1279 } ] } } ] } } ] } } ] } } ] "steps": 1249 } ] } } ] } } ] } } ] } } ]
...@@ -58,8 +58,8 @@ ...@@ -58,8 +58,8 @@
{ "Unfold 'L_l_FloatQuat_of_RMat_2_max_1_'": { "Unfold 'L_l_FloatQuat_of_RMat_2_max_1_'":
[ { "prover": "Alt-Ergo:2.3.3", [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "verdict": "valid",
"time": 2.6935, "time": 1.7844,
"steps": 1025 }, "steps": 1008 },
{ "header": "Definition", { "header": "Definition",
"tactic": "Wp.unfold", "tactic": "Wp.unfold",
"params": {}, "params": {},
......
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {}, [ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0, "select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0,
"target": "(L_l_RMat_of_FloatRMat Mf32_5 rm_0)", "target": "(L_l_RMat_of_FloatRMat Mf32_1 rm_0)",
"pattern": "L_l_RMat_of_FloatRMat$Mf32$rm" }, "pattern": "L_l_RMat_of_FloatRMat$Mf32$rm" },
"children": { "Unfold 'L_l_RMat_of_FloatRMat'": [ { "header": "Definition", "children": { "Unfold 'L_l_RMat_of_FloatRMat'": [ { "header": "Definition",
"tactic": "Wp.unfold", "tactic": "Wp.unfold",
...@@ -9,7 +9,7 @@ ...@@ -9,7 +9,7 @@
"at": 2, "at": 2,
"kind": "have", "kind": "have",
"occur": 0, "occur": 0,
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\n(P_rotation_matrix\n {\n F12_RealRMat_s_a00 = Mf32_5[(shift_float32 a_0 0)] ;\n F12_RealRMat_s_a01 = Mf32_5[(shift_float32 a_0 1)] ;\n F12_RealRMat_s_a02 = Mf32_5[(shift_float32 a_0 2)] ;\n F12_RealRMat_s_a10 = Mf32_5[(shift_float32 a_0 3)] ;\n F12_RealRMat_s_a11 = Mf32_5[(shift_float32 a_0 4)] ;\n F12_RealRMat_s_a12 = Mf32_5[(shift_float32 a_0 5)] ;\n F12_RealRMat_s_a20 = Mf32_5[(shift_float32 a_0 6)] ;\n F12_RealRMat_s_a21 = Mf32_5[(shift_float32 a_0 7)] ;\n F12_RealRMat_s_a22 = Mf32_5[(shift_float32 a_0 8)]\n })", "target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\n(P_rotation_matrix\n {\n F12_RealRMat_s_a00 = Mf32_1[(shift_float32 a_0 0)] ;\n F12_RealRMat_s_a01 = Mf32_1[(shift_float32 a_0 1)] ;\n F12_RealRMat_s_a02 = Mf32_1[(shift_float32 a_0 2)] ;\n F12_RealRMat_s_a10 = Mf32_1[(shift_float32 a_0 3)] ;\n F12_RealRMat_s_a11 = Mf32_1[(shift_float32 a_0 4)] ;\n F12_RealRMat_s_a12 = Mf32_1[(shift_float32 a_0 5)] ;\n F12_RealRMat_s_a20 = Mf32_1[(shift_float32 a_0 6)] ;\n F12_RealRMat_s_a21 = Mf32_1[(shift_float32 a_0 7)] ;\n F12_RealRMat_s_a22 = Mf32_1[(shift_float32 a_0 8)]\n })",
"pattern": "P_rotation_matrix{RealRMat_s}[][]" }, "pattern": "P_rotation_matrix{RealRMat_s}[][]" },
"children": { "Unfold 'P_rotation_matrix'": "children": { "Unfold 'P_rotation_matrix'":
[ { "header": "Definition", [ { "header": "Definition",
...@@ -20,7 +20,7 @@ ...@@ -20,7 +20,7 @@
"at": 2, "at": 2,
"kind": "have", "kind": "have",
"occur": 0, "occur": 0,
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\n(L_transpose\n {\n F12_RealRMat_s_a00 = Mf32_5[(shift_float32 a_0 0)] ;\n F12_RealRMat_s_a01 = Mf32_5[(shift_float32 a_0 1)] ;\n F12_RealRMat_s_a02 = Mf32_5[(shift_float32 a_0 2)] ;\n F12_RealRMat_s_a10 = Mf32_5[(shift_float32 a_0 3)] ;\n F12_RealRMat_s_a11 = Mf32_5[(shift_float32 a_0 4)] ;\n F12_RealRMat_s_a12 = Mf32_5[(shift_float32 a_0 5)] ;\n F12_RealRMat_s_a20 = Mf32_5[(shift_float32 a_0 6)] ;\n F12_RealRMat_s_a21 = Mf32_5[(shift_float32 a_0 7)] ;\n F12_RealRMat_s_a22 = Mf32_5[(shift_float32 a_0 8)]\n })", "target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\n(L_transpose\n {\n F12_RealRMat_s_a00 = Mf32_1[(shift_float32 a_0 0)] ;\n F12_RealRMat_s_a01 = Mf32_1[(shift_float32 a_0 1)] ;\n F12_RealRMat_s_a02 = Mf32_1[(shift_float32 a_0 2)] ;\n F12_RealRMat_s_a10 = Mf32_1[(shift_float32 a_0 3)] ;\n F12_RealRMat_s_a11 = Mf32_1[(shift_float32 a_0 4)] ;\n F12_RealRMat_s_a12 = Mf32_1[(shift_float32 a_0 5)] ;\n F12_RealRMat_s_a20 = Mf32_1[(shift_float32 a_0 6)] ;\n F12_RealRMat_s_a21 = Mf32_1[(shift_float32 a_0 7)] ;\n F12_RealRMat_s_a22 = Mf32_1[(shift_float32 a_0 8)]\n })",
"pattern": "L_transpose{RealRMat_s}[][][][][]" }, "pattern": "L_transpose{RealRMat_s}[][][][][]" },
"children": "children":
{ "Unfold 'L_transpose'": { "Unfold 'L_transpose'":
...@@ -32,37 +32,91 @@ ...@@ -32,37 +32,91 @@
"at": 2, "at": 2,
"kind": "have", "kind": "have",
"occur": 0, "occur": 0,
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nlet r_0 = Mf32_5[(shift_float32 a_0 0)] in\nlet r_1 = Mf32_5[(shift_float32 a_0 1)] in\nlet r_2 = Mf32_5[(shift_float32 a_0 2)] in\nlet r_3 = Mf32_5[(shift_float32 a_0 3)] in\nlet r_4 = Mf32_5[(shift_float32 a_0 4)] in\nlet r_5 = Mf32_5[(shift_float32 a_0 5)] in\nlet r_6 = Mf32_5[(shift_float32 a_0 6)] in\nlet r_7 = Mf32_5[(shift_float32 a_0 7)] in\nlet r_8 = Mf32_5[(shift_float32 a_0 8)] in\n(L_mult_RealRMat\n {\n F12_RealRMat_s_a00 = r_0 ;\n F12_RealRMat_s_a01 = r_1 ;\n F12_RealRMat_s_a02 = r_2 ;\n F12_RealRMat_s_a10 = r_3 ;\n F12_RealRMat_s_a11 = r_4 ;\n F12_RealRMat_s_a12 = r_5 ;\n F12_RealRMat_s_a20 = r_6 ;\n F12_RealRMat_s_a21 = r_7 ;\n F12_RealRMat_s_a22 = r_8\n }\n {\n F12_RealRMat_s_a00 = r_0 ;\n F12_RealRMat_s_a01 = r_3 ;\n F12_RealRMat_s_a02 = r_6 ;\n F12_RealRMat_s_a10 = r_1 ;\n F12_RealRMat_s_a11 = r_4 ;\n F12_RealRMat_s_a12 = r_7 ;\n F12_RealRMat_s_a20 = r_2 ;\n F12_RealRMat_s_a21 = r_5 ;\n F12_RealRMat_s_a22 = r_8\n })", "target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nlet r_0 = Mf32_1[(shift_float32 a_0 0)] in\nlet r_1 = Mf32_1[(shift_float32 a_0 1)] in\nlet r_2 = Mf32_1[(shift_float32 a_0 2)] in\nlet r_3 = Mf32_1[(shift_float32 a_0 3)] in\nlet r_4 = Mf32_1[(shift_float32 a_0 4)] in\nlet r_5 = Mf32_1[(shift_float32 a_0 5)] in\nlet r_6 = Mf32_1[(shift_float32 a_0 6)] in\nlet r_7 = Mf32_1[(shift_float32 a_0 7)] in\nlet r_8 = Mf32_1[(shift_float32 a_0 8)] in\n(L_mult_RealRMat\n {\n F12_RealRMat_s_a00 = r_0 ;\n F12_RealRMat_s_a01 = r_1 ;\n F12_RealRMat_s_a02 = r_2 ;\n F12_RealRMat_s_a10 = r_3 ;\n F12_RealRMat_s_a11 = r_4 ;\n F12_RealRMat_s_a12 = r_5 ;\n F12_RealRMat_s_a20 = r_6 ;\n F12_RealRMat_s_a21 = r_7 ;\n F12_RealRMat_s_a22 = r_8\n }\n {\n F12_RealRMat_s_a00 = r_0 ;\n F12_RealRMat_s_a01 = r_3 ;\n F12_RealRMat_s_a02 = r_6 ;\n F12_RealRMat_s_a10 = r_1 ;\n F12_RealRMat_s_a11 = r_4 ;\n F12_RealRMat_s_a12 = r_7 ;\n F12_RealRMat_s_a20 = r_2 ;\n F12_RealRMat_s_a21 = r_5 ;\n F12_RealRMat_s_a22 = r_8\n })",
"pattern": "L_mult_RealRMat{RealRMat_s}{RealRMat_s}" }, "pattern": "L_mult_RealRMat{RealRMat_s}{RealRMat_s}" },
"children": "children":
{ "Unfold 'L_mult_RealRMat'": { "Unfold 'L_mult_RealRMat'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples", [ { "header": "Split",
"tactic": "Wp.split",
"params": {},
"select":
{ "select": "clause-step",
"at": 8,
"kind": "branch",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\n0<\n(Mf32_1[(shift_float32 a_0 0)]+Mf32_1[(shift_float32 a_0 4)]+\n Mf32_1[(shift_float32 a_0 8)])",
"pattern": "<0+[][][]$Mf32shift_float32$Mf32" },
"children":
{ "Then":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid", "verdict": "valid",
"time": 0.24 }, "time": 0.29,
{ "header": "Definition", "steps": 429570 } ],
"tactic": "Wp.unfold", "Else":
[ { "header": "Split",
"tactic": "Wp.split",
"params": {}, "params": {},
"select": "select":
{ "select": "inside-step", { "select": "clause-step",
"at": 4, "at": 10,
"kind": "have", "kind": "branch",
"occur": 0, "target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nMf32_1[(shift_float32 a_0 4)]<Mf32_1[(shift_float32 a_0 0)]",
"target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\nlet r_0 = Mf32_6[(shift_float32 a_0 0)] in\nlet r_1 = Mf32_6[(shift_float32 a_0 1)] in\nlet r_2 = Mf32_6[(shift_float32 a_0 2)] in\nlet r_3 = Mf32_6[(shift_float32 a_0 3)] in\nlet r_4 = Mf32_6[(shift_float32 a_0 4)] in\nlet r_5 = Mf32_6[(shift_float32 a_0 5)] in\nlet r_6 = ((r_0*r_3)+(r_1*r_4)+(r_2*r_5)) in\nlet r_7 = Mf32_6[(shift_float32 a_0 6)] in\nlet r_8 = Mf32_6[(shift_float32 a_0 7)] in\nlet r_9 = Mf32_6[(shift_float32 a_0 8)] in\nlet r_10 = ((r_0*r_7)+(r_1*r_8)+(r_2*r_9)) in\nlet r_11 = ((r_3*r_7)+(r_4*r_8)+(r_5*r_9)) in\n(EqS9_RealRMat_s\n {\n F9_RealRMat_s_a00 = (r_0*r_0)+(r_1*r_1)+(r_2*r_2) ;\n F9_RealRMat_s_a01 = r_6 ;\n F9_RealRMat_s_a02 = r_10 ;\n F9_RealRMat_s_a10 = r_6 ;\n F9_RealRMat_s_a11 = (r_3*r_3)+(r_4*r_4)+(r_5*r_5) ;\n F9_RealRMat_s_a12 = r_11 ;\n F9_RealRMat_s_a20 = r_10 ;\n F9_RealRMat_s_a21 = r_11 ;\n F9_RealRMat_s_a22 = (r_7*r_7)+(r_8*r_8)+(r_9*r_9)\n } L_id_rmat)", "pattern": "<[][]$Mf32shift_float32$Mf32shift_float32" },
"pattern": "EqS9_RealRMat_s{RealRMat_s}L_id_rmat" },
"children": "children":
{ "Unfold 'EqS9_RealRMat_s'": { "Then":
[ { "header": "Definition", [ { "header": "Split",
"tactic": "Wp.unfold", "tactic": "Wp.split",
"params": {}, "params": {},
"select": "select":
{ "select": "inside-step", { "select": "clause-step",
"at": 4, "at": 12,
"kind": "have", "kind": "branch",
"occur": 0, "target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nMf32_1[(shift_float32 a_0 8)]<Mf32_1[(shift_float32 a_0 0)]",
"target": "L_id_rmat", "pattern": "<[][]$Mf32shift_float32$Mf32shift_float32" },
"pattern": "L_id_rmat" }, "children":
{ "Then":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.32,
"steps": 394374 } ],
"Else":
[ { "header": "Split",
"tactic": "Wp.split",
"params": {},
"select":
{ "select": "clause-step",
"at": 16,
"kind": "branch",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nMf32_1[(shift_float32 a_0 8)]<Mf32_1[(shift_float32 a_0 4)]",
"pattern": "<[][]$Mf32shift_float32$Mf32shift_float32" },
"children": "children":
{ "Unfold 'L_id_rmat'": { "Then":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples", [ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.04,
"steps": 207345 } ],
"Else":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.49,
"steps": 393035 } ] } } ] } } ],
"Else":
[ { "header": "Split",
"tactic": "Wp.split",
"params": {},
"select":
{ "select": "clause-step",
"at": 13,
"kind": "branch",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nMf32_1[(shift_float32 a_0 8)]<Mf32_1[(shift_float32 a_0 4)]",
"pattern": "<[][]$Mf32shift_float32$Mf32shift_float32" },
"children":
{ "Then":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.29,
"steps": 393824 } ],
"Else":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid", "verdict": "valid",
"time": 0.27 } ] } } ] } } ] } } ] } } ] } } ] } } ] "time": 0.5,
"steps": 390520 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {}, [ { "header": "Filter", "tactic": "Wp.filter", "params": { "anti": false },
"select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0, "select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0,
"target": "(L_l_RMat_of_FloatRMat Mf32_5 rm_0)", "target": "(P_rotation_matrix (L_l_RMat_of_FloatRMat Mf32_1 rm_0))",
"pattern": "L_l_RMat_of_FloatRMat$Mf32$rm" }, "pattern": "P_rotation_matrixL_l_RMat_of_FloatRMat" },
"children": { "Unfold 'L_l_RMat_of_FloatRMat'": [ { "header": "Definition", "children": { "Filter": [ { "prover": "Alt-Ergo:2.3.3",
"tactic": "Wp.unfold", "verdict": "valid", "time": 4.7786,
"params": {}, "steps": 1623 } ] } } ]
"select": { "select": "inside-step",
"at": 2,
"kind": "have",
"occur": 0,
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\n(P_rotation_matrix\n {\n F12_RealRMat_s_a00 = Mf32_5[(shift_float32 a_0 0)] ;\n F12_RealRMat_s_a01 = Mf32_5[(shift_float32 a_0 1)] ;\n F12_RealRMat_s_a02 = Mf32_5[(shift_float32 a_0 2)] ;\n F12_RealRMat_s_a10 = Mf32_5[(shift_float32 a_0 3)] ;\n F12_RealRMat_s_a11 = Mf32_5[(shift_float32 a_0 4)] ;\n F12_RealRMat_s_a12 = Mf32_5[(shift_float32 a_0 5)] ;\n F12_RealRMat_s_a20 = Mf32_5[(shift_float32 a_0 6)] ;\n F12_RealRMat_s_a21 = Mf32_5[(shift_float32 a_0 7)] ;\n F12_RealRMat_s_a22 = Mf32_5[(shift_float32 a_0 8)]\n })",
"pattern": "P_rotation_matrix{RealRMat_s}[][]" },
"children": { "Unfold 'P_rotation_matrix'":
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "inside-step",
"at": 2,
"kind": "have",
"occur": 0,
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\n(L_transpose\n {\n F12_RealRMat_s_a00 = Mf32_5[(shift_float32 a_0 0)] ;\n F12_RealRMat_s_a01 = Mf32_5[(shift_float32 a_0 1)] ;\n F12_RealRMat_s_a02 = Mf32_5[(shift_float32 a_0 2)] ;\n F12_RealRMat_s_a10 = Mf32_5[(shift_float32 a_0 3)] ;\n F12_RealRMat_s_a11 = Mf32_5[(shift_float32 a_0 4)] ;\n F12_RealRMat_s_a12 = Mf32_5[(shift_float32 a_0 5)] ;\n F12_RealRMat_s_a20 = Mf32_5[(shift_float32 a_0 6)] ;\n F12_RealRMat_s_a21 = Mf32_5[(shift_float32 a_0 7)] ;\n F12_RealRMat_s_a22 = Mf32_5[(shift_float32 a_0 8)]\n })",
"pattern": "L_transpose{RealRMat_s}[][][][][]" },
"children":
{ "Unfold 'L_transpose'":
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "inside-step",
"at": 2,
"kind": "have",
"occur": 0,
"target": "L_id_rmat",
"pattern": "L_id_rmat" },
"children":
{ "Unfold 'L_id_rmat'":
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "inside-step",
"at": 2,
"kind": "have",
"occur": 0,
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nlet r_0 = Mf32_5[(shift_float32 a_0 0)] in\nlet r_1 = Mf32_5[(shift_float32 a_0 1)] in\nlet r_2 = Mf32_5[(shift_float32 a_0 2)] in\nlet r_3 = Mf32_5[(shift_float32 a_0 3)] in\nlet r_4 = Mf32_5[(shift_float32 a_0 4)] in\nlet r_5 = Mf32_5[(shift_float32 a_0 5)] in\nlet r_6 = Mf32_5[(shift_float32 a_0 6)] in\nlet r_7 = Mf32_5[(shift_float32 a_0 7)] in\nlet r_8 = Mf32_5[(shift_float32 a_0 8)] in\n(L_mult_RealRMat\n {\n F12_RealRMat_s_a00 = r_0 ;\n F12_RealRMat_s_a01 = r_1 ;\n F12_RealRMat_s_a02 = r_2 ;\n F12_RealRMat_s_a10 = r_3 ;\n F12_RealRMat_s_a11 = r_4 ;\n F12_RealRMat_s_a12 = r_5 ;\n F12_RealRMat_s_a20 = r_6 ;\n F12_RealRMat_s_a21 = r_7 ;\n F12_RealRMat_s_a22 = r_8\n }\n {\n F12_RealRMat_s_a00 = r_0 ;\n F12_RealRMat_s_a01 = r_3 ;\n F12_RealRMat_s_a02 = r_6 ;\n F12_RealRMat_s_a10 = r_1 ;\n F12_RealRMat_s_a11 = r_4 ;\n F12_RealRMat_s_a12 = r_7 ;\n F12_RealRMat_s_a20 = r_2 ;\n F12_RealRMat_s_a21 = r_5 ;\n F12_RealRMat_s_a22 = r_8\n })",
"pattern": "L_mult_RealRMat{RealRMat_s}{RealRMat_s}" },
"children":
{ "Unfold 'L_mult_RealRMat'":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.52,
"steps": 579112 },
{ "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "inside-step",
"at": 4,
"kind": "have",
"occur": 0,
"target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\nlet r_0 = Mf32_6[(shift_float32 a_0 0)] in\nlet r_1 = Mf32_6[(shift_float32 a_0 1)] in\nlet r_2 = Mf32_6[(shift_float32 a_0 2)] in\nlet r_3 = Mf32_6[(shift_float32 a_0 3)] in\nlet r_4 = Mf32_6[(shift_float32 a_0 4)] in\nlet r_5 = Mf32_6[(shift_float32 a_0 5)] in\nlet r_6 = ((r_0*r_3)+(r_1*r_4)+(r_2*r_5)) in\nlet r_7 = Mf32_6[(shift_float32 a_0 6)] in\nlet r_8 = Mf32_6[(shift_float32 a_0 7)] in\nlet r_9 = Mf32_6[(shift_float32 a_0 8)] in\nlet r_10 = ((r_0*r_7)+(r_1*r_8)+(r_2*r_9)) in\nlet r_11 = ((r_3*r_7)+(r_4*r_8)+(r_5*r_9)) in\n(EqS9_RealRMat_s\n {\n F9_RealRMat_s_a00 = (r_0*r_0)+(r_1*r_1)+(r_2*r_2) ;\n F9_RealRMat_s_a01 = r_6 ;\n F9_RealRMat_s_a02 = r_10 ;\n F9_RealRMat_s_a10 = r_6 ;\n F9_RealRMat_s_a11 = (r_3*r_3)+(r_4*r_4)+(r_5*r_5) ;\n F9_RealRMat_s_a12 = r_11 ;\n F9_RealRMat_s_a20 = r_10 ;\n F9_RealRMat_s_a21 = r_11 ;\n F9_RealRMat_s_a22 = (r_7*r_7)+(r_8*r_8)+(r_9*r_9)\n }\n {\n F9_RealRMat_s_a00 = 1 ;\n F9_RealRMat_s_a01 = 0 ;\n F9_RealRMat_s_a02 = 0 ;\n F9_RealRMat_s_a10 = 0 ;\n F9_RealRMat_s_a11 = 1 ;\n F9_RealRMat_s_a12 = 0 ;\n F9_RealRMat_s_a20 = 0 ;\n F9_RealRMat_s_a21 = 0 ;\n F9_RealRMat_s_a22 = 1\n })",
"pattern": "EqS9_RealRMat_s{RealRMat_s}{RealRMat_s}" },
"children":
{ "Unfold 'EqS9_RealRMat_s'":
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 1.6,
"steps": 3136482 } ] } } ] } } ] } } ] } } ] } } ] } } ]
...@@ -79,5 +79,5 @@ ...@@ -79,5 +79,5 @@
{ "Unfold 'EqS13_RealQuat_s'": { "Unfold 'EqS13_RealQuat_s'":
[ { "prover": "Alt-Ergo:2.3.3", [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "verdict": "valid",
"time": 8.962, "time": 9.2189,
"steps": 4656 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] "steps": 4599 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
...@@ -59,30 +59,30 @@ ...@@ -59,30 +59,30 @@
{ "Goal 1/6": { "Goal 1/6":
[ { "prover": "Alt-Ergo:2.3.3", [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "verdict": "valid",
"time": 2.0136, "time": 1.5198,
"steps": 102 } ], "steps": 102 } ],
"Goal 2/6": "Goal 2/6":
[ { "prover": "Z3:4.8.6:counterexamples", [ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid", "verdict": "valid",
"time": 0.04, "time": 0.03,
"steps": 61443 } ], "steps": 65603 } ],
"Goal 3/6": "Goal 3/6":
[ { "prover": "Z3:4.8.6:counterexamples", [ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid", "verdict": "valid",
"time": 0.06, "time": 0.05,
"steps": 61451 } ], "steps": 65611 } ],
"Goal 4/6": "Goal 4/6":
[ { "prover": "Alt-Ergo:2.3.3", [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "verdict": "valid",
"time": 2.6631, "time": 2.4062,
"steps": 102 } ], "steps": 102 } ],
"Goal 5/6": "Goal 5/6":
[ { "prover": "Alt-Ergo:2.3.3", [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "verdict": "valid",
"time": 2.8373, "time": 1.7948,
"steps": 102 } ], "steps": 102 } ],
"Goal 6/6": "Goal 6/6":
[ { "prover": "Alt-Ergo:2.3.3", [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "verdict": "valid",
"time": 2.1805, "time": 1.6473,
"steps": 102 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] "steps": 102 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
[ { "prover": "Z3:4.8.6:noBV", "verdict": "timeout", "time": 15. }, [ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
{ "prover": "Z3:4.8.6:counterexamples", "verdict": "timeout", "time": 15. },
{ "prover": "Z3:4.8.6", "verdict": "timeout", "time": 15. },
{ "prover": "Coq:8.12.2", "verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout", "time": 15. },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "timeout", "time": 15. },
{ "prover": "script", "verdict": "valid" },
{ "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "inside-goal", "occur": 0, "select": { "select": "inside-goal", "occur": 0,
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nlet r_0 = Mf32_9[(shiftfield_F10_FloatEulers_phi e_1)] in\nlet r_1 = (\\sin r_0) in\nlet r_2 = Mf32_9[(shiftfield_F10_FloatEulers_psi e_1)] in\nlet r_3 = (\\sin r_2) in\nlet r_4 = Mf32_9[(shiftfield_F10_FloatEulers_theta e_1)] in\nlet r_5 = (\\sin r_4) in\nlet r_6 = (\\cos r_2) in\nlet r_7 = (\\cos r_4) in\nlet r_8 = (\\cos r_0) in\n(L_l_RMat_of_FloatRMat\n Mf32_9[(shift_float32 a_0 0)->(r_6*r_7)-(r_1*r_3*r_5)]\n [(shift_float32 a_0 1)->(r_3*r_7)+(r_1*r_5*r_6)][(shift_float32 a_0 2)\n ->-1*r_5*r_8][(shift_float32 a_0 3)->-1*r_3*r_8][(shift_float32 a_0 4)\n ->r_8*r_6][(shift_float32 a_0 5)->r_1][(shift_float32 a_0 6)\n ->(r_5*r_6)+(r_1*r_3*r_7)][(shift_float32 a_0 7)\n ->(r_3*r_5)-(r_1*r_6*r_7)][(shift_float32 a_0 8)->r_8*r_7] rm_0)", "target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nlet r_0 = Mf32_9[(shiftfield_F10_FloatEulers_phi e_1)] in\nlet r_1 = (\\sin r_0) in\nlet r_2 = Mf32_9[(shiftfield_F10_FloatEulers_psi e_1)] in\nlet r_3 = (\\sin r_2) in\nlet r_4 = Mf32_9[(shiftfield_F10_FloatEulers_theta e_1)] in\nlet r_5 = (\\sin r_4) in\nlet r_6 = (\\cos r_2) in\nlet r_7 = (\\cos r_4) in\nlet r_8 = (\\cos r_0) in\n(L_l_RMat_of_FloatRMat\n Mf32_9[(shift_float32 a_0 0)->(r_6*r_7)-(r_1*r_3*r_5)]\n [(shift_float32 a_0 1)->(r_3*r_7)+(r_1*r_5*r_6)][(shift_float32 a_0 2)\n ->-1*r_5*r_8][(shift_float32 a_0 3)->-1*r_3*r_8][(shift_float32 a_0 4)\n ->r_8*r_6][(shift_float32 a_0 5)->r_1][(shift_float32 a_0 6)\n ->(r_5*r_6)+(r_1*r_3*r_7)][(shift_float32 a_0 7)\n ->(r_3*r_5)-(r_1*r_6*r_7)][(shift_float32 a_0 8)->r_8*r_7] rm_0)",
"pattern": "L_l_RMat_of_FloatRMat[=]$rm[=]shift_float32" }, "pattern": "L_l_RMat_of_FloatRMat[=]$rm[=]shift_float32" },
"children": { "Unfold 'L_l_RMat_of_FloatRMat'": [ { "prover": "Z3:4.8.6:noBV", "children": { "Unfold 'L_l_RMat_of_FloatRMat'": [ { "header": "Definition",
"verdict": "timeout",
"time": 15. },
{ "prover": "Z3:4.8.6:counterexamples",
"verdict": "timeout",
"time": 15. },
{ "prover": "Z3:4.8.6",
"verdict": "timeout",
"time": 15. },
{ "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout",
"time": 15. },
{ "prover": "Alt-Ergo:2.3.3",
"verdict": "timeout",
"time": 15. },
{ "header": "Definition",
"tactic": "Wp.unfold", "tactic": "Wp.unfold",
"params": {}, "params": {},
"select": { "select": "clause-goal", "select": { "select": "clause-goal",
"target": "let r_0 = Mf32_9[(shiftfield_F10_FloatEulers_phi e_1)] in\nlet r_1 = (\\sin r_0) in\nlet r_2 = Mf32_9[(shiftfield_F10_FloatEulers_psi e_1)] in\nlet r_3 = (\\sin r_2) in\nlet r_4 = Mf32_9[(shiftfield_F10_FloatEulers_theta e_1)] in\nlet r_5 = (\\sin r_4) in\nlet r_6 = (\\cos r_2) in\nlet r_7 = (\\cos r_4) in\nlet r_8 = (\\cos r_0) in\n(P_special_orthogonal\n {\n F12_RealRMat_s_a00 = (r_6*r_7)-(r_1*r_3*r_5) ;\n F12_RealRMat_s_a01 = (r_3*r_7)+(r_1*r_5*r_6) ;\n F12_RealRMat_s_a02 = -1*r_5*r_8 ;\n F12_RealRMat_s_a10 = -1*r_3*r_8 ;\n F12_RealRMat_s_a11 = r_8*r_6 ;\n F12_RealRMat_s_a12 = r_1 ;\n F12_RealRMat_s_a20 = (r_5*r_6)+(r_1*r_3*r_7) ;\n F12_RealRMat_s_a21 = (r_3*r_5)-(r_1*r_6*r_7) ;\n F12_RealRMat_s_a22 = r_8*r_7\n })", "target": "let r_0 = Mf32_9[(shiftfield_F10_FloatEulers_phi e_1)] in\nlet r_1 = (\\sin r_0) in\nlet r_2 = Mf32_9[(shiftfield_F10_FloatEulers_psi e_1)] in\nlet r_3 = (\\sin r_2) in\nlet r_4 = Mf32_9[(shiftfield_F10_FloatEulers_theta e_1)] in\nlet r_5 = (\\sin r_4) in\nlet r_6 = (\\cos r_2) in\nlet r_7 = (\\cos r_4) in\nlet r_8 = (\\cos r_0) in\n(P_special_orthogonal\n {\n F12_RealRMat_s_a00 = (r_6*r_7)-(r_1*r_3*r_5) ;\n F12_RealRMat_s_a01 = (r_3*r_7)+(r_1*r_5*r_6) ;\n F12_RealRMat_s_a02 = -1*r_5*r_8 ;\n F12_RealRMat_s_a10 = -1*r_3*r_8 ;\n F12_RealRMat_s_a11 = r_8*r_6 ;\n F12_RealRMat_s_a12 = r_1 ;\n F12_RealRMat_s_a20 = (r_5*r_6)+(r_1*r_3*r_7) ;\n F12_RealRMat_s_a21 = (r_3*r_5)-(r_1*r_6*r_7) ;\n F12_RealRMat_s_a22 = r_8*r_7\n })",
"pattern": "P_special_orthogonal{RealRMat_s}" }, "pattern": "P_special_orthogonal{RealRMat_s}" },
"children": { "Unfold 'P_special_orthogonal'": "children": { "Unfold 'P_special_orthogonal'":
[ { "prover": "Coq:8.12.2", [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "unknown" },
{ "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "verdict": "valid",
"time": 1.6983, "time": 2.004,
"steps": 102 } ] } } ] } } ] "steps": 102 } ] } } ] } } ]
...@@ -59,30 +59,30 @@ ...@@ -59,30 +59,30 @@
{ "Goal 1/6": { "Goal 1/6":
[ { "prover": "Alt-Ergo:2.3.3",