Commit 83db0309 authored by POLLIEN Baptiste's avatar POLLIEN Baptiste
Browse files

Update name

parent ac929be4
......@@ -502,7 +502,7 @@ Definition L_l_RMat_of_FloatQuat_bis_1 (Mf32:addr -> Reals.Rdefinitions.R)
(2%R * (r11 + r12)%R)%R (1%R + ((-1%R)%R * (2%R * (r10 + r1)%R)%R)%R)%R.
(* Why3 assumption *)
Definition P_unary_quaternion (Mf32:addr -> Reals.Rdefinitions.R) (q:addr) :
Definition P_unitary_quaternion (Mf32:addr -> Reals.Rdefinitions.R) (q:addr) :
Prop :=
let r := Mf32 (shift q 0%Z) in
let r1 := Mf32 (shift q 1%Z) in
......@@ -565,21 +565,21 @@ Axiom Q_mult_rmat_id_neutral :
Axiom Q_mutliple_def_rmat_of_quat_1 :
forall (Malloc:Numbers.BinNums.Z -> Numbers.BinNums.Z)
(Mf32:addr -> Reals.Rdefinitions.R) (q:addr),
P_unary_quaternion Mf32 q -> valid_rd Malloc q 4%Z ->
P_unitary_quaternion Mf32 q -> valid_rd Malloc q 4%Z ->
EqS12_RealRMat_s (L_l_RMat_of_FloatQuat Mf32 q)
(L_l_RMat_of_FloatQuat_bis_1 Mf32 q).
Axiom Q_mutliple_def_rmat_of_quat_2 :
forall (Malloc:Numbers.BinNums.Z -> Numbers.BinNums.Z)
(Mf32:addr -> Reals.Rdefinitions.R) (q:addr),
P_unary_quaternion Mf32 q -> valid_rd Malloc q 4%Z ->
P_unitary_quaternion Mf32 q -> valid_rd Malloc q 4%Z ->
EqS12_RealRMat_s (L_l_RMat_of_FloatQuat Mf32 q)
(L_l_RMat_of_FloatQuat_bis_2 Mf32 q).
Axiom Q_mutliple_def_rmat_of_quat_3 :
forall (Malloc:Numbers.BinNums.Z -> Numbers.BinNums.Z)
(Mf32:addr -> Reals.Rdefinitions.R) (q:addr),
P_unary_quaternion Mf32 q -> valid_rd Malloc q 4%Z ->
P_unitary_quaternion Mf32 q -> valid_rd Malloc q 4%Z ->
EqS12_RealRMat_s (L_l_RMat_of_FloatQuat_bis_1 Mf32 q)
(L_l_RMat_of_FloatQuat_bis_2 Mf32 q).
......
......@@ -515,7 +515,7 @@ Definition L_l_RMat_of_FloatQuat_bis_1 (Mf32:addr -> Reals.Rdefinitions.R)
(2%R * (r11 + r12)%R)%R (1%R + ((-1%R)%R * (2%R * (r10 + r1)%R)%R)%R)%R.
(* Why3 assumption *)
Definition P_unary_quaternion (Mf32:addr -> Reals.Rdefinitions.R) (q:addr) :
Definition P_unitary_quaternion (Mf32:addr -> Reals.Rdefinitions.R) (q:addr) :
Prop :=
let r := Mf32 (shift q 0%Z) in
let r1 := Mf32 (shift q 1%Z) in
......@@ -578,21 +578,21 @@ Axiom Q_mult_rmat_id_neutral :
Axiom Q_mutliple_def_rmat_of_quat_1 :
forall (Malloc:Numbers.BinNums.Z -> Numbers.BinNums.Z)
(Mf32:addr -> Reals.Rdefinitions.R) (q:addr),
P_unary_quaternion Mf32 q -> valid_rd Malloc q 4%Z ->
P_unitary_quaternion Mf32 q -> valid_rd Malloc q 4%Z ->
EqS12_RealRMat_s (L_l_RMat_of_FloatQuat Mf32 q)
(L_l_RMat_of_FloatQuat_bis_1 Mf32 q).
Axiom Q_mutliple_def_rmat_of_quat_2 :
forall (Malloc:Numbers.BinNums.Z -> Numbers.BinNums.Z)
(Mf32:addr -> Reals.Rdefinitions.R) (q:addr),
P_unary_quaternion Mf32 q -> valid_rd Malloc q 4%Z ->
P_unitary_quaternion Mf32 q -> valid_rd Malloc q 4%Z ->
EqS12_RealRMat_s (L_l_RMat_of_FloatQuat Mf32 q)
(L_l_RMat_of_FloatQuat_bis_2 Mf32 q).
Axiom Q_mutliple_def_rmat_of_quat_3 :
forall (Malloc:Numbers.BinNums.Z -> Numbers.BinNums.Z)
(Mf32:addr -> Reals.Rdefinitions.R) (q:addr),
P_unary_quaternion Mf32 q -> valid_rd Malloc q 4%Z ->
P_unitary_quaternion Mf32 q -> valid_rd Malloc q 4%Z ->
EqS12_RealRMat_s (L_l_RMat_of_FloatQuat_bis_1 Mf32 q)
(L_l_RMat_of_FloatQuat_bis_2 Mf32 q).
......
......@@ -247,7 +247,7 @@ Definition L_trace_1_ (rmat:S13_RealRMat_s) : Reals.Rdefinitions.R :=
(F13_RealRMat_s_a22 rmat))%R.
(* Why3 assumption *)
Definition P_unary_quaternion_2_ (q:S14_RealQuat_s) : Prop :=
Definition P_unitary_quaternion_2_ (q:S14_RealQuat_s) : Prop :=
let r := F14_RealQuat_s_qi q in
let r1 := F14_RealQuat_s_qx q in
let r2 := F14_RealQuat_s_qy q in
......@@ -287,7 +287,7 @@ Definition L_l_FloatQuat_of_RMat_trace_pos_1_ (rmat:S13_RealRMat_s) :
Axiom Q_impl_rmat_quat_trace_pos :
forall (rm:S13_RealRMat_s) (q:S14_RealQuat_s),
((L_l_RMat_of_FloatQuat_2_ q) = rm) -> (0%R <= (F14_RealQuat_s_qi q))%R ->
(0%R < (L_trace_1_ rm))%R -> P_unary_quaternion_2_ q ->
(0%R < (L_trace_1_ rm))%R -> P_unitary_quaternion_2_ q ->
EqS14_RealQuat_s q (L_l_FloatQuat_of_RMat_trace_pos_1_ rm).
(* Why3 assumption *)
......@@ -827,7 +827,7 @@ Axiom Q_verify_rmat_of_quat_formula :
(L_mult_RealRMat_RealVect3 (L_l_RMat_of_FloatQuat_1_ Mf32 q) a)).
(* Why3 assumption *)
Definition P_unary_quaternion_1_ (Mf32:addr -> Reals.Rdefinitions.R)
Definition P_unitary_quaternion_1_ (Mf32:addr -> Reals.Rdefinitions.R)
(q:addr) : Prop :=
let r := Mf32 (shift q 0%Z) in
let r1 := Mf32 (shift q 1%Z) in
......@@ -837,12 +837,12 @@ Definition P_unary_quaternion_1_ (Mf32:addr -> Reals.Rdefinitions.R)
Axiom Q_quat_of_rmat_special_ortho :
forall (Mf32:addr -> Reals.Rdefinitions.R) (q:addr),
P_unary_quaternion_1_ Mf32 q ->
P_unitary_quaternion_1_ Mf32 q ->
P_special_orthogonal (L_l_RMat_of_FloatQuat_1_ Mf32 q).
Axiom Q_quat_of_rmat_ortho :
forall (Mf32:addr -> Reals.Rdefinitions.R) (q:addr),
P_unary_quaternion_1_ Mf32 q ->
P_unitary_quaternion_1_ Mf32 q ->
P_rotation_matrix (L_l_RMat_of_FloatQuat_1_ Mf32 q).
(* Why3 assumption *)
......@@ -859,7 +859,7 @@ Definition L_conj_1_ (q:S14_RealQuat_s) : S14_RealQuat_s :=
Axiom Q_mutliple_def_rmat_of_quat_4 :
forall (Malloc:Numbers.BinNums.Z -> Numbers.BinNums.Z)
(Mf32:addr -> Reals.Rdefinitions.R) (q:addr),
P_unary_quaternion_1_ Mf32 q -> valid_rd Malloc q 4%Z ->
P_unitary_quaternion_1_ Mf32 q -> valid_rd Malloc q 4%Z ->
EqS13_RealRMat_s (L_l_RMat_of_FloatQuat_1_ Mf32 q)
(L_l_RMat_of_FloatQuat_2_ (L_l_Quat_of_FloatQuat Mf32 q)).
......@@ -908,28 +908,28 @@ Definition L_l_RMat_of_FloatQuat_bis_2 (Mf32:addr -> Reals.Rdefinitions.R)
Axiom Q_mutliple_def_rmat_of_quat_3 :
forall (Malloc:Numbers.BinNums.Z -> Numbers.BinNums.Z)
(Mf32:addr -> Reals.Rdefinitions.R) (q:addr),
P_unary_quaternion_1_ Mf32 q -> valid_rd Malloc q 4%Z ->
P_unitary_quaternion_1_ Mf32 q -> valid_rd Malloc q 4%Z ->
EqS13_RealRMat_s (L_l_RMat_of_FloatQuat_bis_1 Mf32 q)
(L_l_RMat_of_FloatQuat_bis_2 Mf32 q).
Axiom Q_mutliple_def_rmat_of_quat_2 :
forall (Malloc:Numbers.BinNums.Z -> Numbers.BinNums.Z)
(Mf32:addr -> Reals.Rdefinitions.R) (q:addr),
P_unary_quaternion_1_ Mf32 q -> valid_rd Malloc q 4%Z ->
P_unitary_quaternion_1_ Mf32 q -> valid_rd Malloc q 4%Z ->
EqS13_RealRMat_s (L_l_RMat_of_FloatQuat_1_ Mf32 q)
(L_l_RMat_of_FloatQuat_bis_2 Mf32 q).
Axiom Q_mutliple_def_rmat_of_quat_1 :
forall (Malloc:Numbers.BinNums.Z -> Numbers.BinNums.Z)
(Mf32:addr -> Reals.Rdefinitions.R) (q:addr),
P_unary_quaternion_1_ Mf32 q -> valid_rd Malloc q 4%Z ->
P_unitary_quaternion_1_ Mf32 q -> valid_rd Malloc q 4%Z ->
EqS13_RealRMat_s (L_l_RMat_of_FloatQuat_1_ Mf32 q)
(L_l_RMat_of_FloatQuat_bis_1 Mf32 q).
Axiom Q_equivalence_unary_pred :
Axiom Q_equivalence_unitary_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.
P_unitary_quaternion_2_ (L_l_Quat_of_FloatQuat Mf32 q) <->
P_unitary_quaternion_1_ Mf32 q.
(* Why3 assumption *)
Definition L_l_QuatVect_of_RealQuat (q:S14_RealQuat_s) : S15_RealQuatVect_s :=
......@@ -984,7 +984,7 @@ Theorem wp_goal :
let r := F13_RealRMat_s_a00 R in
((L_l_RMat_of_FloatQuat_2_ R1) = R) -> (0%R <= (F14_RealQuat_s_qx R1))%R ->
((F13_RealRMat_s_a11 R) < r)%R -> ((F13_RealRMat_s_a22 R) < r)%R ->
((L_trace_1_ R) <= 0%R)%R -> P_unary_quaternion_2_ R1 ->
((L_trace_1_ R) <= 0%R)%R -> P_unitary_quaternion_2_ R1 ->
EqS14_RealQuat_s R1 (L_l_FloatQuat_of_RMat_0_max_1_ R).
(* Why3 intros R R1 r h1 h2 h3 h4 h5 h6. *)
Proof.
......@@ -997,7 +997,7 @@ unfold F14_RealQuat_s_qi in H2; simpl in H2.
unfold F13_RealRMat_s_a11 in H3; simpl in H3.
unfold F13_RealRMat_s_a22 in H4; simpl in H4.
unfold L_trace_1_ in H5; simpl in H5.
unfold P_unary_quaternion_2_ in H6; simpl in H6.
unfold P_unitary_quaternion_2_ in H6; simpl in H6.
unfold L_l_FloatQuat_of_RMat_0_max_1_; simpl.
assert (H: (1 + - (1) * a4 + - (1) * a8 + a0 = 4 * q2 * q2)).
{
......
......@@ -240,7 +240,7 @@ Definition L_trace_1_ (rmat:S13_RealRMat_s) : Reals.Rdefinitions.R :=
(F13_RealRMat_s_a22 rmat))%R.
(* Why3 assumption *)
Definition P_unary_quaternion_2_ (q:S14_RealQuat_s) : Prop :=
Definition P_unitary_quaternion_2_ (q:S14_RealQuat_s) : Prop :=
let r := F14_RealQuat_s_qi q in
let r1 := F14_RealQuat_s_qx q in
let r2 := F14_RealQuat_s_qy q in
......@@ -285,7 +285,7 @@ Axiom Q_impl_rmat_quat_a00_max :
let r := F13_RealRMat_s_a00 rm in
((L_l_RMat_of_FloatQuat_2_ q) = rm) -> (0%R <= (F14_RealQuat_s_qx q))%R ->
((F13_RealRMat_s_a11 rm) < r)%R -> ((F13_RealRMat_s_a22 rm) < r)%R ->
((L_trace_1_ rm) <= 0%R)%R -> P_unary_quaternion_2_ q ->
((L_trace_1_ rm) <= 0%R)%R -> P_unitary_quaternion_2_ q ->
EqS14_RealQuat_s q (L_l_FloatQuat_of_RMat_0_max_1_ rm).
Axiom Q_ne_zero_quat :
......@@ -311,7 +311,7 @@ Definition L_l_FloatQuat_of_RMat_trace_pos_1_ (rmat:S13_RealRMat_s) :
Axiom Q_impl_rmat_quat_trace_pos :
forall (rm:S13_RealRMat_s) (q:S14_RealQuat_s),
((L_l_RMat_of_FloatQuat_2_ q) = rm) -> (0%R <= (F14_RealQuat_s_qi q))%R ->
(0%R < (L_trace_1_ rm))%R -> P_unary_quaternion_2_ q ->
(0%R < (L_trace_1_ rm))%R -> P_unitary_quaternion_2_ q ->
EqS14_RealQuat_s q (L_l_FloatQuat_of_RMat_trace_pos_1_ rm).
(* Why3 assumption *)
......@@ -865,7 +865,7 @@ Axiom Q_verify_rmat_of_quat_formula :
(L_mult_RealRMat_RealVect3 (L_l_RMat_of_FloatQuat_1_ Mf32 q) a)).
(* Why3 assumption *)
Definition P_unary_quaternion_1_ (Mf32:addr -> Reals.Rdefinitions.R)
Definition P_unitary_quaternion_1_ (Mf32:addr -> Reals.Rdefinitions.R)
(q:addr) : Prop :=
let r := Mf32 (shift q 0%Z) in
let r1 := Mf32 (shift q 1%Z) in
......@@ -875,12 +875,12 @@ Definition P_unary_quaternion_1_ (Mf32:addr -> Reals.Rdefinitions.R)
Axiom Q_quat_of_rmat_special_ortho :
forall (Mf32:addr -> Reals.Rdefinitions.R) (q:addr),
P_unary_quaternion_1_ Mf32 q ->
P_unitary_quaternion_1_ Mf32 q ->
P_special_orthogonal (L_l_RMat_of_FloatQuat_1_ Mf32 q).
Axiom Q_quat_of_rmat_ortho :
forall (Mf32:addr -> Reals.Rdefinitions.R) (q:addr),
P_unary_quaternion_1_ Mf32 q ->
P_unitary_quaternion_1_ Mf32 q ->
P_rotation_matrix (L_l_RMat_of_FloatQuat_1_ Mf32 q).
(* Why3 assumption *)
......@@ -897,7 +897,7 @@ Definition L_conj_1_ (q:S14_RealQuat_s) : S14_RealQuat_s :=
Axiom Q_mutliple_def_rmat_of_quat_4 :
forall (Malloc:Numbers.BinNums.Z -> Numbers.BinNums.Z)
(Mf32:addr -> Reals.Rdefinitions.R) (q:addr),
P_unary_quaternion_1_ Mf32 q -> valid_rd Malloc q 4%Z ->
P_unitary_quaternion_1_ Mf32 q -> valid_rd Malloc q 4%Z ->
EqS13_RealRMat_s (L_l_RMat_of_FloatQuat_1_ Mf32 q)
(L_l_RMat_of_FloatQuat_2_ (L_l_Quat_of_FloatQuat Mf32 q)).
......@@ -946,28 +946,28 @@ Definition L_l_RMat_of_FloatQuat_bis_2 (Mf32:addr -> Reals.Rdefinitions.R)
Axiom Q_mutliple_def_rmat_of_quat_3 :
forall (Malloc:Numbers.BinNums.Z -> Numbers.BinNums.Z)
(Mf32:addr -> Reals.Rdefinitions.R) (q:addr),
P_unary_quaternion_1_ Mf32 q -> valid_rd Malloc q 4%Z ->
P_unitary_quaternion_1_ Mf32 q -> valid_rd Malloc q 4%Z ->
EqS13_RealRMat_s (L_l_RMat_of_FloatQuat_bis_1 Mf32 q)
(L_l_RMat_of_FloatQuat_bis_2 Mf32 q).
Axiom Q_mutliple_def_rmat_of_quat_2 :
forall (Malloc:Numbers.BinNums.Z -> Numbers.BinNums.Z)
(Mf32:addr -> Reals.Rdefinitions.R) (q:addr),
P_unary_quaternion_1_ Mf32 q -> valid_rd Malloc q 4%Z ->
P_unitary_quaternion_1_ Mf32 q -> valid_rd Malloc q 4%Z ->
EqS13_RealRMat_s (L_l_RMat_of_FloatQuat_1_ Mf32 q)
(L_l_RMat_of_FloatQuat_bis_2 Mf32 q).
Axiom Q_mutliple_def_rmat_of_quat_1 :
forall (Malloc:Numbers.BinNums.Z -> Numbers.BinNums.Z)
(Mf32:addr -> Reals.Rdefinitions.R) (q:addr),
P_unary_quaternion_1_ Mf32 q -> valid_rd Malloc q 4%Z ->
P_unitary_quaternion_1_ Mf32 q -> valid_rd Malloc q 4%Z ->
EqS13_RealRMat_s (L_l_RMat_of_FloatQuat_1_ Mf32 q)
(L_l_RMat_of_FloatQuat_bis_1 Mf32 q).
Axiom Q_equivalence_unary_pred :
Axiom Q_equivalence_unitary_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.
P_unitary_quaternion_2_ (L_l_Quat_of_FloatQuat Mf32 q) <->
P_unitary_quaternion_1_ Mf32 q.
(* Why3 assumption *)
Definition L_conj_v_1_ (Mf32:addr -> Reals.Rdefinitions.R) (q:addr) :
......@@ -1028,7 +1028,7 @@ Theorem wp_goal :
let r := F13_RealRMat_s_a11 R in
((L_l_RMat_of_FloatQuat_2_ R1) = R) -> (0%R <= (F14_RealQuat_s_qy R1))%R ->
((F13_RealRMat_s_a00 R) < r)%R -> ((F13_RealRMat_s_a22 R) < r)%R ->
((L_trace_1_ R) <= 0%R)%R -> P_unary_quaternion_2_ R1 ->
((L_trace_1_ R) <= 0%R)%R -> P_unitary_quaternion_2_ R1 ->
EqS14_RealQuat_s R1 (L_l_FloatQuat_of_RMat_1_max_1_ R).
(* Why3 intros R R1 r h1 h2 h3 h4 h5 h6. *)
Proof.
......@@ -1041,7 +1041,7 @@ unfold F14_RealQuat_s_qi in H2; simpl in H2.
unfold F13_RealRMat_s_a00 in H3; simpl in H3.
unfold F13_RealRMat_s_a22 in H4; simpl in H4.
unfold L_trace_1_ in H5; simpl in H5.
unfold P_unary_quaternion_2_ in H6; simpl in H6.
unfold P_unitary_quaternion_2_ in H6; simpl in H6.
unfold L_l_FloatQuat_of_RMat_1_max_1_; simpl.
assert (H: (1 + -(1) * a0 + - (1) * a8 + a4 = 4 * q3 * q3)%R).
{
......
......@@ -240,7 +240,7 @@ Definition L_trace_1_ (rmat:S13_RealRMat_s) : Reals.Rdefinitions.R :=
(F13_RealRMat_s_a22 rmat))%R.
(* Why3 assumption *)
Definition P_unary_quaternion_2_ (q:S14_RealQuat_s) : Prop :=
Definition P_unitary_quaternion_2_ (q:S14_RealQuat_s) : Prop :=
let r := F14_RealQuat_s_qi q in
let r1 := F14_RealQuat_s_qx q in
let r2 := F14_RealQuat_s_qy q in
......@@ -285,7 +285,7 @@ Axiom Q_impl_rmat_quat_a11_max :
let r := F13_RealRMat_s_a11 rm in
((L_l_RMat_of_FloatQuat_2_ q) = rm) -> (0%R <= (F14_RealQuat_s_qy q))%R ->
((F13_RealRMat_s_a00 rm) < r)%R -> ((F13_RealRMat_s_a22 rm) < r)%R ->
((L_trace_1_ rm) <= 0%R)%R -> P_unary_quaternion_2_ q ->
((L_trace_1_ rm) <= 0%R)%R -> P_unitary_quaternion_2_ q ->
EqS14_RealQuat_s q (L_l_FloatQuat_of_RMat_1_max_1_ rm).
(* Why3 assumption *)
......@@ -309,7 +309,7 @@ Axiom Q_impl_rmat_quat_a00_max :
let r := F13_RealRMat_s_a00 rm in
((L_l_RMat_of_FloatQuat_2_ q) = rm) -> (0%R <= (F14_RealQuat_s_qx q))%R ->
((F13_RealRMat_s_a11 rm) < r)%R -> ((F13_RealRMat_s_a22 rm) < r)%R ->
((L_trace_1_ rm) <= 0%R)%R -> P_unary_quaternion_2_ q ->
((L_trace_1_ rm) <= 0%R)%R -> P_unitary_quaternion_2_ q ->
EqS14_RealQuat_s q (L_l_FloatQuat_of_RMat_0_max_1_ rm).
Axiom Q_ne_zero_quat :
......@@ -335,7 +335,7 @@ Definition L_l_FloatQuat_of_RMat_trace_pos_1_ (rmat:S13_RealRMat_s) :
Axiom Q_impl_rmat_quat_trace_pos :
forall (rm:S13_RealRMat_s) (q:S14_RealQuat_s),
((L_l_RMat_of_FloatQuat_2_ q) = rm) -> (0%R <= (F14_RealQuat_s_qi q))%R ->
(0%R < (L_trace_1_ rm))%R -> P_unary_quaternion_2_ q ->
(0%R < (L_trace_1_ rm))%R -> P_unitary_quaternion_2_ q ->
EqS14_RealQuat_s q (L_l_FloatQuat_of_RMat_trace_pos_1_ rm).
(* Why3 assumption *)
......@@ -875,7 +875,7 @@ Axiom Q_verify_rmat_of_quat_formula :
(L_mult_RealRMat_RealVect3 (L_l_RMat_of_FloatQuat_1_ Mf32 q) a)).
(* Why3 assumption *)
Definition P_unary_quaternion_1_ (Mf32:addr -> Reals.Rdefinitions.R)
Definition P_unitary_quaternion_1_ (Mf32:addr -> Reals.Rdefinitions.R)
(q:addr) : Prop :=
let r := Mf32 (shift q 0%Z) in
let r1 := Mf32 (shift q 1%Z) in
......@@ -885,12 +885,12 @@ Definition P_unary_quaternion_1_ (Mf32:addr -> Reals.Rdefinitions.R)
Axiom Q_quat_of_rmat_special_ortho :
forall (Mf32:addr -> Reals.Rdefinitions.R) (q:addr),
P_unary_quaternion_1_ Mf32 q ->
P_unitary_quaternion_1_ Mf32 q ->
P_special_orthogonal (L_l_RMat_of_FloatQuat_1_ Mf32 q).
Axiom Q_quat_of_rmat_ortho :
forall (Mf32:addr -> Reals.Rdefinitions.R) (q:addr),
P_unary_quaternion_1_ Mf32 q ->
P_unitary_quaternion_1_ Mf32 q ->
P_rotation_matrix (L_l_RMat_of_FloatQuat_1_ Mf32 q).
(* Why3 assumption *)
......@@ -907,7 +907,7 @@ Definition L_conj_1_ (q:S14_RealQuat_s) : S14_RealQuat_s :=
Axiom Q_mutliple_def_rmat_of_quat_4 :
forall (Malloc:Numbers.BinNums.Z -> Numbers.BinNums.Z)
(Mf32:addr -> Reals.Rdefinitions.R) (q:addr),
P_unary_quaternion_1_ Mf32 q -> valid_rd Malloc q 4%Z ->
P_unitary_quaternion_1_ Mf32 q -> valid_rd Malloc q 4%Z ->
EqS13_RealRMat_s (L_l_RMat_of_FloatQuat_1_ Mf32 q)
(L_l_RMat_of_FloatQuat_2_ (L_l_Quat_of_FloatQuat Mf32 q)).
......@@ -956,28 +956,28 @@ Definition L_l_RMat_of_FloatQuat_bis_2 (Mf32:addr -> Reals.Rdefinitions.R)
Axiom Q_mutliple_def_rmat_of_quat_3 :
forall (Malloc:Numbers.BinNums.Z -> Numbers.BinNums.Z)
(Mf32:addr -> Reals.Rdefinitions.R) (q:addr),
P_unary_quaternion_1_ Mf32 q -> valid_rd Malloc q 4%Z ->
P_unitary_quaternion_1_ Mf32 q -> valid_rd Malloc q 4%Z ->
EqS13_RealRMat_s (L_l_RMat_of_FloatQuat_bis_1 Mf32 q)
(L_l_RMat_of_FloatQuat_bis_2 Mf32 q).
Axiom Q_mutliple_def_rmat_of_quat_2 :
forall (Malloc:Numbers.BinNums.Z -> Numbers.BinNums.Z)
(Mf32:addr -> Reals.Rdefinitions.R) (q:addr),
P_unary_quaternion_1_ Mf32 q -> valid_rd Malloc q 4%Z ->
P_unitary_quaternion_1_ Mf32 q -> valid_rd Malloc q 4%Z ->
EqS13_RealRMat_s (L_l_RMat_of_FloatQuat_1_ Mf32 q)
(L_l_RMat_of_FloatQuat_bis_2 Mf32 q).
Axiom Q_mutliple_def_rmat_of_quat_1 :
forall (Malloc:Numbers.BinNums.Z -> Numbers.BinNums.Z)
(Mf32:addr -> Reals.Rdefinitions.R) (q:addr),
P_unary_quaternion_1_ Mf32 q -> valid_rd Malloc q 4%Z ->
P_unitary_quaternion_1_ Mf32 q -> valid_rd Malloc q 4%Z ->
EqS13_RealRMat_s (L_l_RMat_of_FloatQuat_1_ Mf32 q)
(L_l_RMat_of_FloatQuat_bis_1 Mf32 q).
Axiom Q_equivalence_unary_pred :
Axiom Q_equivalence_unitary_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.
P_unitary_quaternion_2_ (L_l_Quat_of_FloatQuat Mf32 q) <->
P_unitary_quaternion_1_ Mf32 q.
(* Why3 assumption *)
Definition L_l_QuatVect_of_RealQuat (q:S14_RealQuat_s) : S15_RealQuatVect_s :=
......@@ -1031,7 +1031,7 @@ Theorem wp_goal :
let r := F13_RealRMat_s_a22 R in
((L_l_RMat_of_FloatQuat_2_ R1) = R) -> (0%R <= (F14_RealQuat_s_qz R1))%R ->
((F13_RealRMat_s_a00 R) < r)%R -> ((F13_RealRMat_s_a11 R) < r)%R ->
((L_trace_1_ R) <= 0%R)%R -> P_unary_quaternion_2_ R1 ->
((L_trace_1_ R) <= 0%R)%R -> P_unitary_quaternion_2_ R1 ->
EqS14_RealQuat_s R1 (L_l_FloatQuat_of_RMat_2_max_1_ R).
(* Why3 intros R R1 r h1 h2 h3 h4 h5 h6. *)
Proof.
......@@ -1044,7 +1044,7 @@ unfold F14_RealQuat_s_qi in H2; simpl in H2.
unfold F13_RealRMat_s_a00 in H3; simpl in H3.
unfold F13_RealRMat_s_a11 in H4; simpl in H4.
unfold L_trace_1_ in H5; simpl in H5.
unfold P_unary_quaternion_2_ in H6; simpl in H6.
unfold P_unitary_quaternion_2_ in H6; simpl in H6.
unfold L_l_FloatQuat_of_RMat_2_max_1_; simpl.
assert (H: (1 + - (1) * a0 + - (1) * a4 + a8 = 4 * q4 * q4)%R).
{
......
......@@ -709,7 +709,7 @@ Axiom Q_verify_rmat_of_quat_formula :
(L_mult_RealRMat_RealVect3 (L_l_RMat_of_FloatQuat_1_ Mf32 q) a)).
(* Why3 assumption *)
Definition P_unary_quaternion_1_ (Mf32:addr -> Reals.Rdefinitions.R)
Definition P_unitary_quaternion_1_ (Mf32:addr -> Reals.Rdefinitions.R)
(q:addr) : Prop :=
let r := Mf32 (shift q 0%Z) in
let r1 := Mf32 (shift q 1%Z) in
......@@ -719,12 +719,12 @@ Definition P_unary_quaternion_1_ (Mf32:addr -> Reals.Rdefinitions.R)
Axiom Q_quat_of_rmat_special_ortho :
forall (Mf32:addr -> Reals.Rdefinitions.R) (q:addr),
P_unary_quaternion_1_ Mf32 q ->
P_unitary_quaternion_1_ Mf32 q ->
P_special_orthogonal (L_l_RMat_of_FloatQuat_1_ Mf32 q).
Axiom Q_quat_of_rmat_ortho :
forall (Mf32:addr -> Reals.Rdefinitions.R) (q:addr),
P_unary_quaternion_1_ Mf32 q ->
P_unitary_quaternion_1_ Mf32 q ->
P_rotation_matrix (L_l_RMat_of_FloatQuat_1_ Mf32 q).
(* Why3 assumption *)
......@@ -805,7 +805,7 @@ Definition L_conj_1_ (q:S14_RealQuat_s) : S14_RealQuat_s :=
Axiom Q_mutliple_def_rmat_of_quat_4 :
forall (Malloc:Numbers.BinNums.Z -> Numbers.BinNums.Z)
(Mf32:addr -> Reals.Rdefinitions.R) (q:addr),
P_unary_quaternion_1_ Mf32 q -> valid_rd Malloc q 4%Z ->
P_unitary_quaternion_1_ Mf32 q -> valid_rd Malloc q 4%Z ->
EqS13_RealRMat_s (L_l_RMat_of_FloatQuat_1_ Mf32 q)
(L_l_RMat_of_FloatQuat_2_ (L_l_Quat_of_FloatQuat Mf32 q)).
......@@ -854,36 +854,36 @@ Definition L_l_RMat_of_FloatQuat_bis_2 (Mf32:addr -> Reals.Rdefinitions.R)
Axiom Q_mutliple_def_rmat_of_quat_3 :
forall (Malloc:Numbers.BinNums.Z -> Numbers.BinNums.Z)
(Mf32:addr -> Reals.Rdefinitions.R) (q:addr),
P_unary_quaternion_1_ Mf32 q -> valid_rd Malloc q 4%Z ->
P_unitary_quaternion_1_ Mf32 q -> valid_rd Malloc q 4%Z ->
EqS13_RealRMat_s (L_l_RMat_of_FloatQuat_bis_1 Mf32 q)
(L_l_RMat_of_FloatQuat_bis_2 Mf32 q).
Axiom Q_mutliple_def_rmat_of_quat_2 :
forall (Malloc:Numbers.BinNums.Z -> Numbers.BinNums.Z)
(Mf32:addr -> Reals.Rdefinitions.R) (q:addr),
P_unary_quaternion_1_ Mf32 q -> valid_rd Malloc q 4%Z ->
P_unitary_quaternion_1_ Mf32 q -> valid_rd Malloc q 4%Z ->
EqS13_RealRMat_s (L_l_RMat_of_FloatQuat_1_ Mf32 q)
(L_l_RMat_of_FloatQuat_bis_2 Mf32 q).
Axiom Q_mutliple_def_rmat_of_quat_1 :
forall (Malloc:Numbers.BinNums.Z -> Numbers.BinNums.Z)
(Mf32:addr -> Reals.Rdefinitions.R) (q:addr),
P_unary_quaternion_1_ Mf32 q -> valid_rd Malloc q 4%Z ->
P_unitary_quaternion_1_ Mf32 q -> valid_rd Malloc q 4%Z ->
EqS13_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:S14_RealQuat_s) : Prop :=
Definition P_unitary_quaternion_2_ (q:S14_RealQuat_s) : Prop :=
let r := F14_RealQuat_s_qi q in
let r1 := F14_RealQuat_s_qx q in
let r2 := F14_RealQuat_s_qy q in
let r3 := F14_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 :
Axiom Q_equivalence_unitary_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.
P_unitary_quaternion_2_ (L_l_Quat_of_FloatQuat Mf32 q) <->
P_unitary_quaternion_1_ Mf32 q.
(* Why3 assumption *)
Definition L_l_QuatVect_of_RealQuat (q:S14_RealQuat_s) : S15_RealQuatVect_s :=
......@@ -947,7 +947,7 @@ Local Open Scope R_scope.
Theorem wp_goal :
forall (R:S13_RealRMat_s) (R1:S14_RealQuat_s),
((L_l_RMat_of_FloatQuat_2_ R1) = R) -> (0%R <= (F14_RealQuat_s_qi R1))%R ->
(0%R < (L_trace_1_ R))%R -> P_unary_quaternion_2_ R1 ->
(0%R < (L_trace_1_ R))%R -> P_unitary_quaternion_2_ R1 ->
EqS14_RealQuat_s R1 (L_l_FloatQuat_of_RMat_trace_pos_1_ R).
(* Why3 intros R R1 h1 h2 h3 h4. *)
Proof.
......@@ -957,7 +957,7 @@ destruct Q as[q1 q2 q3 q4].
unfold L_l_RMat_of_FloatQuat_2_ in H1; simpl in H1.
unfold F14_RealQuat_s_qi in H2; simpl in H2.
unfold L_trace_1_ in H3; simpl in H3.
unfold P_unary_quaternion_2_ in H4; simpl in H4.
unfold P_unitary_quaternion_2_ in H4; simpl in H4.
unfold L_l_FloatQuat_of_RMat_trace_pos_1_; simpl.
assert (1 + L_trace_1_ (S13_RealRMat_s1 a0 a1 a2 a3 a4 a5 a6 a7 a8) = 4 * q1 * q1).
{
......
......@@ -113,5 +113,5 @@
{ "Unfold 'EqS12_RealVect3_s'":
[ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 7.5735,
"time": 7.3308,
"steps": 48686 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
......@@ -64,9 +64,9 @@
{ "Then":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 1.97 } ],
"time": 1.98 } ],
"Else":
[ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 12.0861,
"time": 14.8114,
"steps": 160794 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
......@@ -36,5 +36,5 @@
{ "Unfold 'L_trace_2_'":
[ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 11.6594,
"steps": 186185 } ] } } ] } } ] } } ] } } ]
"time": 14.7056,
"steps": 183901 } ] } } ] } } ] } } ] } } ]
......@@ -69,7 +69,7 @@
{ "Then":
[ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 0.2864,
"time": 0.4716,
"steps": 2972 } ],
"Else":
[ { "header": "Split",
......@@ -85,10 +85,10 @@
{ "Then":
[ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 3.2286,
"steps": 69882 } ],
"time": 4.6808,
"steps": 69958 } ],
"Else":
[ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 3.8577,
"steps": 80726 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 5.566,
"steps": 80521 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "clause-goal",