(** * Module [extralibrary]: library functions, theorems, and tactics *) Require Import Arith. Require Import ZArith. Require Import List. (** ** Tactics *) Ltac decEq := match goal with | [ |- (_, _) = (_, _) ] => apply injective_projections; unfold fst,snd; try reflexivity | [ |- (@Some ?T _ = @Some ?T _) ] => apply (f_equal (@Some T)); try reflexivity | [ |- (@cons ?T _ _ = @cons ?T _ _) ] => apply (f_equal2 (@cons T)); try reflexivity | [ |- (?X _ _ _ _ _ = ?X _ _ _ _ _) ] => apply (f_equal5 X); try reflexivity | [ |- (?X _ _ _ _ = ?X _ _ _ _) ] => apply (f_equal4 X); try reflexivity | [ |- (?X _ _ _ = ?X _ _ _) ] => apply (f_equal3 X); try reflexivity | [ |- (?X _ _ = ?X _ _) ] => apply (f_equal2 X); try reflexivity | [ |- (?X _ = ?X _) ] => apply (f_equal X); try reflexivity | [ |- (?X ?A <> ?X ?B) ] => cut (A <> B); [intro; congruence | try discriminate] end. Ltac omegaContradiction := cut False; [contradiction|omega]. Ltac caseEq name := generalize (refl_equal name); pattern name at -1 in |- *; case name. (** ** Arithmetic *) Inductive comparison_nat (x y: nat) : Set := | Nat_less: x < y -> comparison_nat x y | Nat_equal: x = y -> comparison_nat x y | Nat_greater: x > y -> comparison_nat x y. Lemma compare_nat: forall x y, comparison_nat x y. Proof. intros. case (lt_eq_lt_dec x y); intro. destruct s. apply Nat_less; auto. apply Nat_equal; auto. apply Nat_greater; auto. Defined. (** ** Lists *) Lemma notin_cons_l: forall (A: Set) (u: A) (x: A) (l: list A), ~In u (x :: l) -> u <> x. Proof. simpl; intros. apply sym_not_equal. tauto. Qed. Lemma notin_cons_r: forall (A: Set) (u: A) (x: A) (l: list A), ~In u (x :: l) -> ~In u l. Proof. simpl; intros. tauto. Qed. Lemma notin_app_l: forall (A: Set) (u: A) (l1 l2: list A), ~In u (l1 ++ l2) -> ~In u l1. Proof. intros. generalize (in_or_app l1 l2 u). tauto. Qed. Lemma notin_app_r: forall (A: Set) (u: A) (l1 l2: list A), ~In u (l1 ++ l2) -> ~In u l2. Proof. intros. generalize (in_or_app l1 l2 u). tauto. Qed. Hint Resolve sym_not_equal notin_cons_l notin_cons_r notin_app_l notin_app_r. Lemma in_app_equiv: forall (A: Set) (x y: A) (l1 l2 l3 l4: list A), (In x l1 <-> In y l3) -> (In x l2 <-> In y l4) -> (In x (l1 ++ l2) <-> In y (l3 ++ l4)). Proof. intros. generalize (in_or_app l1 l2 x). generalize (in_or_app l3 l4 y). generalize (in_app_or l1 l2 x). generalize (in_app_or l3 l4 y). tauto. Qed. Hint Resolve in_app_equiv. Lemma in_app_l: forall (A: Set) (x: A) (l1 l2: list A), In x l1 -> In x (l1 ++ l2). Proof. intros. apply in_or_app. tauto. Qed. Lemma in_app_r: forall (A: Set) (x: A) (l1 l2: list A), In x l2 -> In x (l1 ++ l2). Proof. intros. apply in_or_app. tauto. Qed. Hint Resolve in_app_l in_app_r. Lemma in_cons_other: forall (A: Set) (x y: A) (l: list A), In x (y :: l) -> x <> y -> In x l. Proof. intros. elim H; intros. congruence. auto. Qed. Hint Resolve in_cons_other. Lemma map_append: forall (A B: Set) (f: A -> B) (l1 l2: list A), map f (l1 ++ l2) = (map f l1) ++ (map f l2). Proof. induction l1; simpl; intros. auto. decEq; auto. Qed. Lemma incl_cons2: forall (A: Set) (x: A) (l1 l2: list A), incl l1 l2 -> incl (x::l1) (x::l2). Proof. intros; red; simpl; intros. generalize (H a). tauto. Qed. Hint Resolve in_app_or in_or_app incl_refl incl_tl incl_cons incl_cons2 incl_app. (** ** Peano induction. *) (** This is a variant of the induction principle over natural numbers. It will be used later to do induction over the size of a type. *) Lemma Peano_induction: forall (P: nat -> Prop), (forall x, (forall y, y < x -> P y) -> P x) -> forall x, P x. Proof. intros P H. assert (forall x, forall y, y < x -> P y). induction x; intros. omegaContradiction. apply H. intros. apply IHx. omega. intro. apply H0 with (S x). omega. Qed.