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