Require Import Metatheory.
Require Import STLC_Core_Definitions.
Require Import STLC_Core_Infrastructure.

Goal progress.
unfold progress.
(* writing fixpoint *)
refine (fix F (t : trm) (T : typ) (Typ : empty |= t ~: T) {struct Typ} :=
  match Typ in empty |= t ~: T return value t \/ exists t', t --> t' with
  | typing_var E x T Ok Binds => _
  | typing_abs L E U T t1 f => _
  | typing_app U T E t1 t2 Typ1 Typ2 => _
  end).
(* Unfortunately, by writing the fixpoint in this way we've lost the fact that
(trm_fvar x) is typed in the empty environment. So, we have a proof that empty |= t ~: T 
which might be true, and we have a proof binds x T0 E, which might also be true, 
since we do not know that E is empty. This makes sense when we note that there is 
no reference to the environment in the return type of our fixpoint and that the variables 
in each match statement are just pattern matching variables. We'll try this again. *)
Admitted.



Goal progress.
unfold progress.
(* Solution, undo previous step and add an additional fact. *)
(* First perform introductions to keep hypotheses in order. *)
intros t T Typ.
(* We use the gen_eq tactic to bind empty to a new variable, E and generalize 
by replacing any occurence of empty in a term with E.*)
gen_eq (@empty typ) as E.
(* We re-introduce our variables using the gen tactic.*)
gen Typ.
gen E.
gen T.
gen t.
(* in writing our fixpoint we must now take into account our new variable E and we
must also generalize in much the same way as the gen_eq tactic. We even have a
new hypothesis, E = empty, which we put in the return type of our fixpoint. *)
refine (fix F (t : trm) (T : typ) (E : env) (Typ : E |= t ~: T) {struct Typ} :=
  match Typ in E |= t ~: T return E = empty -> value t \/ exists t', t --> t' with
  | typing_var E x T Ok Binds => _
  | typing_abs L E U T t1 f => _
  | typing_app U T E t1 t2 Typ1 Typ2 => _
  end).
intros.
(* We use subst to substitute equalities. *)
subst.
(* Here we use the power of discriminate to also compute. 
Remember that binds is really a shorthand for a statement about equality. *)
Print binds.
(* We know that if we evaluate binds in Binds we'll get a statement of the form
None = Some x. We can discriminate these two unequal values to get a contradiction
and eliminate the goal, thusly. *)
discriminate Binds.
(* Actually, the discriminate tactic without any arguments will inspect every hypothesis to
see if it is a discriminable equality. So we could have just typed "discriminate." and the goal
would have been solved just as well. *)
(* That was nice, but we can do the same thing without explicitly writing the fixpoint. 
We do that next. *)
Admitted.


Goal progress.
unfold progress.
intros t T Typ.
(* We generate the equality statement as before. *)
gen_eq (@empty typ) as E.
(* Here we use the induction tactic rather than writing the fixpoint, *)
induction Typ.
(* We get rid of our first subgoal as before. *)
intros. subst. discriminate.
(* Now we just need to prove that an abstraction is a value. *) 
intros Eq.
(* We select the left hand side of the goal. *)
apply or_introl.
(* We now must prove that the abstraction is a value. *)
apply value_abs.
(* We apply term_abs using the set L, because L occurs in the statements of H
and H0. *)
apply (@term_abs L).
(* We introduce the two hypotheses in the goal and we see that we now have a 
variable, x, and a proof that it is not in L. *)
introv NotIn.
(* We can discover that t1 ^ x is well typed in some environment by applying H to x
and the proof that x is notin L. *)
(* typing_regular is a lemma in STLC_Core_Infrastructure. *)
Check typing_regular.
(* It does just what we need, i.e., it proves that any well-typed term is locally closed.
However, it is kind of inconvenient, because its result type is a conjunction. That
means that we cannot apply it directly but must massage either it or the goal to get
things to work correctly. In this example we massage the goal. We choose a new goal
ok (E & x ~ U ) /\ term (t1 ^ x) from which the old goal is readily proved. Now we state
our intention to prove the new goal using the cut tactic. *)
cut (ok (E & x ~ U ) /\ term (t1 ^ x)).
(* The first subgoal, that our new goal proves the old goal, is very easy. *)
tauto.
(* And the second subgoal can be proved by using typing_regular and H. *)
apply (@typing_regular _ _ _ (H x NotIn)).
(* Now we work on the final case. *)
(* We know that an application can always be reduced, so we prove the rhs. *)
intros Eq.
(* We select the right hand side. *)
apply or_intror.
(* We break apart the two induction hypotheses. These are the same as the results we
would get if we applied our recursive function. *)
(* Note that we use an intro pattern to name the results of our operation. *)
(* Also, we can do the destruction even without dealing with left hand side of the implication *)
(* It just gets presented to us as a subgoal. *)
destruct IHTyp1 as [Val1 | [ t1' Red1]].
tauto.
destruct IHTyp2 as [Val2 | [t2' Red2] ].
tauto.
(* Here we're dealing with the case where the right and left hand side are both values. *)
(* We inspect more closely the derivation that the left hand side is an arrow type. *)
inversion Typ1; subst;
(* We throw away any non abstraction subgoals. *)
inversion Val1; subst.
(* We supply the term produced by the reduction. *)
exists (t0 ^^ t2).
(* We prove that it is the result of the reduction. *) 
apply red_beta; auto.
(* The last two are straightforward. *)
exists (trm_app t1 t2'); auto.
exists (trm_app t1' t2); auto.
Qed.