Skip to content

Instantly share code, notes, and snippets.

@technion

technion/modeven.v

Last active June 7, 2018 10:58
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save technion/eac1b44104597446ea2713983249cc24 to your computer and use it in GitHub Desktop.
Save technion/eac1b44104597446ea2713983249cc24 to your computer and use it in GitHub Desktop.
Download ZIP
Mod Even
Raw
modeven.v
Require Import Coq.Arith.Arith.
Require Import Coq.Arith.EqNat.
(* Definition from : https://coq.inria.fr/library/Coq.Arith.Even.html *)
Inductive even : nat -> Prop :=
| even_O : even 0
| even_S : forall n, odd n -> even (S n)
with odd : nat -> Prop :=
odd_S : forall n, even n -> odd (S n).
Theorem FastEven: forall n: nat, n mod 2 = 0 <-> even n.
Proof.
split.
- intros. induction n.
+ apply even_O.
+ apply even_S.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment