Commit 0b992ae5 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Add a realization for number.Parity.

parent f543b7ce
......@@ -878,13 +878,16 @@ COQLIBS_INT = $(addprefix lib/coq/int/, $(COQLIBS_INT_FILES))
COQLIBS_REAL_FILES = Abs ExpLog FromInt MinMax Real Square RealInfix
COQLIBS_REAL = $(addprefix lib/coq/real/, $(COQLIBS_REAL_FILES))
COQLIBS_NUMBER_FILES = Parity
COQLIBS_NUMBER = $(addprefix lib/coq/number/, $(COQLIBS_NUMBER_FILES))
ifeq (@enable_coq_fp_libs@,yes)
COQLIBS_FP_FILES = Rounding Single Double
COQLIBS_FP_ALL_FILES = GenFloat $(COQLIBS_FP_FILES)
COQLIBS_FP = $(addprefix lib/coq/floating_point/, $(COQLIBS_FP_ALL_FILES))
endif
COQLIBS_FILES = $(COQLIBS_INT) $(COQLIBS_REAL) $(COQLIBS_FP)
COQLIBS_FILES = $(COQLIBS_INT) $(COQLIBS_REAL) $(COQLIBS_NUMBER) $(COQLIBS_FP)
COQV = $(addsuffix .v, $(COQLIBS_FILES))
COQVO = $(addsuffix .vo, $(COQLIBS_FILES))
......@@ -905,6 +908,8 @@ drivers/coq-realizations.aux: Makefile
echo 'theory int.'"$$f"' meta "realized" "int.'"$$f"'", "" end'; done; \
for f in $(COQLIBS_REAL_FILES); do \
echo 'theory real.'"$$f"' meta "realized" "real.'"$$f"'", "" end'; done; \
for f in $(COQLIBS_NUMBER_FILES); do \
echo 'theory number.'"$$f"' meta "realized" "number.'"$$f"'", "" end'; done; \
for f in $(COQLIBS_FP_FILES); do \
echo 'theory floating_point.'"$$f"' meta "realized" "floating_point.'"$$f"'", "" end'; done; \
) > $@
......@@ -917,6 +922,8 @@ install_no_local::
cp $(addsuffix .vo, $(COQLIBS_INT)) $(LIBDIR)/why3/coq/int/
mkdir -p $(LIBDIR)/why3/coq/real
cp $(addsuffix .vo, $(COQLIBS_REAL)) $(LIBDIR)/why3/coq/real/
mkdir -p $(LIBDIR)/why3/coq/number
cp $(addsuffix .vo, $(COQLIBS_NUMBER)) $(LIBDIR)/why3/coq/number/
ifeq (@enable_coq_fp_libs@,yes)
mkdir -p $(LIBDIR)/why3/coq/floating_point
cp $(addsuffix .vo, $(COQLIBS_FP)) $(LIBDIR)/why3/coq/floating_point/
......@@ -937,6 +944,7 @@ clean::
update-coq: bin/why3 drivers/coq-realizations.aux
for f in $(COQLIBS_INT_FILES); do bin/why3 --realize -D drivers/coq-realize.drv -T int.$$f -o lib/coq/int/; done
for f in $(COQLIBS_REAL_FILES); do bin/why3 --realize -D drivers/coq-realize.drv -T real.$$f -o lib/coq/real/; done
for f in $(COQLIBS_NUMBER_FILES); do bin/why3 --realize -D drivers/coq-realize.drv -T number.$$f -o lib/coq/number/; done
for f in $(COQLIBS_FP_FILES); do bin/why3 --realize -D drivers/coq-realize.drv -T floating_point.$$f -o lib/coq/floating_point/; done
else
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require int.Int.
(* Why3 assumption *)
Definition even(n:Z): Prop := exists k:Z, (n = (2%Z * k)%Z).
(* Why3 assumption *)
Definition odd(n:Z): Prop := exists k:Z, (n = ((2%Z * k)%Z + 1%Z)%Z).
Lemma even_is_Zeven :
forall n, even n <-> Zeven n.
Proof.
intros n.
refine (conj _ (Zeven_ex n)).
intros (k,H).
rewrite H.
apply Zeven_2p.
Qed.
Lemma odd_is_Zodd :
forall n, odd n <-> Zodd n.
Proof.
intros n.
refine (conj _ (Zodd_ex n)).
intros (k,H).
rewrite H.
apply Zodd_2p_plus_1.
Qed.
(* Why3 goal *)
Lemma even_or_odd : forall (n:Z), (even n) \/ (odd n).
Proof.
intros n.
destruct (Zeven_odd_dec n).
left.
now apply <- even_is_Zeven.
right.
now apply <- odd_is_Zodd.
Qed.
(* Why3 goal *)
Lemma even_not_odd : forall (n:Z), (even n) -> ~ (odd n).
Proof.
intros n H1 H2.
apply (Zeven_not_Zodd n).
now apply -> even_is_Zeven.
now apply -> odd_is_Zodd.
Qed.
(* Why3 goal *)
Lemma odd_not_even : forall (n:Z), (odd n) -> ~ (even n).
Proof.
intros n H1.
contradict H1.
now apply even_not_odd.
Qed.
(* Why3 goal *)
Lemma even_odd : forall (n:Z), (even n) -> (odd (n + 1%Z)%Z).
Proof.
intros n H.
apply <- odd_is_Zodd.
apply Zeven_plus_Zodd.
now apply -> even_is_Zeven.
easy.
Qed.
(* Why3 goal *)
Lemma odd_even : forall (n:Z), (odd n) -> (even (n + 1%Z)%Z).
Proof.
intros n H.
apply <- even_is_Zeven.
apply Zodd_plus_Zodd.
now apply -> odd_is_Zodd.
easy.
Qed.
(* Why3 goal *)
Lemma even_even : forall (n:Z), (even n) -> (even (n + 2%Z)%Z).
Proof.
intros n H.
apply <- even_is_Zeven.
apply Zeven_plus_Zeven.
now apply -> even_is_Zeven.
easy.
Qed.
(* Why3 goal *)
Lemma odd_odd : forall (n:Z), (odd n) -> (odd (n + 2%Z)%Z).
Proof.
intros n H.
apply <- odd_is_Zodd.
apply Zodd_plus_Zeven.
now apply -> odd_is_Zodd.
easy.
Qed.
(* Why3 goal *)
Lemma even_2k : forall (k:Z), (even (2%Z * k)%Z).
Proof.
intros k.
now exists k.
Qed.
(* Why3 goal *)
Lemma odd_2k1 : forall (k:Z), (odd ((2%Z * k)%Z + 1%Z)%Z).
Proof.
intros k.
now exists k.
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