Skip to content

replacing rcfType by realType in angle.v #20

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

replacing rcfType by realType in angle.v #20

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 8 additions & 6 deletions angle.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -84,9 +84,11 @@ Abort.

End nthroot.

From mathcomp Require Import reals.

Section angle_def.

Variable T : rcfType.
Variable T : realType.

Record angle := Angle {
expi : T[i];
Expand Down Expand Up @@ -223,7 +225,7 @@ Arguments pi {T}.

Section angle_basic_prop.

Variable T : rcfType.
Variable T : realType.
Implicit Types a b : angle T.

Lemma add_angleE a b : a + b = add_angle a b.
Expand Down Expand Up @@ -835,7 +837,7 @@ End angle_basic_prop.

Section half_angle.

Variable T : rcfType.
Variable T : realType.

Definition half_anglec (x : T[i]) :=
(if 0 <= complex.Im x then
Expand Down Expand Up @@ -1040,7 +1042,7 @@ Qed.

End half_angle.

Lemma atan2_N1N1 (T : rcfType) : atan2 (- 1) (- 1) = - piquarter T *+ 3.
Lemma atan2_N1N1 (T : realType) : atan2 (- 1) (- 1) = - piquarter T *+ 3.
Proof.
rewrite /atan2 ltr0N1 ltrN10 ler0N1 divrr; last first.
by rewrite unitfE eqr_oppLR oppr0 oner_neq0.
Expand All @@ -1050,7 +1052,7 @@ Qed.

Section properties_of_atan2.

Variables (T : rcfType).
Variables (T : realType).

Lemma sqrtr_sqrN2 (x : T) : x != 0 -> Num.sqrt (x ^- 2) = `|x|^-1.
Proof.
Expand Down Expand Up @@ -1195,7 +1197,7 @@ End properties_of_atan2.

Section derived_trigonometric_functions.

Variable T : rcfType.
Variable T : realType.
Implicit Types a : angle T.

Definition cot a := (tan a)^-1.
Expand Down
12 changes: 6 additions & 6 deletions dh.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum rat poly.
From mathcomp Require Import closed_field polyrcf matrix mxalgebra mxpoly zmodp.
From mathcomp Require Import realalg complex fingroup perm.
Require Import ssr_ext angle euclidean skew vec_angle rot frame rigid.
From mathcomp.analysis Require Import forms.
From mathcomp.analysis Require Import reals forms.

(******************************************************************************)
(* Denavit-Hartenberg convention *)
Expand Down Expand Up @@ -149,7 +149,7 @@ End plucker_of_line.

Section denavit_hartenberg_homogeneous_matrix.

Variable T : rcfType.
Variable T : realType.

Definition dh_mat (jangle : angle T) loffset llength (ltwist : angle T) : 'M[T]_4 :=
hRx ltwist * hTx llength * hTz loffset * hRz jangle.
Expand Down Expand Up @@ -190,7 +190,7 @@ Local Open Scope frame_scope.

Section denavit_hartenberg_convention.

Variable T : rcfType.
Variable T : realType.
Variables F0 F1 : tframe T.
Definition From1To0 := locked (F1 _R^ F0).
Definition p1_in_0 : 'rV[T]_3 := (\o{F1} - \o{F0}) *m (can_tframe T) _R^ F0.
Expand Down Expand Up @@ -444,7 +444,7 @@ End denavit_hartenberg_convention.
(* TODO: in progress, [angeles] p.141-142 *)
Module Joint.
Section joint.
Variable T : rcfType.
Variable T : realType.
Let vector := 'rV[T]_3.
Record t := mk {
vaxis : vector ;
Expand All @@ -455,7 +455,7 @@ End Joint.

Module Link.
Section link.
Variable T : rcfType.
Variable T : realType.
Record t := mk {
length : T ; (* nonnegative, distance between to successive joint axes *)
offset : T ; (* between to successive X axes *)
Expand All @@ -467,7 +467,7 @@ End Link.

Section open_chain.

Variable T : rcfType.
Variable T : realType.
Let point := 'rV[T]_3.
Let vector := 'rV[T]_3.
Let frame := tframe T.
Expand Down
8 changes: 4 additions & 4 deletions differential_kinematics.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -612,18 +612,18 @@ End derivable_FromTo.

(* the coordinate transformation of a point P1 from frame F1 to frame F
(eqn 2.33, 3.10) *)
Definition coortrans (R : rcfType) (F : tframe [ringType of R^o]) (F1 : rframe F)
Definition coortrans (R : realType) (F : tframe [ringType of R^o]) (F1 : rframe F)
(P1 : bvec F1) : bvec F :=
RFrame.o F1 \+b rmap F (FramedVect_of_Bound P1).

(* motion of P1 w.r.t. the fixed frame F (eqn B.2) *)
Definition motion (R : rcfType) (F : tframe [ringType of R^o]) (F1 : R -> rframe F)
Definition motion (R : realType) (F : tframe [ringType of R^o]) (F1 : R -> rframe F)
(P1 : forall t, bvec (F1 t)) t : bvec F := coortrans (P1 t).

(* [sciavicco] p.351-352 *)
Section kinematics.

Variables (R : rcfType) (F : tframe [ringType of R^o]). (* fixed frame *)
Variables (R : realType) (F : tframe [ringType of R^o]). (* fixed frame *)
Variable F1 : R -> rframe F. (* time-varying frame (origin and basis in F) *)
Hypothesis derivable_F1 : forall t, derivable_mx F1 t 1.
Hypothesis derivable_F1o : forall t, derivable_mx (@TFrame.o [ringType of R^o] \o F1) t 1.
Expand Down Expand Up @@ -728,7 +728,7 @@ End kinematics.
(* [sciavicco] p.81-82 *)
Section derivative_of_a_rotation_matrix_contd.

Variables (R : rcfType) (F : tframe [ringType of R^o]).
Variables (R : realType) (F : tframe [ringType of R^o]).
Variable F1 : R -> rframe F.
Hypothesis derivable_F1 : forall t, derivable_mx F1 t 1.
Variable p1 : forall t, bvec (F1 t).
Expand Down
40 changes: 20 additions & 20 deletions frame.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum rat poly.
From mathcomp Require Import closed_field polyrcf matrix mxalgebra mxpoly zmodp.
From mathcomp Require Import realalg complex fingroup perm.
Require Import ssr_ext angle euclidean skew vec_angle.
From mathcomp.analysis Require Import forms.
From mathcomp.analysis Require Import reals forms.

(******************************************************************************)
(* Frames *)
Expand Down Expand Up @@ -90,7 +90,7 @@ Notation "f '|,' i" := (NOFrame.rowframe f i) : frame_scope.
Local Open Scope frame_scope.

Section non_oriented_frame_properties.
Variable T : rcfType.
Variable T : realType.
Let vector := 'rV[T]_3.
Implicit Types p : 'rV[T]_3.
Variable f : noframe T.
Expand Down Expand Up @@ -313,7 +313,7 @@ Coercion noframe_of_frame (T : ringType) (f : frame T) : noframe T :=
Frame.noframe_of f.

Section oriented_frame_properties.
Variables (T : rcfType) (f : Frame.t T).
Variables (T : realType) (f : Frame.t T).
Local Notation "'i'" := (f |, 0).
Local Notation "'j'" := (f |, 1).
Local Notation "'k'" := (f |, 2%:R).
Expand Down Expand Up @@ -427,7 +427,7 @@ Definition can_tframe := TFrame.mk 0 can_frame.

End canonical_frame.

Lemma basis_change (T : rcfType) (M : 'M[T]_3) (F : noframe T) (A : 'M[T]_3) :
Lemma basis_change (T : realType) (M : 'M[T]_3) (F : noframe T) (A : 'M[T]_3) :
let i := F |, 0 in
let j := F |, 1 in
let k := F |, 2%:R in
Expand All @@ -448,7 +448,7 @@ Qed.

Module Base1.
Section base1.
Variables (T : rcfType) (i : 'rV[T]_3).
Variables (T : realType) (i : 'rV[T]_3).
Hypothesis normi : norm i = 1.
Import rv3LieAlgebra.Exports.

Expand Down Expand Up @@ -501,7 +501,7 @@ Definition frame := Frame.mk is_SO.
End base1.

Section base1_lemmas.
Variable T : rcfType.
Variable T : realType.

(* NB: for information *)
Lemma je0 : j 'e_0 = 'e_1 :> 'rV[T]_3.
Expand All @@ -525,15 +525,15 @@ Qed.
End base1_lemmas.
End Base1.

Canonical base1_is_noframe (T : rcfType) (u : 'rV[T]_3) (u1 : norm u = 1) :=
Canonical base1_is_noframe (T : realType) (u : 'rV[T]_3) (u1 : norm u = 1) :=
NOFrameInterface.mk u1 (Base1.normj u1) (Base1.normk u1)
(Base1.idotj u1) (Base1.jdotk u) (Base1.idotk u).

Canonical noframe_subtype (T : rcfType) := [subType for @NOFrame.M T].

Module Base.
Section build_base.
Variables (T : rcfType) (u : 'rV[T]_3).
Variables (T : realType) (u : 'rV[T]_3).

Definition i := if u == 0 then 'e_0 else normalize u.
Definition j := if u == 0 then 'e_1 else Base1.j i.
Expand Down Expand Up @@ -588,7 +588,7 @@ Proof. by rewrite !rowframeE -col_mx3_rowE Frame.MSO. Qed.
End build_base.

Section build_base_lemmas.
Variables (T : rcfType) (u : 'rV[T]_3).
Variables (T : realType) (u : 'rV[T]_3).

Lemma frame0 : frame 0 = can_frame T.
Proof.
Expand Down Expand Up @@ -731,22 +731,22 @@ End build_base_lemmas.

End Base.

Lemma colinear_frame0a (T : rcfType) (u : 'rV[T]_3) : colinear (Base.frame u)|,0 u.
Lemma colinear_frame0a (T : realType) (u : 'rV[T]_3) : colinear (Base.frame u)|,0 u.
Proof.
case/boolP : (u == 0) => [/eqP ->|u0]; first by rewrite colinear0.
by rewrite -Base.iE /Base.i (negbTE u0) scale_colinear.
Qed.

Lemma colinear_frame0b (T : rcfType) (u : 'rV[T]_3) : colinear u (Base.frame u)|,0.
Lemma colinear_frame0b (T : realType) (u : 'rV[T]_3) : colinear u (Base.frame u)|,0.
Proof. by rewrite colinear_sym colinear_frame0a. Qed.

Definition colinear_frame0 := (colinear_frame0a, colinear_frame0b).

Canonical base_is_noframe (T : rcfType) (u : 'rV[T]_3) :=
Canonical base_is_noframe (T : realType) (u : 'rV[T]_3) :=
NOFrameInterface.mk (Base.normi u) (Base.normj u) (Base.normk u)
(Base.idotj u) (Base.jdotk u) (Base.idotk u).

Canonical frame_is_frame (T : rcfType) (u : 'rV[T]_3) :=
Canonical frame_is_frame (T : realType) (u : 'rV[T]_3) :=
@FrameInterface.mk _ (base_is_noframe u) (Base.icrossj u).

(*Module Frame.
Expand Down Expand Up @@ -782,7 +782,7 @@ Notation "A _R^ B" := (@FromTo _ A B) : frame_scope.

Section FromTo_properties.

Variable T : rcfType.
Variable T : realType.
Implicit Types A B C : frame T.

Lemma FromToE A B : (A _R^ B) = A *m (matrix_of_noframe B)^-1 :> 'M[T]_3.
Expand Down Expand Up @@ -833,7 +833,7 @@ Qed.
End FromTo_properties.

(* TODO: move? *)
Lemma sqr_norm_frame (T : rcfType) (a : frame T) (v : 'rV[T]_3) :
Lemma sqr_norm_frame (T : realType) (a : frame T) (v : 'rV[T]_3) :
norm v ^+ 2 = \sum_(i < 3) (v *d a|,i%:R)^+2.
Proof.
have H : norm v = norm (v *m (can_frame T) _R^ a).
Expand All @@ -842,10 +842,10 @@ rewrite H sqr_norm [in LHS]sum3E [in RHS]sum3E; congr (_ ^+ 2 + _ ^+ 2 + _ ^+ 2)
by rewrite FromTo_from_can mxE_dotmul_row_col -tr_row trmxK row_id NOFrame.rowframeE.
Qed.

Definition noframe_of_FromTo (T : rcfType) (A B : frame T) : noframe T :=
Definition noframe_of_FromTo (T : realType) (A B : frame T) : noframe T :=
NOFrame.mk (FromTo_is_O A B).

Definition frame_of_FromTo (T : rcfType) (B A : frame T) : frame T :=
Definition frame_of_FromTo (T : realType) (B A : frame T) : frame T :=
@Frame.mk _ (noframe_of_FromTo B A) (FromTo_is_SO B A).

Module FramedVect.
Expand All @@ -869,7 +869,7 @@ Proof. by move=> ->. Qed.

Section change_of_coordinate_by_rotation.

Variable T : rcfType.
Variable T : realType.
Implicit Types A B : frame T.

Lemma FramedVectvK A (x : fvec A) : `[FramedVect.v x $ A] = x.
Expand Down Expand Up @@ -944,7 +944,7 @@ End about_frame.*)
(* construction of a frame out of three non-colinear points *)
Module triad.
Section triad.
Variable T : rcfType.
Variable T : realType.
Let point := 'rV[T]_3.

Variables a b c : point.
Expand Down Expand Up @@ -1019,7 +1019,7 @@ End triad.
trois points de depart et leurs positions d'arrivee
sample lemma: the rotation obtained behaves like a change of coordinates from left to right *)
Section transformation_given_three_points.
Variable T : rcfType.
Variable T : realType.
Let vector := 'rV[T]_3.
Let point := 'rV[T]_3.

Expand Down
12 changes: 6 additions & 6 deletions quaternion.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum rat poly.
From mathcomp Require Import closed_field polyrcf matrix mxalgebra mxpoly zmodp.
From mathcomp Require Import realalg complex fingroup perm.
Require Import ssr_ext euclidean angle vec_angle frame rot.
From mathcomp.analysis Require Import forms.
From mathcomp.analysis Require Import reals forms.

(******************************************************************************)
(* Quaternions *)
Expand Down Expand Up @@ -419,7 +419,7 @@ End quaternion.
Notation "x '^*q'" := (conjq x) : quat_scope.

Section quaternion1.
Variable R : rcfType.
Variable R : realType.

Definition sqrq (a : quat R) := a.1 ^+ 2 + norm (a.2) ^+ 2.

Expand Down Expand Up @@ -769,7 +769,7 @@ End quaternion1.
Arguments uquat {R}.

Section conjugation.
Variable R : rcfType.
Variable R : realType.
Implicit Types (a : quat R) (v : 'rV[R]_3).

Definition conjugation x v : quat R := x * v%:v * x^*q.
Expand Down Expand Up @@ -806,7 +806,7 @@ Qed.
End conjugation.

Section polar_coordinates.
Variable R : rcfType.
Variable R : realType.
Implicit Types (x : quat R) (v : 'rV[R]_3) (a : angle R).

Definition quat_of_polar a v := mkQuat (cos a) (sin a *: v).
Expand Down Expand Up @@ -1154,7 +1154,7 @@ Canonical dual_unitRing := UnitRingType (dual R) dual_UnitRingMixin.
End dual_number_unit.

Section dual_quaternion.
Variable R : rcfType (*realType*).
Variable R : realType.
Local Open Scope dual_scope.

Definition dquat := @dual (quat_unitRing R).
Expand Down Expand Up @@ -1288,7 +1288,7 @@ Notation "x '^*dq'" := (conjdq x) : dual_scope.

(* TODO: dual quaternions and rigid body transformations *)
Section dquat_rbt.
Variable R : rcfType (*realType*).
Variable R : realType.
Local Open Scope dual_scope.
Implicit Types x : dquat R.

Expand Down
Loading