Abs.v 1.49 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
4
(*  Copyright 2010-2016   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8 9 10 11
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

12 13 14 15 16
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below    *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
17

18
(* Why3 comment *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
19
(* abs is replaced with (ZArith.BinInt.Z.abs x) by the coq driver *)
20

21
(* Why3 goal *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
22 23 24
Lemma abs_def : forall (x:Z), ((0%Z <= x)%Z ->
  ((ZArith.BinInt.Z.abs x) = x)) /\ ((~ (0%Z <= x)%Z) ->
  ((ZArith.BinInt.Z.abs x) = (-x)%Z)).
25 26 27 28 29 30 31 32 33 34
intros x.
split ; intros H.
now apply Zabs_eq.
apply Zabs_non_eq.
apply Znot_gt_le.
contradict H.
apply Zlt_le_weak.
now apply Zgt_lt.
Qed.

35
(* Why3 goal *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
36 37
Lemma Abs_le : forall (x:Z) (y:Z), ((ZArith.BinInt.Z.abs x) <= y)%Z <->
  (((-y)%Z <= x)%Z /\ (x <= y)%Z).
38 39 40 41 42
intros x y.
zify.
omega.
Qed.

43
(* Why3 goal *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
44
Lemma Abs_pos : forall (x:Z), (0%Z <= (ZArith.BinInt.Z.abs x))%Z.
45 46 47
exact Zabs_pos.
Qed.