(** 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.