Stuck on proofs...

Expressions.v

Require Import String.

Inductive ty : Type :=
  | TInt : ty
  | TString : ty.

Inductive Value : Type :=
  | VInt : nat -> Value
  | VString : string -> Value.

Inductive Exp : Type :=
  | ELit : Value -> Exp
  | EVar : string -> Exp.

Inductive hasTy : (list (string * ty)) -> (Exp * ty) -> Prop := 
  | ELit_int_ty : forall ctx n, hasTy ctx (ELit (VInt n), TInt)
  | ELit_str_ty : forall ctx s, hasTy ctx (ELit (VString s), TString)
  | EVar_ty : forall ctx name a,
      (List.In (name, a) ctx) ->
      hasTy ctx (EVar name, a).


Definition ty_eq (t1 t2 : ty) : { t1 = t2 } + {~ t1 = t2 }.
  decide equality.
Defined.

Lemma pair_eq_dec : forall p1 p2: (string * ty), {p1 = p2} + {~ p1 = p2}.
Proof.
  repeat decide equality.
Qed.

Lemma neq : forall p1 p2: (string * ty), (p1 = p2) -> (p1 <> p2) -> False.
Proof.
  intros.
  intuition.
Qed.

Lemma not_in : forall (ctx : list (string * ty)) (p : (string * ty)), (List.In p ctx) -> (~ List.In p ctx) -> False.
Proof.
  intros.
  intuition.
Qed.

Definition in_ctx (ctx : list (string * ty)) (p : (string * ty)) : { List.In p ctx } + {~ List.In p ctx}.
  induction ctx.
  right.
  intros Hnot.
  inversion Hnot.
  destruct IHctx.
  destruct (pair_eq_dec a p).
  left.
  simpl.
  left.
  apply e.
  left.
  simpl.
  right.
  apply i.
  destruct (pair_eq_dec a p).
  left.
  simpl.
  left.
  apply e.
  right.
  simpl.
  intros Hnot.
  destruct Hnot.
  apply (neq a p).
  apply H.
  apply n0.
  apply (not_in ctx p).
  apply H.
  apply n.
Defined.

Definition is_int (ctx : list (string * ty)) (exp : Exp) : bool.
  assert ((hasTy ctx (exp, TInt)) + (~ hasTy ctx (exp, TInt))).
  induction exp.
  induction v.
  left.
  apply (ELit_int_ty ctx n).
  right.
  intros Hnot.
  inversion Hnot.
  destruct (in_ctx ctx (s, TInt)).
  left.
  apply (EVar_ty ctx s TInt).
  apply i.
  right.
  intros Hnot.
  inversion Hnot.
  apply (not_in ctx (s, TInt)).
  apply H1.
  apply n.
  destruct H.
  {
    exact true. 
  }
  {
    exact false.
  }
Defined.

Definition infer (ctx : list (string * ty)) (exp : Exp) : option (Exp * ty).
  assert (is_int ctx exp).

The latest change seems to solve in_ctx, but when I try to advance past Qed. I get an error saying that Cannot guess decreasing argument of fix..

New version. Don't understand what I'm doing.