Homework Assignment 5 Interactive Computer Theorem Proving CS2949, Fall 2006 UC Berkeley 
Submit your solution file for this assignment as an attachment
by email with
the subject "ICTP HW5" by the start of class on October 5.
You should write your solutions entirely on your own, which includes not
consulting any solutions to these problems that may be posted on the web.
Template source file 
Require
Import
List Omega.
Tacticals warmup 
Forward reasoning 
Using the command, write a tactic forward that takes two
arguments: a new hypothesis name H and a proof term that has type
A1 > ... > An > B ; that is, an implication with n assumptions Ai and
conclusion B .
Your tactic should convert the current goal into one subgoal to prove each
Ai , along with an additional subgoal where B has been added as an
assumption with name H .
Hint: Remember that named definitions can be recursive!

When your tactic is done, you should be able to prove the theorem below by
uncommenting the proof script, which will use forward .

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.
Admitted.
End
forward.
Automatic transitivereflexivesymmetric closure 
Write a tactic trs_closure that takes no arguments and augments the set
of assumptions for the current goal to include the
transitivereflexivesymmetric closure of the initial assumptions.
That is:
To make things easier, your tactic only needs to deal with equalities between nat s, and it doesn't need to understand any propositional or firstorder
structure. You may find it helpful to use the tactics reflexivity (0
arguments), symmetry (0 arguments), and transitivity (1 argument).

You'll probably find this tactic useful. Call it like hasType e t to
ensure that expression e has type t before proceeding. (It fails
otherwise, which should mesh well with the backtracking in patternmatching.)

Ltac
hasType e t :=
match type of e with
 t => idtac
end.
And here's another useful one. You don't want your tactic to run forever,
so sometimes you'll want to check that you don't already have an assumption of
a given form. Call notAlreadyThere e to fail if there is already an
assumption stating e , or proceed normally otherwise.

Ltac
notAlreadyThere e :=
match goal with
 [ H : e  _ ] => fail 1
 _ => idtac
end.
After your tactic is done, you should be able to uncomment the proof script below and prove the theorem. 
Theorem
a : forall (x y z : nat), x = y > z = x >
x = x /\ y = y /\ z = z /\
x = y /\ y = x /\
x = z /\ z = x /\
y = z /\ z = y.
Admitted.
Bounded instantiation 
In this , we define an inductive predicate expressing that a
property holds of some natural number at least as high as some bound.
This predicate is tricky to do eliminationstyle reasoning on because we
would naively consider an infinite number of cases for why it holds, but
we can use tacticals to program heuristics that work well for some cases.

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.
Write a tactic bounded_somebody taking one argument n , which should be
interpreted as a search tree depth. Your tactic should try all depthn
possibilities of successive inversions on somebody assumptions, clearing
each assumption after it is inverted. At each node of the search tree, it
should try using eauto to solve the goal automatically. Your tactic
should fail when it isn't able to solve the goal completely with the given
depth.

Here's a test case that should work with your tactic. 
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.
Admitted.
End
somebody.
Programming languages 
This part of the assignment is about proving properties of small programming languages. In the first piece, you'll deal with the simplytyped lambda calculus. Since this assignment is designed to go along with the lecture on automation, the twist comes in the second piece, where we extend the language from the first part and see how few changes you need to make to your proof scripts from the first part to port them to the new language. 
Simplytyped lambda calculus 
The simplytyped lambda calculus is a standard toy programming language commonly found in programming language semantics classes like CS263 at Berkeley. It deserves the "simple" in its name, so don't worry if you aren't familiar with it or you've forgotten what you've learned; the Wikipedia page has a quick definition. 
Module
STLC.
The language of types; the base type (natural numbers) plus the function type constructor "arrow" 
Inductive
type : Set :=
 Nat : type
 Arrow : type > type > type.
The language of terms (or programs); variables, natural number constants,
and function application and abstraction. The constants are the one
addition from the Wikipedia presentation.
To make it easier to deal with variable binding, I've used a standard trick called nameless representation, or Debruijn indices. Instead of a variable reference being given as a name, it's given as a natural number that expresses the address of the place where that variable was bound. In other words, a variable occurrence with index n says that this variable was bound by the nth lambda encountered working outwards in lexical scoping order. For instance, with the backslash character used to denote a lambda binding, this lambda term: 
\x. \y. x
is written as: 
\_. \_. #1
The 1 points to the binder 2 steps outward. (0 would point to the closest enclosing binder.) This example also shows how lambda expressions no longer need to provide variable names. 
Inductive
term : Set :=
 Var : nat > term
 Const : nat > term
 App : term > term > term
 Lam : type > term > term.
Since we're working with a nameless encoding, a context, which maps the free variables of a term to types, need only be a list of types. The variable each type matches up with is determined by its position in the list. 
Definition
context := list type.
A standard relation to express looking up a particular Debruijn index in a context. 
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.
What it means for a term to have a type in a particular context assigning types to its free variables 
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).
Wellformedness 
Say that a term is "wellformed up to bound n" iff all of its free
variable occurrences refer only to the first n free variables at the
outermost scope.
For example, this term is wellformed up to bound 1: 
#0 (\_. #1)
Both variable occurrences refer to the same single toplevel free variable.
This term is not wellformed up to bound 1: 
(\_. #2)
Here's an inductive definition of wellformedness: 
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).
Prove that any term that has a type is wellformed.
There's a messy manual way to do it, but the point of this assignment is to
use lots of automation!
My solution proves this theorem without using any tactics but eauto ,
induction , omega , and simpl .
You'll probably want to use auxiliary definitions/lemmas, along with the
commands.

Theorem
hasType_wellFormed : forall G e t,
hasType G e t
> wellFormed (length G) e.
Admitted.
Uniqueness of typing 
Prove that a term can have at most one type.
You should complete this proof without using any proof scripts that refer to
automaticallygenerated hypothesis names; and you also shouldn't use the
named form of intros or any other way of "cheating." Instead, take
advantage of automation in a way that makes names of hypotheses irrelevant.
My solution uses no tactics but eauto and induction in the bodies of
s and s.
Though you should feel free to try alternate approaches within the spirit
of this problem, I'll include for reference the list of tactics that I used:
auto , clear , eauto , generalize , induction , injection , intros ,
inversion , and subst .
That's just a list of the atomic tactics; I also used a majority of the
constructs from the Ltac tactic definition language, along with some
s.

Theorem
uniqueness : forall G e t1,
hasType G e t1
> forall t2, hasType G e t2
> t1 = t2.
Admitted.
End
STLC.
Extending the language 
Now we add product types to our language and see how easily your proof scripts from the last part adapt. The type "S x T" denotes pairs whose first components have type S and second components have type T. Pairs are formed with an operation "Pair," and their first and second components are extracted with operations "Fst" and "Snd," respectively. 
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.
Now prove the same two theorems again. You should be able to reuse your
proof scripts from the last part almost unchanged.
I adapted my solution by adding 4 lines to it, corresponding to 4 new constructors of the inductive types defining the language. I didn't need to delete or modify any old lines. 
Wellformedness 
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).
Theorem
hasType_wellFormed : forall G e t,
hasType G e t
> wellFormed (length G) e.
Admitted.
Uniqueness of typing 
Theorem
uniqueness : forall G e t1,
hasType G e t1
> forall t2, hasType G e t2
> t1 = t2.
Admitted.
In case you haven't come to appreciate automation enough by this point,
take a look at the output of this command and see what you saved
writing by hand. :)

Print
uniqueness.
End
PLC.