rational.v

From Coq Require Import Unicode.Utf8.
From Coq Require Import Logic.Decidable.
From Coq Require Import QArith.
From Coq Require Import Vectors.Vector.

Notation ℕ := nat.
Notation ℙ := Prop.
Notation 𝔹 := bool.
Notation ℤ := Z.
Notation ℚ := Q.

Import VectorNotations.

Definition vector {dimension: ℕ} := t ℚ dimension.

Example e₀ := [ 7#2 ; 5#3 ].

Definition Root (power: ℤ) (number: ℚ) := {root: ℚ | root^power = number}.

Definition speed {dimension: ℕ} (velocity: vector) := Root 2 (@fold_left _ _ Qplus 0 dimension (map (fun x => x^2) velocity)).

Example e₂ := speed e₀.

Compute e₂.

Example e₂_computes: ∃ (x: ℚ), e₂ = Root 2 x.
Proof with eauto. unfold e₂, e₀, speed, Qplus... Defined.

Example e₂_computed: ℚ.
pose e₂_computes. …