Commit 8f3ec6cd authored by Guillaume Melquiond's avatar Guillaume Melquiond

Add a Coq realization for int.Div2.

parent a1c9da89
......@@ -865,7 +865,7 @@ endif
ifeq (@enable_coq_libs@,yes)
COQLIBS_INT_FILES = Abs ComputerDivision EuclideanDivision Int MinMax Power
COQLIBS_INT_FILES = Abs ComputerDivision Div2 EuclideanDivision Int MinMax Power
COQLIBS_INT_ALL_FILES = Exponentiation $(COQLIBS_INT_FILES)
COQLIBS_INT = $(addprefix lib/coq/int/, $(COQLIBS_INT_ALL_FILES))
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require Import int.EuclideanDivision.
(* Why3 goal *)
Lemma div2 : forall (x:Z), exists y:Z, (x = (2%Z * y)%Z) \/
(x = ((2%Z * y)%Z + 1%Z)%Z).
Proof.
intros x.
exists (div x 2).
refine (_ (Mod_bound x 2 _) (Div_mod x 2 _)) ; try easy.
intros H1 H2.
simpl in H1.
omega.
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