Library HW5

Homework Assignment 5
Interactive Computer Theorem Proving
CS294-9, Fall 2006
UC Berkeley

Submit your solution file for this assignment as an attachment by e-mail 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 warm-up

Forward reasoning

Using the Ltac 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 Ltac 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 transitive-reflexive-symmetric closure

Write a tactic trs_closure that takes no arguments and augments the set of assumptions for the current goal to include the transitive-reflexive-symmetric closure of the initial assumptions. That is:

All of the original assumptions should be kept.
For any term E appearing in the final assumptions, E = E should be present as an assumption.
For any final assumption X = Y, there should also be an assumption Y = X.
For any final assumptions X = Y and Y = Z, there should also be an assumption X = Z.

To make things easier, your tactic only needs to deal with equalities between nats, and it doesn't need to understand any propositional or first-order 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 back-tracking in pattern-matching.)


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 Section, 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 elimination-style 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 depth-n 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 simply-typed 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.

Simply-typed lambda calculus

The simply-typed 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).

Well-formedness

Say that a term is "well-formed 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 well-formed up to bound 1:


#0 (\_. #1)

Both variable occurrences refer to the same single top-level free variable.

This term is not well-formed up to bound 1:


(\_. #2)

Here's an inductive definition of 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).

Prove that any term that has a type is well-formed. 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 Hint 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 automatically-generated 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 Theorems and Lemmas. 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 Hints.


  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 re-use 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.

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).




  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 Print command and see what you saved writing by hand. :-)


  Print uniqueness.

End PLC.

Index

This page has been generated by coqdoc