Module Chap8.
  (* 8.1 *)
  Inductive term : Type :=
  | ttrue
  | tfalse
  | iif (t1 t2 t3 : term)
  | O
  | succ (t : term)
  | pred (t : term)
  | iszero (t : term).

  Scheme Equality for term.

  Inductive is_numeric_val : term -> Prop :=
  | nv_O : is_numeric_val O
  | nv_succ : forall t, is_numeric_val t -> is_numeric_val (succ t).

  Inductive is_value : term -> Prop :=
  | v_true : is_value ttrue
  | v_false : is_value tfalse
  | v_num : forall t, is_numeric_val t -> is_value t.

  Lemma numeric_value_is_value : forall (t : term),
    is_numeric_val t -> is_value t.
  Proof.
    intros t H.
    destruct H as [| t' H'].
    - apply v_num. exact nv_O.
    - apply v_num. apply nv_succ. exact H'.
  Qed.

  (* 8.2 *)
  Inductive type : Type :=
  | TBool
  | TNat.

  Scheme Equality for type.

  Inductive has_type : term -> type -> Prop :=
  | T_True : has_type ttrue TBool
  | T_False : has_type tfalse TBool
  | T_If : forall t1 t2 t3 T,
      has_type t1 TBool ->
      has_type t2 T ->
      has_type t3 T ->
      has_type (iif t1 t2 t3) T
  | T_Zero : has_type O TNat
  | T_Succ : forall t1,
      has_type t1 TNat ->
      has_type (succ t1) TNat
  | T_Pred : forall t1,
      has_type t1 TNat ->
      has_type (pred t1) TNat
  | T_IsZero : forall t1,
      has_type t1 TNat ->
      has_type (iszero t1) TBool.

  Lemma numeric_value_type : forall (t : term),
    is_numeric_val t -> has_type t TNat.
  Proof.
    intros t H.
    induction H as [| t' H' IH].
    - apply T_Zero.
    - apply T_Succ. exact IH.
  Qed.

  Inductive step : term -> term -> Prop :=
  | E_IfTrue : forall t2 t3,
      step (iif ttrue t2 t3) t2
  | E_IfFalse : forall t2 t3,
      step (iif tfalse t2 t3) t3
  | E_If : forall t1 t1' t2 t3,
      step t1 t1' ->
      step (iif t1 t2 t3) (iif t1' t2 t3)
  | E_Succ : forall t1 t1',
      step t1 t1' ->
      step (succ t1) (succ t1')
  | E_PredZero :
      step (pred O) O
  | E_PredSucc : forall t1,
      is_numeric_val t1 ->
      step (pred (succ t1)) t1
  | E_Pred : forall t1 t1',
      step t1 t1' ->
      step (pred t1) (pred t1')
  | E_IsZeroZero :
      step (iszero O) ttrue
  | E_IsZeroSucc : forall t1,
      is_numeric_val t1 ->
      step (iszero (succ t1)) tfalse
  | E_IsZero : forall t1 t1',
      step t1 t1' ->
      step (iszero t1) (iszero t1').

  Lemma step_value_stuck : forall (t t' : term),
    is_value t ->
    step t t' ->
    t = t'.
  Proof.
    intros t t' Hval Hstep.
    destruct Hval.
    - inversion Hstep.
    - inversion Hstep.
    - inversion Hstep. subst.
      + inversion H.
      +
  Admitted.

  (* 8.2.1 *)

  Definition is_well_typed (t : term) : Prop :=
    exists (T : type), has_type t T.

  (* 8.2.2 *)
  Lemma t_ttrue_inv : forall (T : type),
    has_type ttrue T -> T = TBool.
  Proof.
    intros T H. inversion H. reflexivity.
  Qed.

  Lemma t_tfalse_inv : forall (T : type),
    has_type tfalse T -> T = TBool.
  Proof.
    intros T H. inversion H. reflexivity.
  Qed.

  Lemma t_iff_inv : forall (t1 t2 t3 : term) (T : type),
    has_type (iif t1 t2 t3) T ->
    has_type t1 TBool /\ has_type t2 T /\ has_type t3 T.
  Proof.
    intros t1 t2 t3 T H.
    inversion H as [| | | | | | H0 H1 H2].
    split.
    - exact H0.
    - split.
      + exact H1.
      + exact H2.
  Qed.

  Lemma t_O_inv : forall T,
    has_type O T -> T = TNat.
  Proof.
    intros T H. inversion H. reflexivity.
  Qed.

  Lemma t_succ_inv : forall (t1 : term) (T : type),
    has_type (succ t1) T -> has_type t1 TNat /\ T = TNat.
  Proof.
    intros t1 T H.
    inversion H as [| | | | | | H0 _].
    split.
    - exact H0.
    - reflexivity.
  Qed.

  Lemma t_pred_inv : forall (t1 : term) (T : type),
    has_type (pred t1) T -> has_type t1 TNat /\ T = TNat.
  Proof.
    intros t1 T H.
    inversion H as [| | | | | | H0 _].
    split.
    - exact H0.
    - reflexivity.
  Qed.

  Lemma t_iszero_inv : forall (t1 : term) (T : type),
    has_type (iszero t1) T -> has_type t1 TNat /\ T = TBool.
  Proof.
    intros t1 T H.
    inversion H as [| | | | | | H0 H1].
    split.
    - exact H1.
    - reflexivity.
  Qed.

  (* 8.2.3 *)

  Lemma wt_succ_inv : forall (t1 : term),
    is_well_typed (succ t1) -> is_well_typed t1.
  Proof.
    intros t1 [T H].
    apply t_succ_inv in H.
    destruct H as [H1 _].
    exists TNat.
    exact H1.
  Qed.

  Lemma wt_pred_inv : forall (t1 : term),
    is_well_typed (pred t1) -> is_well_typed t1.
  Proof.
    intros t1 [T H].
    apply t_pred_inv in H.
    destruct H as [H1 _].
    exists TNat.
    exact H1.
  Qed.

  Lemma wt_iszero_inv : forall (t1 : term),
    is_well_typed (iszero t1) -> is_well_typed t1.
  Proof.
    intros t1 [T H].
    apply t_iszero_inv in H.
    destruct H as [H1 _].
    exists TNat.
    exact H1.
  Qed.

  Lemma wt_if_inv : forall (t1 t2 t3 : term),
    is_well_typed (iif t1 t2 t3) -> is_well_typed t1 /\ is_well_typed t2 /\ is_well_typed t3.
  Proof.
    intros t1 t2 t3 [T H].
    apply t_iff_inv in H.
    destruct H as [H1 [H2 H3]].
    split.
    - exists TBool. exact H1.
    - split.
      + exists T. exact H2.
      + exists T. exact H3.
  Qed.

  Inductive subterm : term -> term -> Prop :=
  | subterm_refl : forall t, subterm t t
  | subterm_if1 : forall t1 t2 t3 s,
      subterm s t1 ->
      subterm s (iif t1 t2 t3)
  | subterm_if2 : forall t1 t2 t3 s,
      subterm s t2 ->
      subterm s (iif t1 t2 t3)
  | subterm_if3 : forall t1 t2 t3 s,
      subterm s t3 ->
      subterm s (iif t1 t2 t3)
  | subterm_succ : forall t1 s,
      subterm s t1 ->
      subterm s (succ t1)
  | subterm_pred : forall t1 s,
      subterm s t1 ->
      subterm s (pred t1)
  | subterm_iszero : forall t1 s,
      subterm s t1 ->
      subterm s (iszero t1).

  Lemma subterms_typed : forall (t s : term) (T : type),
    has_type t T ->
    subterm s t ->
    exists (T' : type), has_type s T'.
  Proof.
    intros t s T Htype Hst.
    generalize dependent T.
    induction Hst.
    - intros T Htype. exists T. exact Htype.
    - intros T Htype.
      apply t_iff_inv in Htype.
      destruct Htype as [H1 [_ _]].
      apply IHHst in H1.
      exact H1.
    - intros T Htype.
      apply t_iff_inv in Htype.
      destruct Htype as [_ [H2 _]].
      apply IHHst in H2.
      exact H2.
    - intros T Htype.
      apply t_iff_inv in Htype.
      destruct Htype as [_ [_ H3]].
      apply IHHst in H3.
      exact H3.
    - intros T Htype.
      apply t_succ_inv in Htype.
      destruct Htype as [H1 _].
      apply IHHst in H1.
      exact H1.
    - intros T Htype.
      apply t_pred_inv in Htype.
      destruct Htype as [H1 _].
      apply IHHst in H1.
      exact H1.
    - intros T Htype.
      apply t_iszero_inv in Htype.
      destruct Htype as [H1 _].
      apply IHHst in H1.
      exact H1.
  Qed.

  (*
    This is essentially the same as the previous lemma,
    and it is piggybacking off it,
    but it is stated with the is_well_typed predicate instead.
  *)
  Corollary subterms_welltyped : forall (t s : term),
    is_well_typed t -> subterm s t -> is_well_typed s.
  Proof.
    intros t s Hwt Hst.
    revert Hwt.
    induction Hst.
      - intros Hwt. exact Hwt.
  Admitted.

  (* 8.2.4 *)
  Lemma uniqueness_of_types : forall (t : term) (T1 T2 : type),
    has_type t T1 -> has_type t T2 -> T1 = T2.
  Proof.
    intros t T1 T2 H1 H2.
    generalize dependent T2.
    induction H1; intros T2 H2.
    - apply t_ttrue_inv in H2. rewrite H2. reflexivity.
    - apply t_tfalse_inv in H2. rewrite H2. reflexivity.
    - apply t_iff_inv in H2.
      destruct H2 as [_ [H2_2 _]].
      apply IHhas_type2 in H2_2.
      rewrite H2_2.
      reflexivity.
    - apply t_O_inv in H2. rewrite H2. reflexivity.
    - apply t_succ_inv in H2.
      destruct H2 as [_ H2_2].
      rewrite H2_2.
      reflexivity.
    - apply t_pred_inv in H2.
      destruct H2 as [_ H2_2].
      rewrite H2_2.
      reflexivity.
    - apply t_iszero_inv in H2.
      destruct H2 as [_ H2_2].
      rewrite H2_2.
      reflexivity.
  Qed.

  (* 8.3.1 *)
  Lemma canonical_forms_bool : forall (t : term),
    is_value t -> has_type t TBool -> t = ttrue \/ t = tfalse.
  Proof.
    intros t Hval Htype.
    destruct Hval.
    - left. reflexivity.
    - right. reflexivity.
    - apply numeric_value_type in H.
      apply uniqueness_of_types with (T1 := TNat) in Htype; try assumption.
      discriminate Htype.
  Qed.

  Lemma canonical_forms_nat : forall (t : term),
    is_value t -> has_type t TNat -> is_numeric_val t.
  Proof.
    intros t Hval Htype.
    destruct Hval.
    - inversion Htype.
    - inversion Htype.
    - exact H.
  Qed.

  (* 8.3.2 *)
  Lemma progress : forall (t : term) (T : type),
    has_type t T -> is_value t \/ exists (t' : term), step t t'.
  Proof.
    intros t T Htype.
    induction Htype.
    (* T-True *)
    - left. constructor.
    (* T-False *)
    - left. constructor.
    (* T-If *)
    - right. destruct IHHtype1 as [Hval1 | [t1' Hstep1]]; try assumption.
      + apply canonical_forms_bool in Hval1; try assumption.
        destruct Hval1 as [Htrue | Hfalse].
        * exists t2. rewrite Htrue. constructor.
        * exists t3. rewrite Hfalse. constructor.
      + exists (iif t1' t2 t3). constructor. exact Hstep1.
    (* T-Zero *)
    - left. constructor. constructor.
    (* T-Succ *)
    - destruct IHHtype as [Hval1 | [t1' Hstep1]]; try assumption.
      + apply canonical_forms_nat in Hval1; try assumption.
        left.
        apply nv_succ in Hval1.
        apply numeric_value_is_value in Hval1.
        exact Hval1.
      + right.
        exists (succ t1').
        constructor.
        exact Hstep1.
    (* T-Pred *)
    - destruct IHHtype as [Hval1 | [t1' Hstep1]]; try assumption.
      + apply canonical_forms_nat in Hval1; try assumption.
        right.
        destruct Hval1 as [| t1'' Hnv].
        * exists O. constructor.
        * exists t1''. constructor. exact Hnv.
      + right.
        exists (pred t1').
        constructor.
        exact Hstep1.
    (* T-IsZero *)
    - destruct IHHtype as [Hval1 | [t1' Hstep1]]; try assumption.
      + apply canonical_forms_nat in Hval1; try assumption.
        right.
        destruct Hval1 as [| t1'' Hnv].
        * exists ttrue. constructor.
        * exists tfalse. constructor. exact Hnv.
      + right.
        exists (iszero t1').
        constructor.
        exact Hstep1.
  Qed.

  (* 8.3.3 *)
  Lemma preservation : forall (t t' : term) (T : type),
    has_type t T -> step t t' -> has_type t' T.
  Proof.
    intros t t' T Htype Hstep.
    generalize dependent t'.
    (* Induction on the typing derivation *)
    induction Htype; intros t' Hstep.
    (* T-True *)
    - inversion Hstep.
    (* T-False *)
    - inversion Hstep.
    (* T-If *)
    - inversion Hstep; subst.
      + (* E-IfTrue *)
        assumption.
      + (* E-IfFalse *)
        assumption.
      + (* E-If *)
        apply T_If; try assumption. apply IHHtype1. assumption.
    (* T-Zero *)
    - inversion Hstep.
    (* T-Succ *)
    - inversion Hstep; subst.
      + (* E-Succ *)
        apply T_Succ. apply IHHtype. assumption.
    (* T-Pred *)
    - inversion Hstep; subst.
      + (* E-PredZero *)
        apply T_Zero.
      + (* E-PredSucc *)
        apply numeric_value_type. assumption.
      + (* E-Pred *)
        apply T_Pred. apply IHHtype. assumption.
    (* T-IsZero *)
    - inversion Hstep; subst.
      + (* E-IsZeroZero *)
        apply T_True.
      + (* E-IsZeroSucc *)
        apply T_False.
      + (* E-IsZero *)
        apply T_IsZero. apply IHHtype. assumption.
  Qed.

  (* 8.3.3 *)
  Lemma preservation_by_eval_drvs : forall (t t' : term) (T : type),
    has_type t T -> step t t' -> has_type t' T.
  Proof.
    intros t t' T Htype Hstep.
    generalize dependent T.
    (* Induction on the evaluation derivation *)
    induction Hstep; intros T Htype.
    (* E-IfTrue *)
    - apply t_iff_inv in Htype.
      destruct Htype as [H1 [H2 H3]].
      assumption.
    (* E-IfFalse *)
    - apply t_iff_inv in Htype.
      destruct Htype as [H1 [H2 H3]].
      assumption.
    (* E-If *)
    - apply t_iff_inv in Htype.
      destruct Htype as [H1 [H2 H3]].
      apply T_If; try assumption.
      apply IHHstep. exact H1.
    (* E-Succ *)
    - apply t_succ_inv in Htype.
      destruct Htype as [H1 H2].
      apply IHHstep in H1.
      rewrite H2.
      apply T_Succ.
      exact H1.
    (* E-PredZero *)
    - apply t_pred_inv in Htype.
      destruct Htype as [H1 H2].
      rewrite H2.
      apply T_Zero.
    (* E-PredSucc *)
    - apply t_pred_inv in Htype.
      destruct Htype as [H1 H2].
      rewrite H2.
      apply numeric_value_type.
      exact H.
    (* E-Pred *)
    - apply t_pred_inv in Htype.
      destruct Htype as [H1 H2].
      apply IHHstep in H1.
      rewrite H2.
      apply T_Pred.
      exact H1.
    (* E-IsZeroZero *)
    - apply t_iszero_inv in Htype.
      destruct Htype as [H1 H2].
      rewrite H2.
      apply T_True.
    (* E-IsZeroSucc *)
    - apply t_iszero_inv in Htype.
      destruct Htype as [H1 H2].
      rewrite H2.
      apply T_False.
    (* E-IsZero *)
    - apply t_iszero_inv in Htype.
      destruct Htype as [H1 H2].
      apply IHHstep in H1.
      rewrite H2.
      apply T_IsZero.
      exact H1.
  Qed.

  (* 8.3.6 *)
  Lemma not_subject_expansion : ~(
    forall (t t' : term) (T : type),
    step t t' ->
    has_type t' T ->
    has_type t T
  ).
  Proof.
    intros H.
    specialize (H (iif ttrue O ttrue) O TNat).
    assert (has_type (iif ttrue O ttrue) TNat).
    { apply H.
      - constructor.
      - constructor.
    }
    inversion H0 as [| | | | | | H1 H2 H3].
    inversion H3.
  Qed.

  (* 8.3.7 *)
  Inductive step_big : term -> term -> Prop :=
  | B_Value : forall (t : term),
    is_value t ->
    step_big t t
  | B_IfTrue : forall (t1 t2 t3 v2 : term),
    step_big t1 ttrue ->
    is_value v2 ->
    step_big t2 v2 ->
    step_big (iif ttrue t2 t3) v2
  | B_IfFalse : forall (t1 t2 t3 v3 : term),
    step_big t1 tfalse ->
    is_value v3 ->
    step_big t3 v3 ->
    step_big (iif tfalse t2 t3) v3
  | B_Succ : forall (t1 nv1 : term),
    is_numeric_val nv1 ->
    step_big t1 nv1 ->
    step_big (succ t1) (succ nv1)
  | B_PredZero : forall (t1 : term),
    step_big t1 O ->
    step_big (pred O) O
  | B_PredSucc : forall (t1 nv1 : term),
    is_numeric_val nv1 ->
    step_big t1 (succ nv1) ->
    step_big (pred t1) nv1
  | B_IsZeroZero : forall (t1 : term),
    step_big t1 O ->
    step_big (iszero t1) ttrue
  | B_IsZeroSucc : forall (t1 nv1 : term),
    is_numeric_val nv1 ->
    step_big t1 (succ nv1) ->
    step_big (iszero t1) tfalse.

  Lemma big_step_progress : forall (t : term) (T : type),
    has_type t T -> is_value t \/ exists (t' : term), step_big t t'.
  Proof.
    intros t T Htype.
    induction Htype.
    (* T-True *)
    - left. constructor.
    (* T-False *)
    - left. constructor.
    (* T-If *)
    - destruct IHHtype1 as [Hval1 | [t1' Hstep1]]; try assumption.
      + right. apply canonical_forms_bool in Hval1; try assumption.
        destruct Hval1 as [Htrue | Hfalse].
        * exists t2. rewrite Htrue.
  Admitted.

  Lemma big_step_preservation : forall (t t' : term) (T : type),
    has_type t T -> step_big t t' -> has_type t' T.
  Proof.
    intros t t' T Htype Hstep.
    generalize dependent t'.
    induction Htype; intros t' Hstep.
    (* T-True *)
    - inversion Hstep; subst. apply T_True.
    (* T-False *)
    - inversion Hstep; subst. apply T_False.
    (* T-If *)
    - inversion Hstep; subst.
      + apply T_If; try assumption.
      + apply IHHtype2. assumption.
      + apply IHHtype3. assumption.
    (* T-Zero *)
    - inversion Hstep; subst. apply T_Zero.
    (* T-Succ *)
    - inversion Hstep; subst.
      + apply T_Succ. exact Htype.
      + apply T_Succ. apply IHHtype. assumption.
    (* T-Pred *)
    - inversion Hstep; subst.
      + apply T_Pred. assumption.
      + assumption.
      + apply IHHtype in H1.
        apply t_succ_inv in H1.
        apply H1.
    (* T-IsZero *)
    - inversion Hstep; subst.
      + apply T_IsZero. assumption.
      + apply T_True.
      + apply T_False.
  Qed.

  (* 8.3.8 *)
  (* Inductive term2 : Type :=
  | ttrue
  | tfalse
  | iif (t1 t2 t3 : term2)
  | O
  | succ (t : term2)
  | pred (t : term2)
  | iszero (t : term2)
  | wrong. *)
End Chap8.