Coral.InterpExamples: examples of interpretations of λ-terms

Author: Benoît Montagu

Synopsis: Examples of interpretations of λ-terms.

Require Import Infrastructure.
Require Import Interp.
Require Import RLogic.
Require Import Rel.
Require Import RelExtra.
Require Import SubstEnv.
Require Import RelWf.
Require Import Transp.

Example: (λx. x x) (λx. x x)

Delta is the term λx. x x.

Example Delta := Lam (App (BVar 0) (BVar 0)).

Omega is the term (λx. x x) (λx. x x).

Example Omega := App Delta Delta.

Delta is locally closed, hence a wellformed locally-nameless term.

Lemma Delta_lc : lc Delta.
Proof.
constructor. intro. compute. constructor; constructor.
Qed.

Omega is locally closed, hence a wellformed locally-nameless term.

Lemma Omega_lc : lc Omega.
Proof.
constructor; apply Delta_lc.
Qed.

Delta has no free variable.

Lemma Delta_fv : fv Delta [<=] empty.
Proof.
simpl. fsetdec.
Qed.

Omega has no free variable.

Lemma Omega_fv : fv Omega [<=] empty.
Proof.
simpl. fsetdec.
Qed.

Omega cannot evaluate to a value.

Lemma Omega_diverges : ∀ v, not (eval Omega v).
Proof.
  intros v [Hred Hval]. remember Omega as t.
  induction Hred; subst.
  - assumption.
  - apply IHHred; auto.
    inversion H; subst.
    + reflexivity.
    + inversion H3.
    + inversion H4.
Qed.

The interpretation of Omega is the empty relation RelBot.

Lemma Interp_Omega :
  RelEquiv (Interp nil Omega Omega_lc Omega_fv) RelBot.
Proof.
  apply RelIncl_antisym; [| apply RelBot_bot ].
  destruct (Interp_equations nil Omega Omega_lc Omega_fv)
    as [Hlc1 [Hfv1 [Hlc2 [Hfv2 Heq]]]].
  rewrite Heq. clear Heq. simpl.
  destruct (Interp_equations nil Delta Hlc1 Hfv1) as [x1 [Hx1 [t1 [Heq1 [Hlc1' [Hfv1' Heq1']]]]]].
  rewrite Heq1'. clear Heq1'.
  destruct (Interp_equations nil Delta Hlc2 Hfv2) as [x2 [Hx2 [t2 [Heq2 [Hlc2' [Hfv2' Heq2']]]]]].
  rewrite Heq2'. clear Heq2'.
  simpl.
  intros e v [e' [v1 [v2 [Hleq [[Hlam1 [Hself1 Hgather1]] [[Hlam2 [Hself2 Hgather2]] Heval]]]]]].
  simpl in Hself1.
  destruct Hself1 as [Heq1' [Hdome1' [Hgoode1' Hval1]]].
  rewrite <- Heq1 in Heq1'.
  rewrite subst_env_closed in Heq1'; [| apply Delta_fv]. subst v1.
  simpl in Hself2.
  destruct Hself2 as [Heq2' [Hdome2' [Hgoode2' Hval2]]].
  rewrite <- Heq2 in Heq2'.
  rewrite subst_env_closed in Heq2'; [| apply Delta_fv]. subst v2.
  apply Omega_diverges in Heval. assumption.
Qed.

An alternative proof, using the relational logic instead of the interpretation function.

Lemma RLogic_Omega :
  RLogic nil Omega RelBot.
Proof.
  eapply RLogicSub.
  - auto with wf_rel.
  - assert (RLogic nil Delta (RelSelf Delta)) as HDelta.
    { pick fresh x.
      unfold Delta.
      replace (App (BVar 0) (BVar 0)) with (close x (App (Var x) (Var x))).
      - apply RLogicSelf with (R := RelLam empty x RelTopEnvVal (APP (RelSelf (Var x)) (RelSelf (Var x)))); [| constructor].
        apply RLogicLam; auto with wf_rel.
        assert (RLogic (x ¬ RelTopEnvVal) (Var x) (RelSelf (Var x))) as Hx.
        { apply RLogicSelf with (R := RelTopEnvVal); [| constructor].
          apply RLogicVar. simpl. destruct (x == x); congruence.
        }
        apply RLogicApp; assumption.
      - unfold close. simpl. destruct (x == x); congruence.
    }
    eapply RLogicApp; eassumption.
  - intros e v [e' [v1 [v2 [Hleq [[Heq1' [Hdome1' [Hgoode1' Hval1]]] [[Heq2' [Hdome2' [Hgoode2' Hval2]]] Heval]]]]]].
    rewrite subst_env_closed in Heq1'; [| apply Delta_fv]. subst v1.
    rewrite subst_env_closed in Heq2'; [| apply Delta_fv]. subst v2.
    apply Omega_diverges in Heval. assumption.
Qed.