(* 2004 - 04 - 21 *)
Require Import Metatheory.
Require Import STLC_Core_Definitions.

(* The following are some exercises using trm. *)

(* Here we build \.0, the identify function. *)
Check (trm_abs (trm_bvar 0)).

(* Something a bit harder, \.\.1. *)
Check (trm_abs (trm_abs (trm_bvar 1))).

(* And harder still (\.0) (\.\.1) *)
Check (trm_app (trm_abs (trm_bvar 0)) (trm_abs (trm_abs (trm_bvar 1)))).

(* We can also construct terms that are meaningful with a DeBruijn representation but
meaningless in a locally nameless representation. *)
Check (trm_abs (trm_bvar 1)).

(* To deal with this a unary predicate, term is defined. *)
Print term.
(* Note that term has no rule for bound variables, since no bound variable is a term. 
Any free variable is a term. A an application is a term if its subterms are terms.
For an abstraction things are trickier, since \.0 is a term, but 0 is not a term.
We say that an abstraction is a term if its subterm, opened with any variable x, is a term. *)
Print open.

(* open has a shorthand. t^x means the term t opened with the variable (trm_fvar x). *)
Parameter t : trm.
Parameter v : var.
Check (t ^ v).
(* Here we used Parameter to declare our variables without defining them. *)

(* We can evaluate open. *)
Eval compute in (trm_bvar 0 ^ v).
Eval compute in (trm_bvar 1 ^ v).

(* open is defined in terms of open_rec. *)
Print open_rec.
(* Note that open_rec allows recursively opening a trm with any other trm.
It is more general than open. It also has a special shorthand.
 {k ~> u} t means open t with u at k. As before, we can evaluate it. *)
Eval compute in ({ 1 ~> (trm_fvar v) } (trm_abs (trm_bvar 2))).

(* open_rec is also interesting because it uses the shorthand k === l, which is
an abbreviation for Peano_dec.eq_nat_dec k l. If we extract open_rec this will
be obvious. *)
Extraction open_rec.

(* There is a further shorthand for applying open_rec at 0. *)
Eval compute in ( (trm_abs (trm_bvar 1)) ^^ (trm_fvar v) ).

(* For some further exercises we construct proofs that certain trms are terms. *)
Goal term (trm_fvar v).
exact (term_var v).
Qed.

Goal term (trm_app (trm_fvar v) (trm_fvar v)).
apply term_app; exact (term_var v).
Show Proof.
(* Note that these proofs are just values, much like
the proofs of facts like 2 <= 4 which we worked on
earlier. *)
Qed.

(* When it comes to abtractions proofs of terminess are a little harder to build. *)