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

(* One way to deal with this is to find a measure which we know is decreasing and
do induction on that. *)

Require Import Max.

(* Let's try the depth of the term. *)

Fixpoint depth (e : trm) :=
  match e with
  | trm_bvar n => 1
  | trm_fvar x => 1
  | trm_abs t => S (depth t)
  | trm_app t1 t2 => S (max (depth t1) (depth t2))
  end.

(* Note that we chose the depth of a leaf to be one rather than 0, this allows us to
prove that the depth of a trm is always greater than one. *)

Lemma depth_gt_0 : forall e, depth e > 0.
Proof.
  (* Easy proof, _all_ recursive steps are by simple induction. *)
  induction e; simpl; auto with arith.
Qed.

(* We state a simple equality lemma. *)
Lemma depth_open_rec' : forall k (z : var) e,
  depth e = depth ({k ~> (trm_fvar z)} e).
Proof.
  intros.
  (* We need to generalize over k *)
  gen k.
  induction e; simpl; intros; auto.
  (* the bvar case is simple, since opening will yield a bvar or a fvar, both with depth 1 *)
  destruct (k === n); auto.
Qed.

(* This lemma can be used to prove another lemma that we will find useful later. *)
Lemma depth_open_rec : forall n k (z : var) e,
  depth e <= n ->
  depth ({k ~> (trm_fvar z)} e) <= n.
Proof.
  intros.
  rewrite <- depth_open_rec'. auto.
Qed.

Lemma depth_open : forall n e (z : var),
  depth e <= n ->
  depth (open e (trm_fvar z)) <= n.
Proof.
  intros; unfold open; auto using depth_open_rec.
Qed.

(* With these lemmas, we are ready to prove our new induction principle.
    Observe that the induction principle now requires some natural number as
    its first argument. *)
Lemma trm_ind_core' : forall (n : nat) (P: trm -> Prop)
  (Hbvar : forall n, P (trm_bvar n))
  (Hfvar : forall x : var, P (trm_fvar x))
  (Habs : forall t1, (forall x, x \notin fv t1 -> P (t1 ^ x)) -> P (trm_abs t1))
  (Happ : forall t1, P t1 -> forall t2, P t2 -> P (trm_app t1 t2)),
  forall e : trm, depth e <= n -> P e.
Proof.
  intros.
  (* We generalize the variables not associated with P and not the hypotheses *)
  generalize dependent H.
  generalize dependent e.
  generalize dependent n.
  induction n.
  (* The first case is the case for 0. We can prove a contradiction. *)
  intros.
  (* First, we assert the fact that depth e > 0 in order to prove a contradiction. *)
  assert (depth e > 0) by auto using depth_gt_0.
  (* We establish the contradiction using omega. *)
  assert False by omega. tauto.
  (* The second case is the induction step. *)
  intros e.
  (* We need only destruct e, since our recursion is on n, not on e. *)
  destruct e.
  (* The first and second cases are solved immediately, as with our previous attempt. *)
  trivial.
  trivial.
  (* The abstraction case requires a little work. *)
  intros Depth.
  apply Habs.
  intros.
  (* Note that the goal is now about e ^ x rather than just e. 
      We apply the induction hypothesis. *)
  apply IHn.
  (* We rewrite the goal into a statement about depth e, rather than depth (e ^ x) *)
  unfold open. rewrite <- depth_open_rec'.
  auto with arith.
  (* The application case is similar, but requires reasoning about the max function. *)
  intros Depth.
  simpl in *.
  (* It's obvious here why we use the hypothesis (depth e <= n).
      In general one of depth e1 or depth e2 is not equal to n, but it is less than n.
      Here we place in the context the properties about depth e1 and depth e2 that
      we need. *)
  assert (max (depth e1) (depth e2) <= n) by auto with arith.
  assert (depth e1 <= max (depth e1) (depth e2)) by auto with arith.
  assert (depth e2 <= max (depth e1) (depth e2)) by auto with arith.
  assert (depth e1 <= n /\ depth e2 <= n) by omega.
  (* Once the facts about depth that we need are in the proof context the rest is easy. *)
  intuition auto.
Qed.

(* Using the previous induction hypothesis we can build a second hypothesis that
    encapsulates the handling of depth. *)
Lemma trm_ind' : forall (P: trm -> Prop)
  (Hbvar : forall n, P (trm_bvar n))
  (Hfvar : forall x : var, P (trm_fvar x))
  (Habs : forall t1, (forall x, x \notin fv t1 -> P (t1 ^ x)) -> P (trm_abs t1))
  (Happ : forall t1, P t1 -> forall t2, P t2 -> P (trm_app t1 t2)),
  forall e : trm,  P e.
Proof.
  intros.
  apply (trm_ind_core' (depth e)); auto.
Qed.

(* Now we can proceed to prove our original goal. *)
Lemma term_dec : forall e, term e \/ ~ term e.
Proof.
  intros.
  induction e using trm_ind'.
  (* a bvar is never a term *)
  right. red. intros. inversion H.
  (* a fvar is always a term. *)
  left. auto.
  (* abstraction case, find two possibiliites *)
  pick_fresh x.
  destruct (H x Fr).
  (* First case, e ^ x is a term, so trm_abs e is a term. *)
  left. apply_fresh term_abs as x0.
  (* Here there is a problem. We have that term (e ^ x), need to prove term (e ^ x0).
      This calls for a renaming lemma, i.e., we can use term (e ^ x) as a witness that
      term (e ^ x0) if certain conditions hold. *)
  Check term_rename.
  (* Note here that the side conditions are not necessary to the truth of this lemma...
      but they are necessary for proving the lemma using subst_intro. *)
  eauto using term_rename.
  (* Second case, e ^ x is not a term, so we must prove that trm_abs e is not a term. *)
  right. red. intros. auto.
  (* The recursive case is straightforward, as before. *)
  destruct IHe1.
  destruct IHe2.
  left. auto.
  right. red. intros. inversion H1. auto.
  right. red. intros. inversion H0. auto.
Qed.