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.