Commit efa0940b authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fully qualify native Coq symbols that are not scope operators.

parent a20c3a42
......@@ -35,11 +35,11 @@ end
theory bool.Bool
syntax function andb "(andb %1 %2)"
syntax function orb "(orb %1 %2)"
syntax function xorb "(xorb %1 %2)"
syntax function notb "(negb %1)"
syntax function implb "(implb %1 %2)"
syntax function andb "(Init.Datatypes.andb %1 %2)"
syntax function orb "(Init.Datatypes.orb %1 %2)"
syntax function xorb "(Init.Datatypes.xorb %1 %2)"
syntax function notb "(Init.Datatypes.negb %1)"
syntax function implb "(Init.Datatypes.implb %1 %2)"
end
......@@ -83,7 +83,7 @@ end
theory int.Abs
syntax function abs "(Zabs %1)"
syntax function abs "(ZArith.BinInt.Z.abs %1)"
remove prop Abs_pos
......@@ -91,8 +91,8 @@ end
theory int.MinMax
syntax function min "(Zmin %1 %2)"
syntax function max "(Zmax %1 %2)"
syntax function min "(ZArith.BinInt.Z.min %1 %2)"
syntax function max "(ZArith.BinInt.Z.max %1 %2)"
end
......@@ -102,10 +102,8 @@ end
theory int.EuclideanDivision
prelude "Require Import Zdiv."
syntax function div "(Zdiv %1 %2)"
syntax function mod "(Zmod %1 %2)"
syntax function div "(ZArith.BinInt.Z.div %1 %2)"
syntax function mod "(ZArith.BinInt.Z.modulo %1 %2)"
remove prop Div_mod
remove prop Div_bound
......@@ -118,14 +116,12 @@ end
theory int.ComputerDivision
(* Coq Z0div provides the division and modulo operators
(* Coq provides the division and modulo operators
with the same convention as mainstream programming language
such C, Java, OCaml *)
prelude "Require Import ZOdiv."
syntax function div "(ZOdiv %1 %2)"
syntax function mod "(ZOmod %1 %2)"
syntax function div "(ZArith.BinInt.Z.quot %1 %2)"
syntax function mod "(ZArith.BinInt.Z.rem %1 %2)"
remove prop Div_mod
remove prop Div_bound
......@@ -154,8 +150,8 @@ theory real.Real
syntax function (-) "(%1 - %2)%R"
syntax function (-_) "(-%1)%R"
syntax function (*) "(%1 * %2)%R"
syntax function (/) "(Rdiv %1 %2)%R"
syntax function inv "(Rinv %1)"
syntax function (/) "(%1 / %2)%R"
syntax function inv "(Reals.Rdefinitions.Rinv %1)"
syntax predicate (<=) "(%1 <= %2)%R"
syntax predicate (<) "(%1 < %2)%R"
......@@ -205,9 +201,9 @@ end
theory real.Abs
prelude "Require Import Rbasic_fun."
prelude "Require Reals.Rbasic_fun."
syntax function abs "(Rabs %1)"
syntax function abs "(Reals.Rbasic_fun.Rabs %1)"
remove prop Abs_le
remove prop Abs_pos
......@@ -216,7 +212,7 @@ end
theory real.FromInt
syntax function from_int "(IZR %1)"
syntax function from_int "(Reals.Raxioms.IZR %1)"
remove prop Zero
remove prop One
......@@ -229,10 +225,10 @@ end
theory real.Square
prelude "Require Import R_sqrt."
prelude "Require Reals.R_sqrt."
syntax function sqr "(Rsqr %1)"
syntax function sqrt "(sqrt %1)" (* and not Rsqrt *)
syntax function sqr "(Reals.RIneq.Rsqr %1)"
syntax function sqrt "(Reals.R_sqrt.sqrt %1)" (* and not Rsqrt *)
remove prop Sqrt_positive
remove prop Sqrt_square
......@@ -242,11 +238,11 @@ end
theory real.ExpLog
prelude "Require Import Rtrigo_def."
prelude "Require Import Rpower."
prelude "Require Reals.Rtrigo_def."
prelude "Require Reals.Rpower."
syntax function exp "(exp %1)"
syntax function log "(ln %1)"
syntax function exp "(Reals.Rtrigo_def.exp %1)"
syntax function log "(Reals.Rpower.ln %1)"
remove prop Exp_zero
remove prop Exp_sum
......@@ -259,9 +255,9 @@ end
theory real.PowerInt
prelude "Require Import Rfunctions."
prelude "Require Reals.Rfunctions."
syntax function power "(powerRZ %1 %2)"
syntax function power "(Reals.Rfunctions.powerRZ %1 %2)"
remove prop Power_0 (* already as powerRZ_O *)
(* remove prop Power_s *)
......@@ -274,8 +270,8 @@ end
theory list.List
syntax type list "(list %1)"
syntax function Nil "nil"
syntax function Cons "(cons %1 %2)"
syntax function Nil "Init.Datatypes.nil"
syntax function Cons "(Init.Datatypes.cons %1 %2)"
end
......@@ -294,8 +290,8 @@ end
theory option.Option
syntax type option "(option %1)"
syntax function None "None"
syntax function Some "(Some %1)"
syntax function None "Init.Datatypes.None"
syntax function Some "(Init.Datatypes.Some %1)"
end
......
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require Import ZOdiv.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require Import Zquot.
(* Why3 comment *)
(* div is replaced with (ZOdiv x x1) by the coq driver *)
(* div is replaced with (ZArith.BinInt.Z.quot x x1) by the coq driver *)
(* Why3 comment *)
(* mod1 is replaced with (ZOmod x x1) by the coq driver *)
(* mod1 is replaced with (ZArith.BinInt.Z.rem x x1) by the coq driver *)
(* Why3 goal *)
Lemma Div_mod : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
(x = ((y * (ZOdiv x y))%Z + (ZOmod x y))%Z).
(x = ((y * (ZArith.BinInt.Z.quot x y))%Z + (ZArith.BinInt.Z.rem x y))%Z).
intros x y _.
apply ZO_div_mod_eq.
apply Z.quot_rem'.
Qed.
(* Why3 goal *)
Lemma Div_bound : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
((0%Z <= (ZOdiv x y))%Z /\ ((ZOdiv x y) <= x)%Z).
((0%Z <= (ZArith.BinInt.Z.quot x y))%Z /\
((ZArith.BinInt.Z.quot x y) <= x)%Z).
intros x y (Hx,Hy).
split.
apply ZO_div_pos with (1 := Hx).
now apply Zlt_le_weak.
now apply Z.quot_pos.
destruct (Z_eq_dec y 1) as [H|H].
rewrite H, ZOdiv_1_r.
rewrite H, Z.quot_1_r.
apply Zle_refl.
destruct (Zle_lt_or_eq 0 x Hx) as [H'|H'].
apply Zlt_le_weak.
apply ZO_div_lt with (1 := H').
apply Z.quot_lt with (1 := H').
omega.
now rewrite <- H', ZOdiv_0_l.
now rewrite <- H', Zquot_0_l.
Qed.
(* Why3 goal *)
Lemma Mod_bound : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
(((-(Zabs y))%Z < (ZOmod x y))%Z /\ ((ZOmod x y) < (Zabs y))%Z).
(((-(ZArith.BinInt.Z.abs y))%Z < (ZArith.BinInt.Z.rem x y))%Z /\
((ZArith.BinInt.Z.rem x y) < (ZArith.BinInt.Z.abs y))%Z).
intros x y Zy.
destruct (Zle_or_lt 0 x) as [Hx|Hx].
refine ((fun H => conj (Zlt_le_trans _ 0 _ _ (proj1 H)) (proj2 H)) _).
clear -Zy ; zify ; omega.
now apply ZOmod_lt_pos.
now apply Zrem_lt_pos.
refine ((fun H => conj (proj1 H) (Zle_lt_trans _ 0 _ (proj2 H) _)) _).
clear -Zy ; zify ; omega.
apply ZOmod_lt_neg with (2 := Zy).
apply Zrem_lt_neg with (2 := Zy).
now apply Zlt_le_weak.
Qed.
(* Why3 goal *)
Lemma Div_sign_pos : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
(0%Z <= (ZOdiv x y))%Z.
(0%Z <= (ZArith.BinInt.Z.quot x y))%Z.
intros x y (Hx, Hy).
apply ZO_div_pos with (1 := Hx).
now apply Zlt_le_weak.
now apply Z.quot_pos.
Qed.
(* Why3 goal *)
Lemma Div_sign_neg : forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ (0%Z < y)%Z) ->
((ZOdiv x y) <= 0%Z)%Z.
((ZArith.BinInt.Z.quot x y) <= 0%Z)%Z.
intros x y (Hx, Hy).
generalize (ZO_div_pos (-x) y).
rewrite ZOdiv_opp_l.
generalize (Z.quot_pos (-x) y).
rewrite Zquot_opp_l.
omega.
Qed.
(* Why3 goal *)
Lemma Mod_sign_pos : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ ~ (y = 0%Z)) ->
(0%Z <= (ZOmod x y))%Z.
(0%Z <= (ZArith.BinInt.Z.rem x y))%Z.
intros x y (Hx, Zy).
now apply ZOmod_lt_pos.
now apply Zrem_lt_pos.
Qed.
(* Why3 goal *)
Lemma Mod_sign_neg : forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ ~ (y = 0%Z)) ->
((ZOmod x y) <= 0%Z)%Z.
((ZArith.BinInt.Z.rem x y) <= 0%Z)%Z.
intros x y (Hx, Zy).
now apply ZOmod_lt_neg.
now apply Zrem_lt_neg.
Qed.
(* Why3 goal *)
Lemma Rounds_toward_zero : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
((Zabs ((ZOdiv x y) * y)%Z) <= (Zabs x))%Z.
((ZArith.BinInt.Z.abs ((ZArith.BinInt.Z.quot x y) * y)%Z) <= (ZArith.BinInt.Z.abs x))%Z.
intros x y Zy.
rewrite Zmult_comm.
zify.
generalize (ZO_mult_div_le x y).
generalize (ZO_mult_div_ge x y).
generalize (Z.mul_quot_le x y).
generalize (Z.mul_quot_ge x y).
omega.
Qed.
(* Why3 goal *)
Lemma Div_1 : forall (x:Z), ((ZOdiv x 1%Z) = x).
exact ZOdiv_1_r.
Lemma Div_1 : forall (x:Z), ((ZArith.BinInt.Z.quot x 1%Z) = x).
exact Z.quot_1_r.
Qed.
(* Why3 goal *)
Lemma Mod_1 : forall (x:Z), ((ZOmod x 1%Z) = 0%Z).
exact ZOmod_1_r.
Lemma Mod_1 : forall (x:Z), ((ZArith.BinInt.Z.rem x 1%Z) = 0%Z).
exact Z.rem_1_r.
Qed.
(* Why3 goal *)
Lemma Div_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) ->
((ZOdiv x y) = 0%Z).
exact ZOdiv_small.
((ZArith.BinInt.Z.quot x y) = 0%Z).
exact Z.quot_small.
Qed.
(* Why3 goal *)
Lemma Mod_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) ->
((ZOmod x y) = x).
exact ZOmod_small.
((ZArith.BinInt.Z.rem x y) = x).
exact Z.rem_small.
Qed.
(* Why3 goal *)
Lemma Div_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\
(0%Z <= z)%Z)) -> ((ZOdiv ((x * y)%Z + z)%Z x) = (y + (ZOdiv z x))%Z).
(0%Z <= z)%Z)) ->
((ZArith.BinInt.Z.quot ((x * y)%Z + z)%Z x) = (y + (ZArith.BinInt.Z.quot z x))%Z).
intros x y z (Hx&Hy&Hz).
rewrite (Zplus_comm y).
rewrite <- ZO_div_plus.
rewrite <- Z_quot_plus.
now rewrite Zplus_comm, Zmult_comm.
apply Zmult_le_0_compat with (2 := Hz).
apply Zplus_le_0_compat with (1 := Hz).
......@@ -131,10 +133,11 @@ Qed.
(* Why3 goal *)
Lemma Mod_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\
(0%Z <= z)%Z)) -> ((ZOmod ((x * y)%Z + z)%Z x) = (ZOmod z x)).
(0%Z <= z)%Z)) ->
((ZArith.BinInt.Z.rem ((x * y)%Z + z)%Z x) = (ZArith.BinInt.Z.rem z x)).
intros x y z (Hx&Hy&Hz).
rewrite Zplus_comm, Zmult_comm.
apply ZO_mod_plus.
apply Z_rem_plus.
apply Zmult_le_0_compat with (2 := Hz).
apply Zplus_le_0_compat with (1 := Hz).
apply Zmult_le_0_compat with (1 := Hy).
......
......@@ -179,9 +179,9 @@ Lemma mod_divides_computer : forall (a:Z) (b:Z), (~ (b = 0%Z)) ->
(((ZOmod a b) = 0%Z) -> (divides b a)).
Proof.
intros a b Zb H.
exists (ZOdiv a b).
exists (Z.quot a b).
rewrite Zmult_comm.
now apply ZO_div_exact_full_2.
now apply Zquot.Z_quot_exact_full.
Qed.
(* Why3 goal *)
......@@ -190,7 +190,7 @@ Lemma divides_mod_computer : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> ((divides b
Proof.
intros a b Zb (q,H).
rewrite H.
apply ZO_mod_mult.
apply Zquot.Z_rem_mult.
Qed.
(* Why3 goal *)
......
......@@ -119,9 +119,9 @@ Lemma Gcd_computer_mod : forall (a:Z) (b:Z), (~ (b = 0%Z)) -> ((gcd b
Proof.
intros a b _.
rewrite (Zgcd_comm a b).
rewrite (gcd_euclid b a (ZOdiv a b)).
rewrite (gcd_euclid b a (Z.quot a b)).
apply f_equal.
rewrite (ZO_div_mod_eq a b) at 2.
rewrite (Z.quot_rem' a b) at 2.
ring.
Qed.
......
......@@ -5,6 +5,8 @@ Require Import Rbasic_fun.
Require BuiltIn.
Require real.Real.
Import Rbasic_fun.
(* Why3 comment *)
(* abs is replaced with (Rabs x) by the coq driver *)
......
......@@ -6,6 +6,9 @@ Require Import Rpower.
Require BuiltIn.
Require real.Real.
Import Rtrigo_def.
Import Rpower.
(* Why3 comment *)
(* exp is replaced with (exp x) by the coq driver *)
......
......@@ -8,6 +8,7 @@ Require real.Real.
Require real.RealInfix.
Require Import Exponentiation.
Import Rfunctions.
(* Why3 comment *)
(* power is replaced with (powerRZ x x1) by the coq driver *)
......
......@@ -5,6 +5,8 @@ Require Import R_sqrt.
Require BuiltIn.
Require real.Real.
Import R_sqrt.
(* Why3 goal *)
Lemma sqr_def : forall (x:R), ((Rsqr x) = (x * x)%R).
reflexivity.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment