Aborted attempt to prove weak normalization (with weak reductions) of system F

system_f.v

(*

Ideas:
1. Strong reduction (ugh): Keep computing through lambdas. Most straightforward, but annoying, need to reason about db even more
2. Computability take an eval context as well, so that all predicates are "up to substitution".
   Problem: how to we deal with "computable contexts"?
   E.g. aplications: Do they thake the previous elements in the env or not?
   Does "positive" style predicates help?
3. Screw this and go with names.
4. Reason about only closed terms (somehow?) Not sure how to formulate the main lemma.
5. Have explicit closures/substitutions in the terms? (I THINK THIS IS THE ONE)
6. A broken substitution that doesn't traverse lambdas? This seems fishy. Easy to try though!


*)


(* Trying to formalize the normalization of closed system F terms *)

Require Import List Arith Bool.

Import ListNotations.

Definition name := nat.

(* Don't really need de Bruijn for types *)
Inductive type :=
| Tvar : name -> type
| Arrow : type -> type -> type
| Forall : name -> type -> type.

(* Boring ol' shadowing substitution *)
Fixpoint ty_subst (n : name) (t u : type) :=
  match t with
  | Tvar k => if n =? k then u else Tvar k
  | Arrow t1 t2 => Arrow (ty_subst n t1 u) (ty_subst n t2 u)
  | Forall k t1 =>
    if n =? k then t else
    Forall k (ty_subst n t1 u)
  end.

Fixpoint is_free (n : name) (t : type) :=
  match t with
  | Tvar k => if n =? k then true else false
  | Arrow t1 t2 => (is_free n t1) || (is_free n t2)
  | Forall k t1 =>
    if n =? k then false else
      (is_free n t1)
  end.

(* No explicit type abstractions or applications: we don't really care about type-checking. *)
Inductive term :=
| Var : nat -> term
| App : term -> term -> term
| Abs : term -> term.

(* Contexts usually are backwards lists, but I'm lazy and want to use existing list stuff. *)
Definition context := list type.

Definition is_free_ctxt : name -> context -> bool :=
  fun n ctxt =>
    List.existsb (fun ty => is_free n ty) ctxt.

Definition eval_ctxt := list term.

Print List.skipn.

Inductive TmEval : eval_ctxt -> term -> term -> Prop :=
| Eval_var : forall ectx n t v,
    List.nth_error ectx n = Some t ->
    TmEval (List.skipn (S n) ectx) t v ->
    TmEval ectx (Var n) v
(* Call by name *)
| Eval_app : forall ectx t t' u v,
    TmEval ectx t (Abs t') ->
    TmEval (u :: ectx) t' v ->
    TmEval ectx (App t u) v
(* Weak reduction *)
| Eval_abs : forall ectx t, TmEval ectx (Abs t) (Abs t)
.

Hint Constructors TmEval.

(* Type checking is undecidable, but who cares? *)
Inductive Tyrel : context -> term -> type -> Prop :=
| Tyrel_var : forall ctxt n ty,
    List.nth_error ctxt n = Some ty ->
    Tyrel ctxt (Var n) ty
| Tyrel_abs : forall ctxt ty1 ty2 t,
    Tyrel (ty1::ctxt) t ty2 ->
    Tyrel ctxt (Abs t) (Arrow ty1 ty2)
| Tyrel_app : forall ctxt ty1 ty2 t u,
    Tyrel ctxt t (Arrow ty1 ty2) ->
    Tyrel ctxt u ty1 ->
    Tyrel ctxt (App t u) ty2
| Tyrel_ty_abs : forall ctxt n ty t,
    is_free_ctxt n ctxt = false ->
    Tyrel ctxt t ty ->
    Tyrel ctxt t (Forall n ty)
| Tyrel_ty_app : forall ctxt n ty1 ty2 t,
    Tyrel ctxt t (Forall n ty1) ->
    Tyrel ctxt t (ty_subst n ty1 ty2). (* No types for substs, because they only matter operationally. *)

Definition norm (ectx : eval_ctxt) (t : term) :=
  exists v, TmEval ectx t v.

(* The main theorem we *want* *)
Definition normalizes := forall t ty,
    Tyrel [] t ty -> norm [] t.

Definition valuation := name -> eval_ctxt -> term -> Prop.

Print forallb.

Fixpoint closed_n (n : nat)(t : term) : bool :=
  match t with
  | Var m => n <? m
  | Abs t => closed_n (S n) t
  | App t1 t2 => (closed_n n t1) && (closed_n n t2)
  end.

Definition closed (t : term) := closed_n 0 t.

Definition extend (f : valuation)(v : name)(P : eval_ctxt -> term -> Prop) : valuation :=
  fun var => if var =? v then P else f var.


(* Fixpoint apps (t : term) (args : eval_ctxt) : term := *)
(*   match args with *)
(*   | [] => t *)
(*   | u :: us => apps (App t u) us *)
(*   end. *)


Fixpoint apps (t : term) (args : eval_ctxt) : term :=
  match args with
  | [] => t
  | u :: us => App (apps t us) u
  end.

Record computable (P : eval_ctxt -> term -> Prop) :=
  {
  comp_norm : forall ectx t, P ectx t -> norm ectx t;
  comp_conv : forall ectx t t', (forall v, TmEval ectx t' v -> TmEval ectx t v) -> P ectx t' -> P ectx t;
  comp_whe : forall ectx t us v,
      TmEval ectx t v ->
      P ectx (apps v us) ->
      P ectx (apps t us);
  }.

(* Record computable (P : eval_ctxt -> term -> Prop) := *)
(*   { *)
(*   comp_norm : forall ectx t, P ectx t -> norm ectx t; *)
(*   comp_conv : forall ectx t t', (forall v, TmEval ectx t' v -> TmEval ectx t v) -> P ectx t' -> P ectx t; *)
(*   comp_whe : forall ectx t u t', *)
(*       TmEval ectx t (Abs t') -> *)
(*       P (u :: ectx) t' -> *)
(*       P ectx (App t u); *)
(*   }. *)


(* Lemma apps_rev_cons : forall t args a, *)
(*     apps_rev t (args ++ [a]) = apps_rev (App t a) args. *)
(* Proof. *)
(*   induction args; simpl; auto; intros. *)
(*   rewrite IHargs; auto. *)
(* Qed. *)

(* Lemma apps_rev_rev : forall t args, *)
(*     apps t args = apps_rev t (List.rev args). *)
(* Proof. *)
(*   intros t args; revert t; *)
(*     induction args; simpl; auto. *)
(*   intros; rewrite apps_rev_cons; auto. *)
(* Qed. *)


Lemma tmeval_is_abs : forall ectx t v,
    TmEval ectx t v -> exists t', v = Abs t'.
Proof.
  intros until v; intros H; induction H.
  - destruct IHTmEval; eauto.
  - destruct IHTmEval2; eauto.
  - eauto.
Qed.

Lemma eval_eval : forall ectx t v v',
    TmEval ectx t v -> TmEval ectx v v' -> TmEval ectx t v'.
Proof.
  intros until v'; intros H.
  assert (val_v := tmeval_is_abs _ _ _ H).
  destruct val_v; subst.
  intros H'; inversion H'; auto.
Qed.

Lemma eval_apps : forall ectx t us v v',
    TmEval ectx t v ->  TmEval ectx (apps v us) v' -> TmEval ectx (apps t us) v'.
Proof.
  intros until us; revert t;
    induction us; simpl; intros.
  - eapply eval_eval; eauto.
  - inversion H0; subst.
    assert (TmEval ectx (apps t us) (Abs t')) by eauto.
    econstructor; eauto.
Qed.

(* ============================ *)
(* forall (ectx : eval_ctxt) (t : term) (us : eval_ctxt) (v : term), *)
(* TmEval ectx t v -> norm ectx (apps v us) -> norm ectx (apps t us) *)
Lemma norm_apps : forall ectx t us v,
    TmEval ectx t v -> norm ectx (apps v us) -> norm ectx (apps t us).
Proof.
  intros until v.
  intros eval_t eval_apps.
  destruct eval_apps.
  exists x; eapply eval_apps; eauto.
Qed.


(* Just a sanity check *)
Lemma computable_norm : computable norm.
Proof.
  constructor; [auto | |].
  - intros until t'; intros h1 h2; destruct h2; eexists; apply h1; eauto.
  - apply norm_apps.
Qed.


(* The usual interpretation of types in system F with computable predicates *)
Fixpoint tyval (ty : type) : valuation -> eval_ctxt -> term -> Prop :=
  fun val =>
    match ty with
    | Tvar v => val v
    | Arrow t1 t2 =>
      fun ectx t =>
        norm ectx t /\
        forall u,
          tyval t1 val ectx u ->
          tyval t2 val ectx (App t u)
    | Forall v ty =>
      fun ectx t =>
        forall P, computable P -> tyval ty (extend val v P) ectx t
    end.

Definition computable_valuation (val : valuation) :=
  forall v, computable (val v).


Lemma computable_tyval : forall ty val,
    computable_valuation val ->
    computable (tyval ty val).
Proof.
  induction ty; simpl; unfold computable_valuation; intros val H; auto.
  - constructor; try split; intros; try (destruct H0; now auto).
    + destruct H1 as [[v H2] _]; eexists; apply H0; apply H2.
    + edestruct IHty2; [now eauto|].
      apply comp_conv0 with (t' := (App t' u)).
      -- intros.
         inversion H3; subst.
         econstructor; eauto.
      -- apply H1; now auto.
    + destruct H1 as [H21 H22]; destruct H21.
      eapply norm_apps; eauto; eexists; eauto.
    + (* WHE case *)
      destruct H1 as [[v' h21] h22];
        edestruct IHty2; [now eauto|].
      eapply comp_whe0 with (ectx := ectx)(t := t) (us := u :: us); now eauto.
  - constructor; try split; intros.
    + pose (P := norm).
      assert (computable P) by apply computable_norm.
      pose (val' := extend val n P).
      edestruct (IHty val'); eauto.
      unfold computable_valuation; unfold val', extend.
      intros v; destruct (v =? n); auto.
    + pose (val' := extend val n P).
      edestruct (IHty val'); unfold computable_valuation, val', extend; [intros v; destruct (v =? n)|]; eauto.
    + pose (val' := extend val n P).
      edestruct (IHty val'); unfold computable_valuation, val', extend; [intros v'; destruct (v' =? n)|]; eauto.
Qed.

Hint Resolve computable_tyval.

Print List.

(* Should we assume the lengths are the same? IDK *)
Definition ctxt_val : valuation -> eval_ctxt -> context -> Prop :=
  fun val ectx ctx =>
  forall n ty,
    nth_error ctx n = Some ty ->
    tyval ty val ectx (Var n).


Theorem ty_safe : forall ctx t ty ectx val,
    computable_valuation val ->
    Tyrel ctx t ty ->
    ctxt_val val ectx ctx ->
    tyval ty val ectx t.
Proof.
  intros ctx t ty ectx val val_comp H; revert ectx val val_comp; induction H; simpl; intros; auto.
  - (* The good stuff *)
    split; [exists (Abs t); auto|].
    intros.
    pose (ectx' := u :: ectx).
    assert (ctxt_val val ectx' (ty1 :: ctxt)).
    + unfold ectx', ctxt_val; simpl.
      destruct n; simpl; intros.
      -- inversion H2; subst.
         Check computable.
         assert (H3 : computable (tyval ty val)) by auto.
         destruct H3.
         apply comp_conv0 with (t' := u); auto.
Abort.