(** * Exercise 9.1: Formalization of simply typed lambda calculus with error - *)

(** We define types, variables, terms, and environments. *)

Inductive ty := 
|  Nat: ty
|  Fun: ty -> ty -> ty.

Inductive var :=
|  Var: nat -> var.

Inductive ter :=
|  O: ter
|  V: var -> ter
|  L: var -> ty -> ter -> ter
|  A: ter -> ter -> ter
|  E: ter    (* error *)
|  T: ter -> ter -> ter.  (* try t1 with t2 *)

Inductive value: ter -> Prop := 
|  value_O: value O
|  value_V: forall x, value (V x)
|  value_L: forall x tau t, value (L x tau t).

(* a result is either a value or error *)
Inductive result: ter -> Prop := 
|  result_O: result O
|  result_V: forall x, result (V x)
|  result_L: forall x tau t, result (L x tau t)
|  result_E: result E.

Hint Constructors value result.
Ltac sinv h := (inversion h; clear h; subst).  (* a useful tactic *)

(* of course, values are included in the results: *)
Proposition Value_Result : forall v, value v -> result v.
Proof with eauto. intros v H. induction H... Qed.  

Hint Unfold Value_Result. 


(** Definition of reduction relation. *)

Hypothesis subst: var -> ter -> ter -> ter.

Inductive step: ter -> ter -> Prop :=
|  step_Adl: forall t1 t1' t2, step t1 t1' -> step (A t1 t2) (A t1' t2)
|  step_Adr: forall v t t', value v -> step t t' -> step (A v t) (A v t')
|  step_A : forall v x tau t, value v -> step (A (L x tau t) v) (subst x v t)
|  step_E1 : forall t, step (A E t) E
|  step_E2 : forall v, value v -> step (A v E) E 
|  step_Td : forall t1 t1' t2, step t1 t1' -> step (T t1 t2) (T t1' t2)
|  step_T1 : forall v t2, value v -> step (T v t2) v
|  step_T2 : forall t2, step (T E t2) t2.

Hint Constructors step.


(** Definition of the evaluation relation *)

Inductive eval: ter -> ter -> Prop :=
(* fill in your definition of the big-step semantics here *).

Hint Constructors eval.

Proposition Eval_codom: forall t r, eval t r -> result r. 
Proof. 
intros t v HE. induction HE; eauto.
Qed.


(** The reflexive-transitive closure of the step relation *)
Inductive stepstar: ter -> ter -> Prop :=
| stepstar_refl : forall t, stepstar t t
| stepstar_step : forall s t u, step s t -> stepstar t u -> stepstar s u.

Hint Constructors stepstar.

Lemma stepstar_trans: forall s t u, 
stepstar s t -> stepstar t u -> stepstar s u.
Proof.
intros s t u HS. induction HS;  eauto.
Qed.

Lemma Lifting: forall f,
(forall s t, step s t -> step (f s) (f t)) -> 
forall s t, stepstar s t -> stepstar (f s) (f t) .
Proof.
intros. induction H0; eauto.
Qed.


(** The coincidence proof *)

Proposition Eval_expansion: forall s t r, 
step s t -> eval t r -> eval s r. 
Proof with eauto.
(* Fill in your proof here *)
Admitted.

Lemma Step2Eval: forall t r, 
result r -> stepstar t r -> eval t r. 
Proof with eauto.
(* Fill in your proof here *)
Admitted.

Lemma Eval2Step: forall t r, eval t r -> stepstar t r.
Proof with eauto.
(* Fill in your proof here *)
Admitted.


Theorem Coincidence: forall t r, result r ->
(eval t r <-> stepstar t r). 
Proof with eauto.
intuition. 
(* Fill in your proof here *)
Admitted.