Parity.v 3 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
MARCHE Claude's avatar
MARCHE Claude committed
4
(*  Copyright 2010-2017   --   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.
MARCHE Claude's avatar
MARCHE Claude committed
17 18 19
Require int.Abs.
Require int.ComputerDivision.

20
(* Why3 assumption *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
21
Definition even (n:Z): Prop := exists k:Z, (n = (2%Z * k)%Z).
22 23

(* Why3 assumption *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
24
Definition odd (n:Z): Prop := exists k:Z, (n = ((2%Z * k)%Z + 1%Z)%Z).
25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126

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.
127

128 129 130 131 132 133 134 135 136 137 138
(* Why3 goal *)
Lemma even_mod2 : forall (n:Z), (even n) <->
  ((ZArith.BinInt.Z.rem n 2%Z) = 0%Z).
Proof.
intros n.
rewrite even_is_Zeven.
rewrite <- Zeven_bool_iff.
rewrite Zquot.Zeven_rem.
now rewrite Z.eqb_eq.
Qed.