From 12daccee87b77ca0ee0a79878205c166091bc731 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 3 Oct 2011 11:15:39 +0200 Subject: [PATCH] Add a realization of real.square. Remark about the theory: if one considers that the square root is always nonnegative (by definition in Coq), then Lemma Sqrt_positive has an extraneous hypothesis. --- realizations/coq/real/Square.v | 49 ++++++++++++++++++++++++++++++++++ 1 file changed, 49 insertions(+) create mode 100644 realizations/coq/real/Square.v diff --git a/realizations/coq/real/Square.v b/realizations/coq/real/Square.v new file mode 100644 index 000000000..ce9cb4eff --- /dev/null +++ b/realizations/coq/real/Square.v @@ -0,0 +1,49 @@ +(* This file is generated by Why3's Coq driver *) +(* Beware! Only edit allowed sections below *) +Require Import ZArith. +Require Import Rbase. +Require Import R_sqrt. +(*Add Rec LoadPath "/home/guillaume/bin/why3/share/why3/theories".*) +(*Add Rec LoadPath "/home/guillaume/bin/why3/share/why3/modules".*) +Require real.Real. +Definition sqr(x:R): R := (x * x)%R. + +Definition sqrt: R -> R. +(* YOU MAY EDIT THE PROOF BELOW *) +exact sqrt. +Defined. +(* DO NOT EDIT BELOW *) + + +(* YOU MAY EDIT THE CONTEXT BELOW *) + +(* DO NOT EDIT BELOW *) + +Lemma Sqrt_positive : forall (x:R), (0%R <= x)%R -> (0%R <= (sqrt x))%R. +(* YOU MAY EDIT THE PROOF BELOW *) +intros x _. +apply sqrt_pos. +Qed. +(* DO NOT EDIT BELOW *) + +(* YOU MAY EDIT THE CONTEXT BELOW *) + +(* DO NOT EDIT BELOW *) + +Lemma Sqrt_square : forall (x:R), (0%R <= x)%R -> ((sqr (sqrt x)) = x). +(* YOU MAY EDIT THE PROOF BELOW *) +exact sqrt_sqrt. +Qed. +(* DO NOT EDIT BELOW *) + +(* YOU MAY EDIT THE CONTEXT BELOW *) + +(* DO NOT EDIT BELOW *) + +Lemma Square_sqrt : forall (x:R), (0%R <= x)%R -> ((sqrt (x * x)%R) = x). +(* YOU MAY EDIT THE PROOF BELOW *) +exact sqrt_square. +Qed. +(* DO NOT EDIT BELOW *) + + -- 2.24.1