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.