/stlc_slop2.v at 799290752a917144ecb8bf2ea71072c07d16700a

(** Simply typed lambda calculus in Rocq!
Ported from https://git.unnamed.website/miscelleaneous/tree/STLC.lean *)

From Stdlib Require Import Arith Bool Lia List Unicode.Utf8.
Import ListNotations.
From Hammer Require Import Tactics Hammer.

(** We use Greek letters for variables with type [Typ] *)
Inductive Typ : Type :=
  (** New named type *)
  | new : nat → Typ
  (** Function type *)
  | fn : Typ → Typ → Typ.

Fixpoint Typ_eqb (a b : Typ) : bool :=
  match a, b with
  | new x, new y => Nat.eqb x y
  | fn a1 b1, fn a2 b2 => Typ_eqb a1 a2 && Typ_eqb b1 b2
  | _, _ => false
  end.

Lemma Typ_eqb_refl : ∀ t, Typ_eqb t t = true.
Proof.
  induction t.
  - apply Nat.eqb_refl.
  - hauto lq: on.
Qed.

Lemma Typ_eqb_eq : ∀ a b, Typ_eqb a b = true ↔ a = b.
Proof.
  induction a as [x | a1 IHa1 a2 IHa2]; destruct b as [y | b1 b2]; split; try discriminate.
  - sfirstorder use: Nat.eqb_eq.
  - sfirstorder use: Nat.eqb_refl.
  - intro H.
    apply andb_true_iff in H.
    sfirstorder.
  - hauto lq: on use: Typ_eqb_refl.
Qed.

Inductive Term : Type :=
  (** variable *)
  | var : nat → Term
  (** lambda with de Bruijn indices *)
  | lam : Term → Term
  (** Function application *)
  | app : Term → Term → Typ → Term.

(** The type checker! *)
Fixpoint check (env : list Typ) (t : Term) (τ : Typ) : bool :=
  match t with
  | var x =>
    match nth_error env x with
    | Some t' => Typ_eqb t' τ
    | None => false
    end
  | lam b =>
    match τ with
    | fn α β => check (α :: env) b β
    | _ => false
    end
  | app f a α =>
    check env f (fn α τ) && check env a α
  end.

(** Increment free variables by [k] *)
Fixpoint incr (k d : nat) (t : Term) : Term :=
  match t with
  | var x => var (if Nat.leb d x then x + k else x)
  | lam b => lam (incr k (S d) b)
  | app f a α => app (incr k d f) (incr k d a) α
  end.

(** [incr] preserves type *)
Theorem check_incr : ∀ t env' env env'' τ k,
  check (env' ++ env) t τ = true →
  length env'' = k →
  check (env' ++ env'' ++ env) (incr k (length env') t) τ = true.
Proof.
  induction t as [x | b IHb | f IHf a IHa α]; intros env' env env'' τ k H Hk.
  - simpl in H.
    simpl.
    destruct (Nat.leb (length env') x) eqn:E; simpl.
    + apply Nat.leb_le in E.
      rewrite nth_error_app2 in H by lia.
      rewrite nth_error_app2 by lia.
      rewrite nth_error_app2 by lia.
      replace (x + k - length env' - length env'') with (x - length env') by lia.
      exact H.
    + apply Nat.leb_gt in E.
      rewrite nth_error_app1 in H by lia.
      rewrite nth_error_app1 by lia.
      exact H.
  - destruct τ as [|τ1 τ2]; [discriminate|].
    simpl in H.
    exact (IHb (τ1 :: env') env env'' τ2 k H Hk).
  - simpl in H.
    apply andb_true_iff in H.
    destruct H as [H1 H2].
    hauto lq: on.
Qed.

(** [incr 0] does nothing *)
Theorem incr_zero : ∀ t d, incr 0 d t = t.
Proof.
  induction t.
  - hauto l: on.
  - sfirstorder.
  - sfirstorder.
Qed.

(** Substitute [s] at index [n] in a term *)
Fixpoint sub (n : nat) (s : Term) (t : Term) : Term :=
  match t with
  | var x =>
    if Nat.eqb x n then incr n 0 s
    else var (if Nat.ltb n x then x - 1 else x)
  | lam b =>
    lam (sub (S n) s b)
  | app f a α =>
    app (sub n s f) (sub n s a) α
  end.

(** [sub] preserves type *)
Theorem check_sub : ∀ t env' env σ s τ,
  check (env' ++ σ :: env) t τ = true →
  check env s σ = true →
  check (env' ++ env) (incr (length env') 0 s) σ = true →
  check (env' ++ env) (sub (length env') s t) τ = true.
Proof.
  induction t as [x | b IHb | f IHf a IHa α];
    intros env' env σ s' τ H Hs Hs'.
  - simpl in H. simpl.
    destruct (Nat.eqb x (length env')) eqn:E; simpl.
    + apply Nat.eqb_eq in E. subst x.
      rewrite nth_error_app2 in H by lia.
      replace (length env' - length env') with 0 in H by lia.
      simpl in H.
      apply Typ_eqb_eq in H. subst τ.
      exact Hs'.
    + apply Nat.eqb_neq in E.
      destruct (Nat.ltb (length env') x) eqn:E2; simpl.
      * apply Nat.ltb_lt in E2.
        rewrite nth_error_app2 in H by lia.
        rewrite nth_error_app2 by lia.
        replace (x - length env') with (S (x - length env' - 1)) in H by lia.
        simpl in H.
        replace (x - 1 - length env') with (x - length env' - 1) by lia.
        exact H.
      * apply Nat.ltb_ge in E2.
        assert (x < length env') by lia.
        rewrite nth_error_app1 in H by lia.
        rewrite nth_error_app1 by lia.
        exact H.
  - destruct τ as [|τ1 τ2]; [simpl in H; discriminate|].
    simpl in H. simpl.
    apply (IHb (τ1 :: env') env σ s' τ2 H Hs).
    apply (check_incr s' [] env (τ1 :: env') σ (S (length env'))).
    + exact Hs.
    + reflexivity.
  - simpl in H. apply andb_true_iff in H. destruct H as [H1 H2].
    simpl.
    apply andb_true_iff.
    sfirstorder.
Qed.

(** Eval without worrying about types.
    Rocq doesn't have [partial def], so we use a fuel parameter. *)
Fixpoint eval_untyped (fuel : nat) (t : Term) : Term :=
  match fuel with
  | 0 =>
    t
  | S fuel' =>
    match t with
    | var x =>
      var x
    | lam b =>
      lam (eval_untyped fuel' b)
    | app f a α =>
      let a' := eval_untyped fuel' a in
      match eval_untyped fuel' f with
      | lam b => eval_untyped fuel' (sub 0 a' b)
      | x => app x a' α
      end
    end
  end.

(** Eval a well-typed expression.
    Like the Lean version this admits termination; we use a fuel
    parameter so the function is structurally recursive in Rocq.
    TODO: prove termination via a logical-relations argument
    (see https://cecchetti.sites.cs.wisc.edu/cs704/2025fa/notes/lec23-normalization.pdf). *)
Fixpoint eval (fuel : nat) (env : list Typ) (t : Term) (τ : Typ)
    (h : check env t τ = true) {struct fuel}
    : { t' : Term | check env t' τ = true }.
Proof.
  destruct fuel as [|fuel'].
  - exact (exist _ t h).
  - destruct t as [x | b | f0 a0 α0].
    + exact (exist _ (var x) h).
    + destruct τ as [|α β]; [discriminate|].
      simpl in h.
      destruct (eval fuel' (α :: env) b β h) as [b' hb].
      exists (lam b').
      simpl.
      exact hb.
    + simpl in h. apply andb_true_iff in h. destruct h as [hf ha].
      destruct (eval fuel' env a0 α0 ha) as [a' ha'].
      destruct (eval fuel' env f0 (fn α0 τ) hf) as [f' hf'].
      destruct f' as [x' | b | g c β].
      * exists (app (var x') a' α0).
        apply andb_true_iff.
        auto.
      * simpl in hf'.
        apply (eval fuel' env (sub 0 a' b) τ).
        apply (check_sub b [] env α0 a' τ hf' ha').
        simpl.
        rewrite incr_zero.
        exact ha'.
      * exists (app (app g c β) a' α0). simpl.
        apply andb_true_iff.
        auto.
Defined.