Commit 5c0367f8 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Remove extraneous spaces from Coq output.

parent f66541b2
......@@ -58,9 +58,9 @@ theory int.Int
syntax function (-_) "(-%1)%Z"
syntax predicate (<=) "(%1 <= %2)%Z"
syntax predicate (<) "(%1 < %2)%Z"
syntax predicate (<) "(%1 < %2)%Z"
syntax predicate (>=) "(%1 >= %2)%Z"
syntax predicate (>) "(%1 > %2)%Z"
syntax predicate (>) "(%1 > %2)%Z"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc.Assoc
......@@ -158,9 +158,9 @@ theory real.Real
syntax function inv "(Rinv %1)"
syntax predicate (<=) "(%1 <= %2)%R"
syntax predicate (<) "(%1 < %2)%R"
syntax predicate (<) "(%1 < %2)%R"
syntax predicate (>=) "(%1 >= %2)%R"
syntax predicate (>) "(%1 > %2)%R"
syntax predicate (>) "(%1 > %2)%R"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc.Assoc
......
......@@ -20,7 +20,7 @@ apply ZO_div_mod_eq.
Qed.
(* Why3 goal *)
Lemma Div_bound : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
Lemma Div_bound : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
((0%Z <= (div x y))%Z /\ ((div x y) <= x)%Z).
intros x y (Hx,Hy).
split.
......@@ -38,7 +38,7 @@ Qed.
(* Why3 goal *)
Lemma Mod_bound : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
(((-(Zabs y))%Z < (mod1 x y))%Z /\ ((mod1 x y) < (Zabs y))%Z).
(((-(Zabs y))%Z < (mod1 x y))%Z /\ ((mod1 x y) < (Zabs 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)) _).
......@@ -51,7 +51,7 @@ 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) ->
Lemma Div_sign_pos : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
(0%Z <= (div x y))%Z.
intros x y (Hx, Hy).
apply ZO_div_pos with (1 := Hx).
......@@ -59,7 +59,7 @@ now apply Zlt_le_weak.
Qed.
(* Why3 goal *)
Lemma Div_sign_neg : forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ (0%Z < y)%Z) ->
Lemma Div_sign_neg : forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ (0%Z < y)%Z) ->
((div x y) <= 0%Z)%Z.
intros x y (Hx, Hy).
generalize (ZO_div_pos (-x) y).
......@@ -103,19 +103,19 @@ exact ZOmod_1_r.
Qed.
(* Why3 goal *)
Lemma Div_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> ((div x
Lemma Div_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> ((div x
y) = 0%Z).
exact ZOdiv_small.
Qed.
(* Why3 goal *)
Lemma Mod_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> ((mod1 x
Lemma Mod_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> ((mod1 x
y) = x).
exact ZOmod_small.
Qed.
(* Why3 goal *)
Lemma Div_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\
Lemma Div_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\
(0%Z <= z)%Z)) -> ((div ((x * y)%Z + z)%Z x) = (y + (div z x))%Z).
intros x y z (Hx&Hy&Hz).
rewrite (Zplus_comm y).
......@@ -130,7 +130,7 @@ now rewrite H in Hx.
Qed.
(* Why3 goal *)
Lemma Mod_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\
Lemma Mod_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\
(0%Z <= z)%Z)) -> ((mod1 ((x * y)%Z + z)%Z x) = (mod1 z x)).
intros x y z (Hx&Hy&Hz).
rewrite Zplus_comm, Zmult_comm.
......
......@@ -28,7 +28,7 @@ case Z_le_dec ; intros H ; ring.
Qed.
(* Why3 goal *)
Lemma Div_bound : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
Lemma Div_bound : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
((0%Z <= (div x y))%Z /\ ((div x y) <= x)%Z).
intros x y (Hx,Hy).
unfold div.
......@@ -49,7 +49,7 @@ Qed.
(* Why3 goal *)
Lemma Mod_bound : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> ((0%Z <= (mod1 x
y))%Z /\ ((mod1 x y) < (Zabs y))%Z).
y))%Z /\ ((mod1 x y) < (Zabs y))%Z).
intros x y Zy.
zify.
assert (H1 := Z_mod_neg x y).
......@@ -79,7 +79,7 @@ now rewrite Zmod_1_r, Zdiv_1_r.
Qed.
(* Why3 goal *)
Lemma Div_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> ((div x
Lemma Div_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> ((div x
y) = 0%Z).
intros x y Hxy.
unfold div.
......
......@@ -82,7 +82,7 @@ apply Zgcd_0.
Qed.
(* Why3 goal *)
Lemma gcd_0_neg : forall (a:Z), (a < 0%Z)%Z -> ((gcd a 0%Z) = (-a)%Z).
Lemma gcd_0_neg : forall (a:Z), (a < 0%Z)%Z -> ((gcd a 0%Z) = (-a)%Z).
Proof.
intros a H.
rewrite <- Zabs_non_eq.
......
......@@ -31,7 +31,7 @@ exact ln_1.
Qed.
(* Why3 goal *)
Lemma Log_mul : forall (x:R) (y:R), ((0%R < x)%R /\ (0%R < y)%R) ->
Lemma Log_mul : forall (x:R) (y:R), ((0%R < x)%R /\ (0%R < y)%R) ->
((log (x * y)%R) = ((log x) + (log y))%R).
intros x y (Hx,Hy).
now apply ln_mult.
......@@ -43,7 +43,7 @@ exact ln_exp.
Qed.
(* Why3 goal *)
Lemma Exp_log : forall (x:R), (0%R < x)%R -> ((exp (log x)) = x).
Lemma Exp_log : forall (x:R), (0%R < x)%R -> ((exp (log x)) = x).
exact exp_ln.
Qed.
......
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