Require Import Arith List.

Fixpoint evenb (n : nat) : bool :=
  match n with
  | 0 => true  | S p => negb (evenb p)
  end.

Definition is_zero (x : nat) :=
   match x with O => true | _ => false end.

Lemma is_zero_l1 :
  forall x, is_zero x = false -> x <> 0.
Proof.
intros x.
unfold is_zero.
intros hyp.
case_eq x.
 intros x0.
 rewrite x0 in hyp.
 discriminate.
intros x' xx'.
discriminate.
Qed.

Lemma is_zero_l2 :
  forall x, is_zero x <> false -> x = 0.
Proof.
intros x.
unfold is_zero.
intros hyp.
destruct x as [ | x'].
 reflexivity.
destruct hyp.
reflexivity.
Qed.

Fixpoint mult2 n :=
  match n with
  | 0 => 0
  | S p => S (S (mult2 p))
  end.

Lemma mult2_add : forall n, mult2 n = n + n.
Proof.
induction n as [ | n' IHn'].
 reflexivity.
change (mult2 (S n')) with (S (S (mult2 n'))).
rewrite IHn'.
SearchAbout (S _ + _).
Check NPeano.Nat.add_succ_l.
SearchAbout (_ + S _).
Check plus_n_Sm.

rewrite plus_n_Sm.
 rewrite NPeano.Nat.add_succ_l.
reflexivity.
Qed.

Lemma mult2_evenb :
  forall n, evenb (mult2 n) = true.
Proof.
induction n as [ | n' IHn'].
 reflexivity.
change (mult2 (S n')) with (S (S (mult2 n'))).
set (x := (S (mult2 n'))).
change (evenb (S x)) with (negb (evenb x)).
unfold x.
change (evenb (S (mult2 n'))) with
  (negb (evenb (mult2 n'))).
rewrite IHn'.
reflexivity.
Qed.


(* I want lo 3 = 5::3::1::nil *)
(* I want lo 2 = 3::1::nil *)
(*        lo 1 = 1::nil *)
(*        l0 0 = nil *)

Fixpoint lo n :=
match n with
| O => nil
| S p => 2 * p + 1:: lo p
end.

Compute lo 5.

Lemma lelo :
  forall n, length (lo n) = n.
Proof.
induction n as [ | n IHn].
 reflexivity.
simpl.
rewrite IHn. 
reflexivity.
Qed.

Fixpoint sl (l : list nat) : nat :=
  match l with
  | nil => 0
  | a::l' => a + sl l'
  end.

Lemma sl_lo : forall n, sl (lo n) = n * n.
Proof.
induction n as [| n IHn].
 reflexivity.
simpl.
rewrite IHn.
ring.
Qed.

Fixpoint lo' (n m : nat) : list nat :=
match n with
| 0 => nil
| S p => m :: lo' p (m + 2)
end.

Definition lo2 n := lo' n 1.

Compute (lo2 5, lo 5).

Lemma lelo' :
  forall n m, length (lo' n m) = n.
Proof.
induction n as [| n IHn ].
  reflexivity.
simpl.
intros m; rewrite IHn.
reflexivity.
Qed.

Lemma lelo2 : 
 forall n, length (lo2 n) = n.
Proof.
intros n.
unfold lo2. rewrite lelo'.
reflexivity.
Qed.

Lemma sl_lo' :
  forall n m, sl (lo' n (m + 1)) = n * m + n * n.
Proof.
induction n as [ | n IHn].
 intros m. 
 simpl.
 reflexivity.
intros m.
simpl.
replace (m + 1 + 2) with ((m + 2) + 1).
 rewrite IHn.
 ring.
ring.
Qed.

Lemma sl_lo2 :
  forall n, sl (lo2 n) = n * n.
Proof.
intros n; unfold lo2. 
replace 1 with (0 + 1).
 rewrite sl_lo'.
 rewrite mult_0_r, NPeano.Nat.add_0_l.
 reflexivity.
rewrite NPeano.Nat.add_0_l.
reflexivity.
Qed.

Lemma evenb_correct1 :
  forall x : nat,  (exists y : nat, x = 2 * y) <->  evenb x = true.