Require Import Metatheory. Require Import STLC_Core_Definitions. (* Here we prove that \.0, the identity function, is a well-formed term. *) Goal term (trm_abs (trm_bvar 0)). Proof. (* The @ before the constructor allows us to specify all variables, including those that are implicit. L is implicit in term_abs, because its value can be inferred from the subsequent functional argument. *) apply (@term_abs {}). (* Note that we chose to specify the empty set here. x \notin {} is always true, so the type of our function might as well be forall x, term (trm_bvar 0 ^ x). *) (* Now we introduce the parameters of the function. *) intros. (* The change tactic allows us to substitute one term for another if the two terms are interconvertible. The Coq engine checks this and will not allow this tactic when the terms are not interconvertible. You can experiment with the change tactic with a statement like this, Coq will complain. change (trm_bvar 0 ^ x) with (trm_bvar 0) *) change (trm_bvar 0 ^ x) with (trm_fvar x). apply term_var. Qed. (* When we print the theorem we see that the constructor has a function as one of its arguments. *) Print Unnamed_thm. (* One can prove that any term is well formed using the empty set. So, at this point, we haven't made any use of the extra complexity caused by including this set L. *) (* Here's a proof that an application, (\.0)x is a well-formed term. *) Parameter x : var. Goal term(trm_app (trm_abs (trm_bvar 0)) (trm_fvar x)). Proof. apply (term_app). apply (@term_abs {}). intros. change (trm_bvar 0 ^ x0) with (trm_fvar x0). exact (term_var x0). exact (term_var x). Show Proof. Qed.