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

Functionnal proof rmat_of_eulers

parent c6163b37
......@@ -662,20 +662,21 @@ Theorem wp_goal :
((((((r3 * r3)%R * r4)%R * r4)%R + (r9 * r9)%R)%R + (r10 * r10)%R)%R = 1%R).
(* Why3 intros r r1 r2 r3 r4 r5 r6 r7 r8 r9 r10. *)
Proof.
intros r r1 r2 r3 r4 r5 r6 r7 r8 r9 r10.
unfold r9, r10.
ring_simplify.
rewrite Rmult_comm with (r1 := Rpow_def.pow r5 2).
rewrite Rplus_assoc. rewrite <- Rmult_plus_distr_l .
unfold r5, r8; rewrite sin_cos_sqr; repeat rewrite Rmult_comm with (r2:=1%R); repeat rewrite Rmult_1_l.
ring_simplify.
repeat rewrite Rmult_assoc. repeat rewrite <- Rmult_plus_distr_l with (r1:= Rpow_def.pow r3 2).
rewrite Rmult_comm with (r1 := Rpow_def.pow (Rtrigo_def.sin r2) 2).
rewrite Rplus_assoc. rewrite <- Rmult_plus_distr_l.
rewrite sin_cos_sqr; repeat rewrite Rmult_comm with (r2:=1%R); repeat rewrite Rmult_1_l.
unfold r4, r7. rewrite Rplus_comm with (r1:=Rpow_def.pow (Rtrigo_def.cos r1) 2).
rewrite sin_cos_sqr; repeat rewrite Rmult_comm with (r2:=1%R); repeat rewrite Rmult_1_l.
unfold r3, r6. rewrite sin_cos_sqr.
auto.
intros r r1 r2 r3 r4 r5 r6 r7 r8 r9 r10.
unfold r9, r10.
ring_simplify.
rewrite Rmult_comm with (r1 := Rpow_def.pow r5 2).
rewrite Rplus_assoc. rewrite <- Rmult_plus_distr_l .
unfold r5, r8; rewrite sin_cos_sqr; repeat rewrite Rmult_comm with (r2:=1%R); repeat rewrite Rmult_1_l.
ring_simplify.
repeat rewrite Rmult_assoc. repeat rewrite <- Rmult_plus_distr_l with (r1:= Rpow_def.pow r3 2).
rewrite Rmult_comm with (r1 := Rpow_def.pow (Rtrigo_def.sin r2) 2).
rewrite Rplus_assoc. rewrite <- Rmult_plus_distr_l.
rewrite sin_cos_sqr; repeat rewrite Rmult_comm with (r2:=1%R); repeat rewrite Rmult_1_l.
unfold r4, r7.
rewrite Rplus_comm with (r1:=Rpow_def.pow (Rtrigo_def.cos r1) 2).
rewrite sin_cos_sqr; repeat rewrite Rmult_comm with (r2:=1%R); repeat rewrite Rmult_1_l.
unfold r3, r6. rewrite sin_cos_sqr.
auto.
Qed.
[ { "prover": "script", "verdict": "timeout", "time": 10., "steps": 2332912 },
{ "header": "Definition", "tactic": "Wp.unfold", "params": {},
[ { "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_9[(shiftfield_F10_FloatEulers_psi e_1)] in\nlet r_1 = (\\cos r_0) in\nlet r_2 = Mf32_9[(shiftfield_F10_FloatEulers_theta e_1)] in\nlet r_3 = (\\cos r_2) in\nlet r_4 = (\\sin r_0) in\nlet r_5 = (\\sin r_2) in\nlet r_6 = Mf32_9[(shiftfield_F10_FloatEulers_phi e_1)] in\nlet r_7 = (\\cos r_6) in\nlet r_8 = (\\sin r_6) in\n(L_l_RMat_of_FloatRMat\n Mf32_9[(shift_float32 a_0 0)->r_1*r_3][(shift_float32 a_0 1)->r_4*r_3]\n [(shift_float32 a_0 2)->-r_5][(shift_float32 a_0 3)\n ->(r_8*r_5*r_1)-(r_4*r_7)][(shift_float32 a_0 4)\n ->(r_7*r_1)+(r_8*r_4*r_5)][(shift_float32 a_0 5)->r_8*r_3]\n [(shift_float32 a_0 6)->(r_8*r_4)+(r_5*r_7*r_1)][(shift_float32 a_0 7)\n ->(r_4*r_5*r_7)-(r_8*r_1)][(shift_float32 a_0 8)->r_7*r_3] rm_0)",
"pattern": "L_l_RMat_of_FloatRMat[=]$rm[=]shift_float32" },
......@@ -60,50 +59,30 @@
{ "Goal 1/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 0.5,
"time": 1.5546,
"steps": 102 } ],
"Goal 2/6":
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.48,
"steps": 2332912 },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout",
"time": 10. },
{ "prover": "Alt-Ergo:2.3.3",
"verdict": "timeout",
"time": 10. } ],
"time": 0.49,
"steps": 2354057 } ],
"Goal 3/6":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout",
"time": 10. },
{ "prover": "Alt-Ergo:2.3.3",
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.1626,
"time": 2.0949,
"steps": 102 } ],
"Goal 4/6":
[ { "prover": "Z3:4.8.6:noBV",
"verdict": "timeout",
"time": 10. },
{ "prover": "Z3:4.8.6:counterexamples",
"verdict": "timeout",
"time": 10. },
{ "prover": "Z3:4.8.6",
"verdict": "timeout",
"time": 10. },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout",
"time": 10. },
{ "prover": "Alt-Ergo:2.3.3",
"verdict": "timeout",
"time": 10. } ],
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.58,
"steps": 2356395 } ],
"Goal 5/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 0.6993,
"time": 1.717,
"steps": 102 } ],
"Goal 6/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 0.7479,
"time": 1.5857,
"steps": 102 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
[ { "prover": "Z3:4.8.6:noBV", "verdict": "timeout", "time": 10. },
{ "prover": "Z3:4.8.6:counterexamples", "verdict": "timeout", "time": 10. },
{ "prover": "Z3:4.8.6", "verdict": "timeout", "time": 10. },
{ "prover": "Coq:8.12.2", "verdict": "valid", "time": 0.49 },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout", "time": 10. },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "timeout", "time": 10. } ]
[ { "prover": "Z3:4.8.6:noBV", "verdict": "timeout", "time": 10. },
{ "prover": "Z3:4.8.6:counterexamples", "verdict": "timeout", "time": 10. },
{ "prover": "Z3:4.8.6", "verdict": "timeout", "time": 10. },
{ "prover": "Coq:8.12.2", "verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout", "time": 10. },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "timeout", "time": 10. } ]
......@@ -189,58 +189,6 @@ void float_rmat_of_axis_angle(struct FloatRMat *rm, struct FloatVect3 *uv, float
RMAT_ELMT(*rm, 2, 2) = uz2 + (1. - uz2) * can;
}
/*@
lemma cos_add:
\forall real a, b;
\cos(a + b) == \cos(a) * \cos(b) - \sin(a)* \sin(b);
*/
/*@
lemma cos_sub:
\forall real a, b;
\cos(a - b) == \cos(a) * \cos(b) + \sin(a)* \sin(b);
*/
/*@
lemma sin_add:
\forall real a, b;
\sin(a + b) == \sin(a) * \cos(b) + \cos(a) * \sin(b);
*/
/*@
lemma sin_sub:
\forall real a, b;
\sin(a - b) == \sin(a) * \cos(b) - \cos(a)* \sin(b);
*/
/*@
lemma cos_sin_square:
\forall real a;
SQR(\cos(a)) + SQR(\sin(a)) == 1.0;
*/
/*@
lemma remarkable_identity_1:
\forall real a, b;
SQR(a + b) == SQR(a) + 2 * a * b + SQR(b);
lemma remarkable_identity_2:
\forall real a, b;
SQR(a - b) == SQR(a) - 2 * a * b + SQR(b);
lemma factorisation:
\forall real a, b, c;
a * b + a * c == a * (b + c);
*/
/*@
lemma float_rmat_of_eulers_321:
\forall real a, b, c;
SQR(\sin(a)) * SQR(\cos(b))
+ SQR(\sin(a) * \sin(b) * \cos(c) - \sin(c) * \cos(a))
+ SQR(\cos(c) * \cos(a) + \sin(a) * \sin(b) * \sin(c)) == 1.0;
*/
/* C n->b rotation matrix */
void float_rmat_of_eulers_321(struct FloatRMat *rm, struct FloatEulers *e)
{
......
......@@ -322,6 +322,33 @@ logic RealQuat l_Quat_of_FloatQuat(struct FloatQuat *q) =
l_FloatQuat_of_RMat_2_max(transpose(l_RMat_of_FloatRMat(rmat)));
*/
/***************************
* Trigo lemma
***************************/
/*@
lemma cos_sin_square:
\forall real a;
SQR(\cos(a)) + SQR(\sin(a)) == 1.0;
*/
/*@
lemma float_rmat_of_eulers_321_1:
\forall real a, b, c;
SQR(\sin(a)) * SQR(\cos(b))
+ SQR(\sin(a) * \sin(b) * \cos(c) - \sin(c) * \cos(a))
+ SQR(\cos(c) * \cos(a) + \sin(a) * \sin(b) * \sin(c)) == 1.0;
*/
/*@
lemma float_rmat_of_eulers_321_2:
\forall real a, b, c;
SQR(\cos(a)) * SQR(\cos(b))
+ SQR(\sin(c) * \sin(b) * \cos(a) - \sin(a) * \cos(c))
+ SQR(\sin(a) * \sin(c) + \sin(b) * \cos(a) * \cos(c)) == 1.0;
*/
#ifdef __cplusplus
} /* extern "C" */
#endif
......
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