Rec.Extras.lambda_model

From mathcomp Require Import ssreflect.all_ssreflect.
Require Import Base.axioms Base.fintype Framework.graded Extras.lambda_terms.
Set Implicit Arguments.
Unset Strict Implicit.

Local Ltac asimpl :=
  repeat progress (cbn; fsimpl; gsimpl; tm_simpl).

Section LambdaModel.
  Variable (D : Type).
  Variable (app : D -> D -> D).
  Variable (lam : (D -> D) -> D).

  Definition lambda_smodel : Tm.smodel D D := Tm.SModel id app lam.
  Notation "⟦ s ⟧ rho" := (Tm.seval lambda_smodel rho s) (at level 2, format "⟦ s ⟧ rho").

  Lemma ev_var n (rho : fin n -> D) (i : fin n) :
    ⟦ Tm.var i ⟧ rho = rho i.
  Proof. by []. Qed.

  Lemma ev_app n (rho : fin n -> D) (s t : tm n) :
    ⟦ Tm.app s t ⟧ rho = app (⟦ s ⟧ rho) (⟦ t ⟧ rho).
  Proof. by []. Qed.

  Lemma ev_lam n (rho : fin n -> D) (b : tm n.+1) :
    ⟦ Tm.lam b ⟧ rho = lam (fun v => ⟦ b ⟧ (v .: rho)).
  Proof. by []. Qed.

  Lemma ev_inst m n (rho : fin n -> D) (f : fin m -> tm n) (s : tm m) :
    ⟦ s.[f]%tm ⟧ rho = ⟦ s ⟧ (fun i => ⟦ f i ⟧ rho).
  Proof. by asimpl. Qed.

  Variable (beta : forall f x, app (lam f) x = f x).

  Inductive step {n} : tm n -> tm n -> Prop :=
  | step_beta (b : tm n.+1) (s : tm n) :
      step (Tm.app (Tm.lam b) s) b.[s .: Tm.var]%tm
  | step_appL (s1 s2 t : tm n) :
      step s1 s2 -> step (Tm.app s1 t) (Tm.app s2 t)
  | step_appR (s t1 t2 : tm n) :
      step t1 t2 -> step (Tm.app s t1) (Tm.app s t2)
  | step_lam (b1 b2 : tm n.+1) :
      @step n.+1 b1 b2 -> step (Tm.lam b1) (Tm.lam b2).

  Lemma step_invariant n (s t : tm n) :
    step s t -> forall rho, ⟦ s ⟧ rho = ⟦ t ⟧ rho.
  Proof.
    elim=> {n s t}[n b s|n s1 s2 t _ ih|n s t1 t2 _ ih|n b1 b2 _ ih] rho.
    - rewrite ev_app ev_lam beta ev_inst. f_equal. fext=>/=-[i|]//=.
    - by rewrite !ev_app ih.
    - by rewrite !ev_app ih.
    - rewrite !ev_lam. f_equal; fext=>/= d. exact: ih.
  Qed.
End LambdaModel.