(* * Copyright (c) 2009, Andrew Appel, Robert Dockins and Aquinas Hobor. * *) (** This libaray reexports portions of the Coq standard libraries used throughtout the proof. It also defines some convenience tactics. *) Require Export ClassicalReasoningAboutComputation. Require Export List. Require Export Bool. Require Export Omega. Require Export Relations. Definition compose (A B C:Type) (g:B -> C) (f:A -> B) := fun x => g (f x). Implicit Arguments compose [A B C]. Infix "oo" := compose (at level 54, right associativity). Lemma compose_assoc (A B C D:Type) (h:C->D) (g:B->C) (f:A->B) : (h oo g) oo f = h oo g oo f. Proof. intros; apply extensionality; intro x; unfold compose; auto. Qed. Definition id (A:Type) := fun x:A => x. Lemma id_unit1 : forall A B (f:A->B), f oo id A = f. Proof. intros; apply extensionality; intro x; auto. Qed. Lemma id_unit2 : forall A B (f:A->B), id B oo f = f. Proof. intros; apply extensionality; intro x; auto. Qed. (** Perform inversion on a hypothesis, removing it from the context, and perform substitutions *) Tactic Notation "inv" hyp(H) := inversion H; clear H; subst. (** Specialize a hypothesis with respect to specific terms or proofs. *) Tactic Notation "spec" hyp(H) := match type of H with ?a -> _ => let H1 := fresh in (assert (H1: a); [|generalize (H H1); clear H H1; intro H]) end. Tactic Notation "spec" hyp(H) constr(a) := (generalize (H a); clear H; intro H). Tactic Notation "spec" hyp(H) constr(a) constr(b) := (generalize (H a b); clear H; intro H). Tactic Notation "spec" hyp(H) constr(a) constr(b) constr(c) := (generalize (H a b c); clear H; intro H). Tactic Notation "spec" hyp(H) constr(a) constr(b) constr(c) constr(d) := (generalize (H a b c d); clear H; intro H). Tactic Notation "spec" hyp(H) constr(a) constr(b) constr(c) constr(d) constr(e) := (generalize (H a b c d e); clear H; intro H). (** Apply the extensionality axiom. *) Tactic Notation "extensionality" := (match goal with | |- ?f = ?g => apply (extensionality f g); intro end). Tactic Notation "extensionality" ident(x) := (match goal with | |- ?f = ?g => apply (extensionality f g); intro x end). Tactic Notation "extensionality" ident(x) ident(y) := (match goal with | |- ?f = ?g => apply (extensionality f g); intro x; apply (extensionality (f x) (g x)); intro y end). Tactic Notation "extensionality" ident(x) ident(y) ident(z):= (match goal with | |- ?f = ?g => apply (extensionality f g); intro x; apply (extensionality (f x) (g x)); intro y; apply (extensionality (f x y) (g x y)); intro z end).