266 lines
3.9 KiB
Coq
266 lines
3.9 KiB
Coq
Inductive even: nat -> Prop :=
|
|
| EvenO: even 0
|
|
| EvenS: forall n:nat,
|
|
odd n -> even (S n)
|
|
with odd: nat -> Prop :=
|
|
| OddS: forall n:nat,
|
|
even n -> odd (S n).
|
|
|
|
(*
|
|
Print even_ind.
|
|
Scheme even_ind' := Induction for even Sort Prop.
|
|
Print even_ind'.
|
|
*)
|
|
|
|
Fixpoint evenb (n:nat): bool :=
|
|
match n with
|
|
| O => true
|
|
| S n' => oddb n'
|
|
end
|
|
with oddb (n:nat): bool :=
|
|
match n with
|
|
| O => false
|
|
| S n' => evenb n'
|
|
end.
|
|
|
|
Lemma foo: forall n:nat,
|
|
evenb n = true -> oddb (S n) = true.
|
|
Proof.
|
|
intros n H.
|
|
induction n.
|
|
- reflexivity.
|
|
- simpl.
|
|
Abort.
|
|
|
|
Definition evenBP (n: nat): (evenb n = true <-> even n) /\ (oddb n = true <-> odd n).
|
|
Proof.
|
|
induction n.
|
|
- simpl.
|
|
split.
|
|
+ split; intro H; constructor.
|
|
+ split; intro H; inversion H.
|
|
- destruct IHn as [[H0 H1] [H2 H3]].
|
|
simpl.
|
|
split.
|
|
+ split.
|
|
* intro H.
|
|
constructor.
|
|
exact (H2 H).
|
|
* intro H.
|
|
apply H3.
|
|
|
|
Definition evenBP (n: nat): evenb n = true -> even n.
|
|
Proof.
|
|
intros H.
|
|
induction n.
|
|
- constructor.
|
|
- apply EvenS.
|
|
(*
|
|
1 subgoal
|
|
|
|
n : nat
|
|
H : evenb (S n) = true
|
|
IHn : evenb n = true -> even n
|
|
|
|
========================= (1 / 1)
|
|
|
|
odd n
|
|
*)
|
|
|
|
destruct n.
|
|
+ discriminate.
|
|
+ simpl in H.
|
|
simpl.
|
|
|
|
|
|
|
|
(***************************************)
|
|
|
|
|
|
Inductive even: nat -> Prop :=
|
|
| EvenO: even 0
|
|
| EvenS: forall n:nat,
|
|
even n -> even (S (S n)).
|
|
|
|
Example even256: even 256.
|
|
Proof.
|
|
repeat constructor.
|
|
Show Proof.
|
|
Qed.
|
|
|
|
Fixpoint evenb (n:nat): bool :=
|
|
match n with
|
|
| O => true
|
|
| S O => false
|
|
| S (S n') => evenb n'
|
|
end.
|
|
|
|
Fixpoint evenBP (n: nat): evenb n = true -> even n.
|
|
Proof.
|
|
intros H.
|
|
destruct n as [| [|n]].
|
|
- constructor.
|
|
- inversion H.
|
|
- constructor.
|
|
simpl in H.
|
|
exact (evenBP n H).
|
|
Qed.
|
|
|
|
Example even256': even 256.
|
|
Proof.
|
|
apply (evenBP 256).
|
|
simpl; reflexivity.
|
|
Show Proof.
|
|
Qed.
|
|
|
|
(* ✓ *)
|
|
|
|
|
|
(***************************************)
|
|
|
|
Inductive even: nat -> Prop :=
|
|
| EvenO: even 0
|
|
| EvenS: forall n:nat,
|
|
even n -> even (S (S n))
|
|
with odd: nat -> Prop :=
|
|
| Odd1: odd 1
|
|
| OddS: forall n:nat,
|
|
even (S n) -> odd n.
|
|
|
|
Fixpoint evenb (n:nat): bool :=
|
|
match n with
|
|
| O => true
|
|
| S O => false
|
|
| S (S n') => evenb n'
|
|
end.
|
|
|
|
Example even256: even 256.
|
|
Proof.
|
|
repeat constructor.
|
|
Show Proof.
|
|
Qed.
|
|
|
|
Lemma foo: forall n:nat,
|
|
evenb (S n) = negb (evenb n).
|
|
Proof.
|
|
intros n.
|
|
induction n.
|
|
- simpl; reflexivity.
|
|
- rewrite IHn.
|
|
Require Import Bool.
|
|
rewrite negb_involutive.
|
|
simpl.
|
|
reflexivity.
|
|
Qed.
|
|
|
|
Theorem evenBP: forall n:nat,
|
|
evenb n = true -> even n.
|
|
Proof.
|
|
intros n H.
|
|
induction n.
|
|
- constructor.
|
|
-
|
|
|
|
|
|
Require Import Bool.
|
|
Print reflect.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(*********************************************)
|
|
|
|
|
|
Inductive even: nat -> Prop :=
|
|
| EvenO: even 0
|
|
| EvenSS: forall n:nat,
|
|
even n -> even (S (S n)).
|
|
|
|
(*
|
|
Inductive odd: nat -> Prop :=
|
|
| Odd1: odd (S O)
|
|
| OddSS: forall n:nat,
|
|
odd n -> odd (S (S n)).
|
|
|
|
Lemma evenSodd: forall n:nat,
|
|
even n -> odd (S n).
|
|
Proof.
|
|
intros n H.
|
|
induction n.
|
|
- constructor.
|
|
- apply OddSS.
|
|
*)
|
|
|
|
Lemma evenS: forall n:nat,
|
|
even n -> ~(even (S n)).
|
|
Proof.
|
|
intros n H.
|
|
induction n.
|
|
- intro HH.
|
|
|
|
Abort.
|
|
|
|
Lemma even256: even 256.
|
|
Proof.
|
|
repeat constructor.
|
|
Show Proof.
|
|
Qed.
|
|
|
|
Fixpoint evenb (n:nat): bool :=
|
|
match n with
|
|
| O => true
|
|
| S O => false
|
|
| S (S n') => evenb n'
|
|
end.
|
|
|
|
Require Import Arith.
|
|
Print Nat.even.
|
|
Print Nat.Even.
|
|
Search (Nat.Even).
|
|
Print Nat.even_spec.
|
|
|
|
Axiom foo1: forall n:nat,
|
|
~(even n) -> even (S n).
|
|
Axiom foo1': forall n:nat,
|
|
(even n) -> ~(even (S n)).
|
|
|
|
Axiom foo2: forall n:nat,
|
|
evenb n = true -> evenb (S n) = false.
|
|
|
|
Theorem evenBP: forall n:nat,
|
|
evenb n = true -> even n.
|
|
Proof.
|
|
intros n H.
|
|
induction n.
|
|
- constructor.
|
|
-
|
|
(*
|
|
#+BEGIN_OUTPUT (Goal)
|
|
1 subgoal
|
|
|
|
n : nat
|
|
H : evenb (S n) = true
|
|
IHn : evenb n = true -> even n
|
|
|
|
========================= (1 / 1)
|
|
|
|
even (S n)
|
|
#+END_OUTPUT (Goal) *)
|
|
|
|
destruct IHn.
|
|
pose proof (foo2 (S n) H).
|
|
inversion H.
|
|
|
|
apply foo1.
|
|
intro HH.
|
|
apply IHn.
|
|
|
|
o
|