Library CoLoR.Term.SimpleType.TermsEta

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Adam Koprowski, 2006-04-27
The eta-reduction relation of simply typed lambda-calculus.

Set Implicit Arguments.


Module TermsEta (Sig : TermsSig.Signature).

  Module Export TB := TermsBeta.TermsBeta Sig.

  Definition Eta_preterm Pt A := \A => prelift Pt 1 @@ %0.

  Definition EtaApp : forall M A B, type M = A --> B ->
    { M': Term | env M' = env M
      /\ term M' = Eta_preterm (term M) A /\ type M' = type M }.


  Inductive EtaExpansionStep : relation Term :=
  | EtaExp: forall M A B (Mtyp: type M = A --> B), EtaExpansionStep M (proj1_sig (EtaApp M Mtyp)).

  Definition EtaExpansion := Reduction EtaExpansionStep.
  Notation "M -e+-> N" := (EtaExpansion M N) (at level 30).

  Inductive EtaReductionStep : relation Term :=
  | EtaRed: forall M A B (Mtyp: type M = A --> B), EtaReductionStep (proj1_sig (EtaApp M Mtyp)) M.

  Definition EtaReduction := Reduction EtaReductionStep.
  Notation "M -e-> N" := (EtaRed M N) (at level 30).

End TermsEta.