Skip to content

Instantly share code, notes, and snippets.

Created June 17, 2021 15:02
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
What would you like to do?
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. …
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment