(** 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. Definition pred (n : nat) : nat := match n with | 0 => n | S p => p end. (** simplifications *) Lemma pred_S : forall n, pred (S n) = n. Proof. reflexivity. Qed. Lemma S_pred : forall n, S (pred n) = n. intro n. case n. simpl. Abort. Lemma S_pred : forall n, 0 <> n -> S (pred n) = n. Proof. intros n H. destruct n. destruct H;trivial. reflexivity. Qed. (** 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. intro n;destruct n. auto. simpl. intro H. rewrite H. auto. Qed. Lemma list_decompose : forall A (l:list A) , l = nil \/ exists a l', l = a::l'. Proof. intros A l;destruct l;[left | right]. trivial. exists a ; now exists l. Qed. (** recursive functions *) Fixpoint my_plus (n m : nat) : nat := match n with | 0 => m | S p => S (my_plus p m) end. Notation "n + p" := (my_plus n p) : nat_scope. Fixpoint my_mult (n m : nat) := match n with 0 => 0 | S p => m + my_mult p m end. 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. intro n; reflexivity. Qed. Lemma plus_Sm_n : forall m n, S m + n = S (m + n). Proof. intros n m;reflexivity. Qed. Lemma mult_1_m : forall n, 1 * n = n. Proof. intro n;try reflexivity. simpl . Abort (* Coming back soon *) . (** Proofs by cases *) Lemma plus_zero_l : forall n p, n + p = 0 -> n = 0. Proof. intros n p. case n. reflexivity. simpl. intros n0 H. discriminate. Qed. Lemma plus_zero : forall n p, n + p = 0 -> n = 0 /\ p = 0. Proof. intros n p H; generalize (plus_zero_l _ _ H). intro H0. subst n. simpl in H. subst p. split;reflexivity. Qed. Lemma plus_m_0 : forall m, m + 0 = m. Proof. intro m; destruct m;simpl. reflexivity. Restart. intro m; induction m; simpl. reflexivity. rewrite IHm. reflexivity. Qed. Lemma plus_m_Sn : forall m n, m + S n = S (m + n). Proof. intro m. induction m. reflexivity. intro n. simpl. rewrite IHm; trivial. Qed. Lemma plus_comm : forall n p, n + p = p + n. Proof. induction n; simpl;auto. intro p;rewrite (IHn p). SearchAbout (_ + S _). now rewrite <- plus_m_Sn. Qed. (** Now we can go back to mult_1 *) Lemma mult_1 : forall n, 1 * n = n. Proof. intros n;simpl. SearchAbout (_ + 0). now rewrite plus_m_0. Qed. (** Exercises *) Lemma plus_assoc : forall n p q, n + (p + q) = (n + p) + q. Admitted. Lemma mult_m_0 : forall n: nat, n * 0 = 0. Admitted. Lemma mult_com : forall n p, n * p = p * n. induction n;simpl;auto. (* embedded lemmas *) Lemma mult_m_Sn : forall m n, m * S n = m + m * n. Proof. induction m;simpl;auto. intro n. rewrite IHm. repeat rewrite (plus_assoc). now rewrite (plus_comm m n). Qed. intro p;rewrite mult_m_Sn. now rewrite IHn. Qed. (** induction on lists *) Open Scope list_scope. Fixpoint app {A:Type}(l l':list A): list A := match l with nil => l' | x::l1 => x::(app l1 l') end. Infix "++" := app (right associativity, at level 60) : list_scope. (* ++ in StdLib *) Fixpoint rev {A:Type}(l:list A) : list A := match l with nil => nil | x::l' => rev l' ++ (x::nil) end. Lemma app_assoc : forall {A:Type}(l1 l2 l3: list A), l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3. Proof. induction l1;simpl;auto. intros l2 l3; now rewrite IHl1. Qed. Lemma rev_rev {A} (l:list A) : rev (rev l) = l. induction l;simpl;auto. Lemma rev_of_app {A:Type} : forall l1 l2 : list A, rev (l1 ++ l2) = rev l2 ++ rev l1. induction l1;simpl. intro l2; generalize (rev l2). induction l;simpl;auto. now rewrite <- IHl. intros l2;rewrite IHl1. now rewrite app_assoc. Qed. rewrite rev_of_app. simpl. now rewrite IHl. Qed. (** 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. intros A l;unfold fast_rev. induction l; simpl;auto. Restart. intros A l; unfold fast_rev. replace (rev l) with (rev l ++ nil). generalize (@nil A). induction l. reflexivity. intro l0;simpl;rewrite IHl;simpl. repeat rewrite <- IHl. now rewrite <- app_assoc. generalize (rev l);intro l';induction l';simpl;auto. now rewrite IHl'. Qed. (** 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. induction l1;simpl. intro l2;tauto. intro l2;rewrite IHl1. tauto. Qed. Lemma In_rev : forall A (a:A)(l:list A), In a (rev l) <-> In a l. induction l;simpl. tauto. rewrite In_app. rewrite IHl. simpl. tauto. Qed. 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. intros A eqb Heqb x. induction l;simpl. split;[discriminate | contradiction]. case (eqb x a) (* important *). simpl. Undo 2. case_eq (eqb x a). intro H0;simpl. rewrite Heqb in H0. subst a. intuition. intro H0; simpl. rewrite IHl. rewrite <- Heqb. rewrite H0. split;auto. intro H;destruct H as [H1 | H2]. discriminate. assumption. Qed. (** More examples *) Lemma le_plus : forall n p, n <= p + n. Proof. induction n;simpl;auto. (** bad choice: addition is driven by its first argument (here p) *) Restart. intro n; induction p. simpl;auto. simpl. auto. Qed. (*** 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. (* let's us keep m as generic as possible *) intro n. induction n. reflexivity. simpl. intro m. rewrite IHn. reflexivity. Qed. Theorem plus'_my_plus : forall n p, plus' n p = n+p. induction n;simpl;auto. SearchAbout (plus' _ (S _)). intros; rewrite plus'nS. now rewrite IHn. Qed.