(** Let us redefine some functions of the standard library, So we mask some results that are used in normal use of Coq *) Require Arith. Require Import List. (* define the predecessor function *) Definition pred (n : nat) : nat := n (* dummy definition to be replaced*). (** simplifications *) Lemma pred_S : forall n, pred (S n) = n. Proof. (* do the proof *) Admitted. (* Print pred_S.*) Lemma S_pred : forall n, 0 <> n -> S (pred n) = n. Proof. (* do the proof *) Admitted. Lemma zero_neq_one: 0 <> 1. Proof. Admitted. (*Print zero_neq_one.*) (** we could use "case" but with less intros *) Lemma S_pred' : forall n, 0 <> n -> S (pred n) = n. Proof. intros n. case n. intro H; now destruct H. reflexivity. Qed. (** using case_eq *) Lemma S_pred'' : forall n, 0 <> n -> S (pred n) = n. Proof. intros n H. case_eq n. intro H0;now destruct H. reflexivity. Qed. (** New : rewrite H rewrite (H x) rewrite <- H. rewrite H in H0. *) Lemma pred_0: forall n, pred n = 0 -> n = 0 \/ n = 1. Proof. Admitted. Lemma list_decompose : forall A (l:list A) , l = nil \/ exists a l', l = a::l'. Proof. Admitted (** recursive functions *) (* define addition *) Fixpoint my_plus (n m : nat) : nat := n. Notation "n + p" := (my_plus n p) : nat_scope. (* define multiplication *) Fixpoint my_mult (n m : nat) := n. Notation "n * p" := (my_mult n p) : nat_scope. Compute 9 * 3 + 9. (** immediate simplifications *) Lemma plus_0_n : forall n, 0 + n = n. Proof. Admitted. Lemma plus_Sm_n : forall m n, S m + n = S (m + n). Proof. Admitted. (** Proofs by cases *) Lemma plus_zero_l : forall n p, n + p = 0 -> n = 0. Proof. Admitted. Lemma plus_zero : forall n p, n + p = 0 -> n = 0 /\ p = 0. Proof. Admitted. Lemma plus_m_0 : forall m, m + 0 = m. Proof. Admitted. Lemma plus_m_Sn : forall m n, m + S n = S (m + n). Proof. Admitted. Lemma plus_comm : forall n p, n + p = p + n. Proof. Admitted (** Now we can go back to mult_1 *) Lemma mult_1 : forall n, 1 * n = n. Proof. Admitted. (** Exercises *) Lemma plus_assoc : forall n p q, n + (p + q) = (n + p) + q. Proof. Admitted. Lemma mult_m_0 : forall n: nat, n * 0 = 0. Proof. Admitted. Lemma mult_com : forall n p, n * p = p * n. Proof. Admitted. (** induction on lists *) Open Scope list_scope. (* define list concatenation *) Fixpoint app {A:Type}(l l':list A): list A := l. Infix "++" := app (right associativity, at level 60) : list_scope. (* ++ in StdLib *) (* define list reversal *) Fixpoint rev {A:Type}(l:list A) : list A := l. Lemma app_assoc : forall {A:Type}(l1 l2 l3: list A), l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3. Proof. Admitted. Lemma rev_rev {A} (l:list A) : rev (rev l) = l. Proof. Admitted. Lemma rev_of_app {A:Type} : forall l1 l2 : list A, rev (l1 ++ l2) = rev l2 ++ rev l1. Proof. Admitted (** program equivalence *) Fixpoint rev_app {A}(l1 l2:list A) : list A := match l1 with nil => l2 | a::l'1 => rev_app l'1 (a::l2) end. Definition fast_rev {A}(l: list A) := rev_app l nil. Theorem fast_rev_correct : forall A (l:list A), rev l = fast_rev l. Proof. Admitted. (** Recursive predicates *) Fixpoint In {A}(a:A)(l:list A) : Prop := match l with nil => False | x::l' => a = x \/ In a l' end. Lemma In_app : forall A (a:A)(l1 l2:list A), In a (l1 ++ l2) <-> In a l1 \/ In a l2. Proof. Admitted Lemma In_rev : forall A (a:A)(l:list A), In a (rev l) <-> In a l. Proof. Admitted. Fixpoint mem {A}(eqb : A -> A ->bool)(a:A) (l:list A) : bool := match l with nil =>false | x::l' =>orb (eqb a x) (mem eqb a l') end. SearchAbout (nat->nat->bool). Compute mem NPeano.Nat.eqb 6 (3::5::6::8::nil). Lemma mem_correct : forall A (eqb : A -> A -> bool), (forall a b, eqb a b = true <-> a = b)-> forall x l, mem eqb x l = true <-> In x l. Proof. Admitted. (** More examples *) Lemma le_plus : forall n p, n <= p + n. Proof. Admitted. (*** Nothing is simple ***) Fixpoint plus' n m := match n with 0 => m | S p => plus' p (S m) end. Lemma plus'nS : forall n m, plus' n (S m) = S (plus' n m). Proof. intros n m;induction n. reflexivity. simpl. (* rewrite IHn. IHn is useless for the goal *) Abort. Lemma plus'nS : forall n m, plus' n (S m) = S (plus' n m). Proof. Admitted. Theorem plus'_my_plus : forall n p, plus' n p = n+p. Proof. Admitted.