Require Export Coq.Arith.Plus Coq.Bool.Bool.
Fixpoint evenb (n : nat) : bool :=
match n with
| 0 => true
| S (S n') => evenb n'
| _ => false
end.
Definition double (n : nat) : nat
:= n + n.
Lemma double_S :
forall n : nat, double (S n) = S (S (double n)).
Proof.
intros.
unfold double.
rewrite <- plus_n_Sm.
reflexivity.
Qed.
Lemma double_evenb:
forall n : nat, evenb (double n) = true.
Proof.
induction n.
reflexivity.
rewrite double_S; simpl.
assumption.
Qed.
Definition even (n : nat) : Prop
:= exists m : nat, n = double m.
Corollary evenb_even:
forall n : nat, even n -> evenb n = true.
Proof.
intros n evenn.
destruct evenn.
subst.
now apply double_evenb.
Qed.
Lemma evenb_step:
forall n : nat, evenb n = negb (evenb (S n)).
Proof.
induction n.
reflexivity.
simpl in *. rewrite IHn, negb_involutive.
reflexivity.
Qed.
Corollary evenb_step':
forall n : nat, negb (evenb n) = evenb (S n).
Proof.
intros. rewrite evenb_step, negb_involutive.
reflexivity.
Qed.
Lemma even_upwards:
forall n : nat,
even n -> even (S (S n)).
Proof.
intros n ev.
destruct ev as [m].
exists (S m).
subst.
symmetry.
now apply double_S.
Qed.
Require Export Coq.Init.Wf Coq.Arith.Lt Omega.
Theorem naturals_wellfounded:
well_founded lt.
Proof.
intro x; induction x as [ | n IH];
constructor; intros y ineq.
(* case x = 0 *)
destruct lt_n_O with (n := y); assumption.
(* Inductive case, x = S n *)
destruct (lt_eq_lt_dec n y) as [L | y_lt_n].
destruct L as [ n_lt_y | n_eq_y].
(* case n + 2 <= y +1 <= n+1 *)
apply lt_le_S in ineq.
apply lt_le_S, le_n_S, le_trans with (p := S n) in n_lt_y;
try assumption.
destruct le_Sn_n with (n := S n); assumption.
(* case n = y *)
rewrite <- n_eq_y; intros; assumption.
(* case n < y *)
inversion IH as [ H].
now apply H, y_lt_n.
Qed.
Lemma even_wf:
forall n : nat, (forall m : nat, m < n -> evenb m = true -> even m) -> evenb n = true -> even n.
Proof.
intros n below ceven.
destruct n as [ | n'].
exists 0; reflexivity.
(* n is positive *)
remember (evenb n') as even_n'.
destruct even_n'.
(* case n' is even *)
rewrite <- evenb_step' in ceven.
rewrite Heqeven_n' in ceven.
apply no_fixpoint_negb in ceven.
destruct ceven.
(* case n' is odd *)
destruct n' as [ | n''].
discriminate.
destruct below with (m := n'') as [m ].
constructor; constructor.
simpl in ceven.
assumption.
exists (S m).
subst. symmetry; apply double_S.
Qed.
Lemma even_evenb:
forall n : nat, evenb n = true -> even n.
Proof.
intro n.
eapply well_founded_ind with (A := nat) (P := fun n : nat, evenb n = true -> even n).
now apply naturals_wellfounded.
now apply even_wf.
Qed.
Example even_test: even 1026.
Proof.
apply even_evenb.
reflexivity.
Qed.
Definition evenproof (n : nat) : option (even n).
remember (evenb n) as b.
destruct b.
constructor.
apply even_evenb; congruence.
exact None.
Defined.
Time Eval compute in evenproof 459.
Time Eval compute in evenproof 918.
Check well_founded_ind.