(** Homework Assignment 5#
# ##Interactive Computer Theorem Proving#
# CS294-9, Fall 2006#
# UC Berkeley *) Require Import List Omega. (** * Tacticals warm-up *) Ltac forward H e := match type of e with | ?A -> ?B => let H' := fresh "H'" in (assert (H' : A); [idtac | forward H (e H'); clear H']) | ?B => assert (H : B); [exact e | idtac] end. Section forward. Variables P Q R S : Prop. Hypothesis Pt : P. Hypothesis Qt : Q. Hypothesis Rt : R. Hypothesis impl : P -> Q -> R -> S. Theorem mp3 : S. forward Hs impl; [exact Pt | exact Qt | exact Rt | exact Hs]. Qed. End forward. Ltac hasType e t := match type of e with | t => idtac end. Ltac notAlreadyThere e := match goal with | [ H : e |- _ ] => fail 1 | _ => idtac end. Ltac trs_closure := repeat match goal with | [ H : context[?E] |- _ ] => hasType E nat; notAlreadyThere (E = E); assert (E = E); [reflexivity | idtac] | [ H : ?X = ?Y |- _ ] => notAlreadyThere (Y = X); assert (Y = X); [symmetry; assumption | idtac] | [ H1 : ?X = ?Y, H2 : ?Y = ?Z |- _ ] => notAlreadyThere (X = Z); assert (X = Z); [transitivity Y; assumption | idtac] end. Theorem a : forall (x y z : nat), x = y -> z = y -> x = z. intros; trs_closure; assumption. Qed. (** ** Bounded instantiation *) Section somebody. Variable P : nat -> Prop. Inductive somebody : nat -> Prop := | Me : forall n, P n -> somebody n | Him : forall n, somebody (S n) -> somebody n. Ltac bounded_somebody n := match n with | O => idtac | S ?n' => match goal with | [ H : somebody _ |- _ ] => inversion H; clear H; subst; eauto; bounded_somebody n'; fail end end. Variable Q : Prop. Hypothesis P0 : P 0 -> Q. Hypothesis P1 : P 1 -> Q. Hypothesis P2 : P 2 -> Q. Hypothesis Pge3 : forall n, n >= 3 -> somebody n -> Q. Theorem testIt : somebody 0 -> Q. intros. bounded_somebody 3. Qed. End somebody. (** * Simply-typed lambda calculus *) Module STLC. Inductive type : Set := | Nat : type | Arrow : type -> type -> type. Inductive term : Set := | Var : nat -> term | Const : nat -> term | App : term -> term -> term | Lam : type -> term -> term. Definition context := list type. Inductive lookup : context -> nat -> type -> Prop := | Lookup_O : forall t G, lookup (t :: G) O t | Lookup_S : forall t' G n t, lookup G n t -> lookup (t' :: G) (S n) t. Inductive hasType : list type -> term -> type -> Prop := | HT_Var : forall (G : context) (x : nat) (t : type), lookup G x t -> hasType G (Var x) t | HT_Const : forall (G : context) (n : nat), hasType G (Const n) Nat | HT_App : forall (G : context) (e1 e2 : term) (dom ran : type), hasType G e1 (Arrow dom ran) -> hasType G e2 dom -> hasType G (App e1 e2) ran | HT_Lam : forall (G : context) (dom : type) (e : term) (ran : type), hasType (dom :: G) e ran -> hasType G (Lam dom e) (Arrow dom ran). (** ** Well-formedness *) Inductive wellFormed : nat -> term -> Prop := | WF_Var : forall (bound : nat) (x : nat), x < bound -> wellFormed bound (Var x) | WF_Const : forall (bound : nat) (n : nat), wellFormed bound (Const n) | WF_App : forall (bound : nat) (e1 e2 : term), wellFormed bound e1 -> wellFormed bound e2 -> wellFormed bound (App e1 e2) | WF_Lam : forall (bound : nat) (t : type) (e : term), wellFormed (S bound) e -> wellFormed bound (Lam t e). Hint Constructors wellFormed. Lemma lookup_wellFormed : forall G x t, lookup G x t -> x < length G. induction 1; simpl; omega. Qed. Hint Resolve lookup_wellFormed. Theorem hasType_wellFormed : forall G e t, hasType G e t -> wellFormed (length G) e. induction 1; eauto. Qed. (** ** Uniqueness of typing *) Ltac ics H := inversion H; clear H; subst. Ltac lookup_inversion := match goal with | [ H : lookup _ O _ |- _ ] => ics H | [ H : lookup _ (S _) _ |- _ ] => ics H end. Hint Extern 1 (_ = _) => lookup_inversion. Lemma uniqueness_lookup : forall G x t1, lookup G x t1 -> forall t2, lookup G x t2 -> t1 = t2. induction 1; auto. Qed. Hint Resolve uniqueness_lookup. Ltac hasType_inversion := match goal with | [ H : hasType _ (Var _) _ |- _ ] => ics H | [ H : hasType _ (Const _) _ |- _ ] => ics H | [ H : hasType _ (App _ _) _ |- _ ] => ics H | [ H : hasType _ (Lam _ _) _ |- _ ] => ics H end. Hint Extern 1 (_ = _) => hasType_inversion. Ltac icis H := injection H; clear H; intros; subst. Ltac type_injection := match goal with | [ H : Arrow _ _ = Arrow _ _ |- _ ] => icis H end. Hint Extern 1 (_ = _) => type_injection. Ltac useIh := match goal with | [ H1 : forall t : type, hasType ?G ?E t -> _, H2 : hasType ?G ?E ?T |- _ ] => generalize (H1 _ H2); clear H1; intros; subst; auto; fail end. Hint Extern 1 (_ = _) => useIh. Theorem uniqueness : forall G e t1, hasType G e t1 -> forall t2, hasType G e t2 -> t1 = t2. induction 1; eauto. Qed. End STLC. (** * Extending the language *) Module PLC. Inductive type : Set := | Nat : type | Arrow : type -> type -> type | Prod : type -> type -> type. Inductive term : Set := | Var : nat -> term | Const : nat -> term | App : term -> term -> term | Lam : type -> term -> term | Pair : term -> term -> term | Fst : term -> term | Snd : term -> term. Definition context := list type. Inductive lookup : context -> nat -> type -> Prop := | Lookup_O : forall t G, lookup (t :: G) O t | Lookup_S : forall t' G n t, lookup G n t -> lookup (t' :: G) (S n) t. Inductive hasType : list type -> term -> type -> Prop := | HT_Var : forall (G : context) (x : nat) (t : type), lookup G x t -> hasType G (Var x) t | HT_Const : forall (G : context) (n : nat), hasType G (Const n) Nat | HT_App : forall (G : context) (e1 e2 : term) (dom ran : type), hasType G e1 (Arrow dom ran) -> hasType G e2 dom -> hasType G (App e1 e2) ran | HT_Lam : forall (G : context) (dom : type) (e : term) (ran : type), hasType (dom :: G) e ran -> hasType G (Lam dom e) (Arrow dom ran) | HT_Pair : forall (G : context) (e1 e2 : term) (t1 t2 : type), hasType G e1 t1 -> hasType G e2 t2 -> hasType G (Pair e1 e2) (Prod t1 t2) | HT_Fst : forall (G : context) (e : term) (t1 t2 : type), hasType G e (Prod t1 t2) -> hasType G (Fst e) t1 | HT_Snd : forall (G : context) (e : term) (t1 t2 : type), hasType G e (Prod t1 t2) -> hasType G (Snd e) t2. (** ** Well-formedness *) Inductive wellFormed : nat -> term -> Prop := | WF_Var : forall (bound : nat) (x : nat), x < bound -> wellFormed bound (Var x) | WF_Const : forall (bound : nat) (n : nat), wellFormed bound (Const n) | WF_App : forall (bound : nat) (e1 e2 : term), wellFormed bound e1 -> wellFormed bound e2 -> wellFormed bound (App e1 e2) | WF_Lam : forall (bound : nat) (t : type) (e : term), wellFormed (S bound) e -> wellFormed bound (Lam t e) | WF_Pair : forall (bound : nat) (e1 e2 : term), wellFormed bound e1 -> wellFormed bound e2 -> wellFormed bound (Pair e1 e2) | WF_Fst : forall (bound : nat) (e : term), wellFormed bound e -> wellFormed bound (Fst e) | WF_Snd : forall (bound : nat) (e : term), wellFormed bound e -> wellFormed bound (Snd e). Hint Constructors wellFormed. Lemma lookup_wellFormed : forall G x t, lookup G x t -> x < length G. induction 1; simpl; omega. Qed. Hint Resolve lookup_wellFormed. Theorem hasType_wellFormed : forall G e t, hasType G e t -> wellFormed (length G) e. induction 1; eauto. Qed. (** ** Uniqueness of typing *) Ltac ics H := inversion H; clear H; subst. Ltac lookup_inversion := match goal with | [ H : lookup _ O _ |- _ ] => ics H | [ H : lookup _ (S _) _ |- _ ] => ics H end. Hint Extern 1 (_ = _) => lookup_inversion. Lemma uniqueness_lookup : forall G x t1, lookup G x t1 -> forall t2, lookup G x t2 -> t1 = t2. induction 1; auto. Qed. Hint Resolve uniqueness_lookup. Ltac hasType_inversion := match goal with | [ H : hasType _ (Var _) _ |- _ ] => ics H | [ H : hasType _ (Const _) _ |- _ ] => ics H | [ H : hasType _ (App _ _) _ |- _ ] => ics H | [ H : hasType _ (Lam _ _) _ |- _ ] => ics H | [ H : hasType _ (Pair _ _) _ |- _ ] => ics H | [ H : hasType _ (Fst _) _ |- _ ] => ics H | [ H : hasType _ (Snd _) _ |- _ ] => ics H end. Hint Extern 1 (_ = _) => hasType_inversion. Ltac icis H := injection H; clear H; intros; subst. Ltac type_injection := match goal with | [ H : Arrow _ _ = Arrow _ _ |- _ ] => icis H | [ H : Prod _ _ = Prod _ _ |- _ ] => icis H end. Hint Extern 1 (_ = _) => type_injection. Ltac useIh := match goal with | [ H1 : forall t : type, hasType ?G ?E t -> _, H2 : hasType ?G ?E ?T |- _ ] => generalize (H1 _ H2); clear H1; intros; subst; auto; fail end. Hint Extern 1 (_ = _) => useIh. Theorem uniqueness : forall G e t1, hasType G e t1 -> forall t2, hasType G e t2 -> t1 = t2. induction 1; eauto. Qed. End PLC.