Library Premodel

Interpretation yields a premodel of lambda calculus

Require Export Interpretation.
Require Import Contexts Types.

Implicit Types Gamma Delta : context.

Implicit Types u v : inttype -> Prop.
Implicit Types m n : basetype -> Prop.

Implicit Types A B C : inttype.
Implicit Types F G H : basetype.

Implicit Types x y z : var.
Implicit Types s t : term.

Variables are interpreted according to the type context

Lemma int_x rho x : valid rho -> [ x ] rho ~ rho x.
intros v A.
split.
- intros [n Gamma crG tyG].
  assert (E := invtyVar _ _ _ _ tyG).
  eapply compatible_sub_Gamma ; eauto.
- intros.
  apply intty with 0 (fun y => if decide (x =y) then A :type else OMEGA) ; auto.
  + intros y B E. decide (x = y) ; auto.
  + apply tyVarA. decide (x = x) ; auto.
Qed.

Term applications are interpreted as filter applications

Lemma int_st rho s t : valid rho -> [ s t ] rho ~ [ s ] rho @ [ t ] rho.
intros v.
apply closure_filter_equiv ; auto using int_IF.
- intros F [m Gamma ? tys].
  inversion tys.
  exists A ; eauto using intty, compatible_sub, cte_csub_R.

- intros F [A [n Gamma ? ?] [m Delta ? ?]].
  eauto using intty, compatible_cint.
Qed.

For non-empty arguments u, the interpretation of an abstraction respects beta reduction

Lemma int_lam rho s u : valid rho -> IFilter u -> (exists B, u B) -> [ s ] (u .: rho ) ~ [ Lam s ] rho @ u.
intros v uF [B uB].
apply closure_filter_equiv ; auto using int_IF, valid_up.
- intros F [n Gamma c tys].
  remember (Gamma 0) as V.
  destruct V as [A|].
  + exists A.
    * econstructor ; eauto using compatible_down.
      econstructor. rewrite HeqV. eauto using ty_equiv, cons_drop_inv.
    * now apply (c 0).
  + exists B ; auto.
    eapply (intty _ _ _ _ (drop 1 Gamma)) ; eauto using compatible_down.
    econstructor.
    eapply tycsub ; eauto.
    exists ((B : type ) .: Empty).
    intros [|x] ; simpl ; auto.
    * now rewrite <- HeqV.
    * now rewrite int_O.
- intros F [A [n Gamma ? tyL] ?].
  inversion tyL.
  eauto using compatible_up, intty, valid_up.
Qed.