(** Homework Assignment 5#<br>#
#<a href="http://www.cs.berkeley.edu/~adamc/itp/">#Interactive Computer Theorem
Proving#</a><br>#
CS294-9, Fall 2006#<br>#
UC Berkeley *)

(** Submit your solution file for this assignment as an attachment
  #<a href="mailto:adamc@cs.berkeley.edu?subject=ICTP HW5">#by e-mail#</a># 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.

  #<a href="HW5.v">#Template source file#</a>#
  *)

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.
    (*forward Hs impl;
    [exact Pt
      | exact Qt
      | exact Rt
      | exact Hs].
  Qed.*)
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
  [nat]s, 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.
   (*intros. tr_closure; repeat split; assumption.
     Qed.*)
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.
    (*intros; bounded_somebody 3.
  Qed.*)
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; 
  #<a href="http://en.wikipedia.org/wiki/Simply_typed_lambda_calculus">#the
  Wikipedia page#</a># 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 #<i>#nameless#</i># representation, or #<i>#Debruijn indices#</i>#.
    Instead of a variable reference being given as a name, it's given as a
    natural number that expresses the #<i>#address#</i># 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 #<i>#context#</i>#, 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
    [Theorem]s and [Lemma]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
    [Hint]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 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.