Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

Parity.v 2.04 KB
Newer Older
1 2
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below    *)
3 4
Require Import BuiltIn.
Require BuiltIn.
5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 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
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.