Require Import Metatheory. Require Import STLC_Core_Definitions. (* In the empty environment, the identity function can be typed. I choose the simplest typing, although really there are an infinite number. *) Goal empty |= trm_abs (trm_bvar 0) ~: typ_arrow (typ_var var_default) (typ_var var_default). (* Since we're typing an abstraction, only typing_abs will work. However, we do need to supply the implicit parameter, L. *) apply (@typing_abs {}). (* Now we msut supply the function that maps variables to proofs. *) (* First we introduce the arguments to the function. *) intros. (* Now we evaluate the open function. *) unfold open. unfold open_rec. (* We have to deal with two cases, the case when 0 = 0 and the case when 0 <> 0. The Penn group has written some tactics for dealing with that---we use them. *) case_nat. (* The only match here is typing_var. *) apply typing_var. (* We prove that our environment is ok using auto. *) info auto. (* The Penn implementation has a lot of nice stuff about binding, so we can use auto to prove our other subgoal. *) info auto. (* Now all we have is the ridiculous case where one of our hypotheses is 0<>0. tauto can eliminate this. *) tauto. Qed. (* It's interesting to type a slightly more complex abstraction. Here our choice of L must be something other than the empty set. *) Goal empty |= trm_abs (trm_abs (trm_bvar 1)) ~: typ_arrow (typ_var var_default) (typ_arrow (typ_var var_default) (typ_var var_default)). apply (@typing_abs {}). intros. unfold open. unfold open_rec. case_nat. intros. (* In typechecking the inner portion of the lambda, it is necessary to make sure that L contains all elements in the domain of the environment. *) apply (@typing_abs {{x}}). (* You'll see that you cannot find a type derivation for the whole program if at this point you choose L to be the emtpy set instead. *) unfold open. unfold open_rec. intros. apply typing_var. (* We prove that the environment is ok with auto. *) info auto. (* Note that H0, the hypothesesis that x0 is notin {{x}} was necessary to prove that the environment was ok. *) info auto. (* We eliminate the ridiculous goal using tauto. *) tauto. Qed. (* Here we prove that the identity function applied to the identity function reduces to the identity function. *) Goal (trm_app (trm_abs (trm_bvar 0)) (trm_abs (trm_bvar 0))) --> (trm_abs (trm_bvar 0)). (* First, we use the change tactic, so that our goal will match one of the reduction rules. *) change (trm_abs (trm_bvar 0)) at 3 with (trm_bvar 0 ^^ (trm_abs (trm_bvar 0))). (* Then we apply the proper constructor. *) apply red_beta. (* To prove that an abstraction is a term we must supply a value for L. *) apply (@term_abs {}). intros. unfold open. unfold open_rec. case_nat. apply (term_var). (* Eliminate the foolish case --- where 0 <> 0 *) tauto. (* Now it is just necessary to prove that the identity function is a value *) apply value_abs. (* Now just prove that the identity function is a term, something we've done before. *) apply (@term_abs {}). intros. unfold open. unfold open_rec. case_nat. apply (term_var). tauto. Qed.