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
 Guillaume Melquiond committed Apr 21, 2012 1 2 ``````(* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) `````` MARCHE Claude committed Sep 11, 2012 3 4 ``````Require Import BuiltIn. Require BuiltIn. `````` Guillaume Melquiond committed Apr 21, 2012 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. ``````