Coral.EvalFacts: properties of the evaluation relation

Author: Benoît Montagu
Copyright © Inria 2020 CeCILL-B License
Synopsis: Facts about the eval relation.

Require Import Infrastructure.
Import Notations.
Require Import StepsFacts.

eval produces locally-closed terms when it is given locally-closed terms.
Lemma eval_lc t v:
  eval t v →
  lc t →
  lc v.
Proof.
  intros [? ?] ?. eauto using steps_lc.
Qed.

Hint Resolve eval_lc : core.

eval produces terms with less free variables than its input term.
Lemma eval_fv t v:
  eval t v →
  fv v [<=] fv t.
Proof.
  intros [? ?]. eauto using steps_fv.
Qed.

eval always produces values.
Lemma eval_is_value t v: eval t v → is_value v.
Proof.
  intros [? ?]. assumption.
Qed.

Hint Resolve eval_is_value : core.

eval gives back its input as a result, when its input is a value.
Lemma eval_of_value t v: eval t v → is_value t → t = v.
Proof.
  intros [Hstep Hval2] Hval1.
  inversion Hstep; subst; auto.
  exfalso. eapply is_value_normal; eauto.
Qed.

The eval relation is reflexive for values.
Lemma eval_refl v:
  is_value v →
  eval v v.
Proof.
  intro. split; auto.
  reflexivity.
Qed.

Hint Resolve eval_refl : core.

eval is idempotent.
Lemma eval_eval t v:
  eval t v →
  eval v v.
Proof.
  intro. apply eval_refl; eauto.
Qed.

Hint Resolve eval_eval : core.

eval produces a good value if its input is locally-closed and has no free variables.
Lemma eval_good_value t v:
  lc t →
  fv t [<=] empty →
  eval t v →
  good_value v.
Proof.
  intros Hlc Hfv Heval. split; [|split]; eauto.
  rewrite (eval_fv _ _ Heval). assumption.
Qed.

Hint Resolve eval_good_value : core.

Unfolding lemma for eval.
Lemma eval_iff t v:
  eval t v ↔
  match t with
  | BVar _ | Var _ ⇒ False
  | Let t1 t2 ⇒ ∃ t1', eval t1 t1' ∧ eval (open t2 t1') v
  | Lam _ ⇒ t = v
  | App t1 t2 ⇒ ∃ t1' t2', eval t1 (Lam t1') ∧ eval t2 t2' ∧ eval (open t1' t2') v
  | Unit ⇒ v = Unit
  | Pair t1 t2 ⇒ ∃ t1' t2', eval t1 t1' ∧ eval t2 t2' ∧ v = Pair t1' t2'
  | Fst t ⇒ ∃ t2', eval t (Pair v t2')
  | Snd t ⇒ ∃ t1', eval t (Pair t1' v)
  | InjL t ⇒ ∃ t', eval t t' ∧ InjL t' = v
  | InjR t ⇒ ∃ t', eval t t' ∧ InjR t' = v
  | Match t t1 t2 ⇒
    (∃ t', eval t (InjL t') ∧ eval (open t1 t') v)
    ∨ (∃ t', eval t (InjR t') ∧ eval (open t2 t') v)
  end.
Proof.
  split.
  - { intros [Hsteps Hval]. induction Hsteps.
      - destruct x; simpl in Hval; try contradiction; auto.
        + destruct Hval as [Hval1 Hval2]. ∃ x1, x2. split; [| split]; auto.
        + ∃ x. split; auto.
        + ∃ x. split; auto.
      - generalize dependent z. induction H; intros.
        + ∃ t1, t2. split; [| split].
          × split; simpl; auto. reflexivity.
          × split; auto. reflexivity.
          × split; auto.
        + destruct (IHHsteps Hval) as [t1'' [t2'' [Heval1 [Heval2 Heval3]]]].
          ∃ t1'', t2''. split; [| split] ; auto.
          destruct Heval1. split; simpl; auto. econstructor; eauto.
        + destruct (IHHsteps Hval) as [t1'' [t2'' [Heval1 [Heval2 Heval3]]]].
          ∃ t1'', t2''. split; [| split] ; auto.
          destruct Heval2. split; simpl; auto. econstructor; eauto.
        + ∃ t1. split.
          × split; auto. reflexivity.
          × split; auto.
        + destruct (IHHsteps Hval) as [t1'' [Heval1 Heval2]].
          destruct Heval1. ∃ t1''. split; auto. split; auto. econstructor; eauto.
        + ∃ t2. split; [| split]; auto using steps_congruence_Pair_left.
        + ∃ t1. split; [| split]; simpl;
            auto using steps_congruence_Pair_right.
        + destruct (IHHsteps Hval) as [t1'' [t2'' [Heval1 [Heval2 Heq]]]].
          ∃ t1'', t2''. split; [| split]; auto.
          destruct Heval1. split; auto. econstructor; eauto.
        + destruct (IHHsteps Hval) as [t1'' [t2'' [Heval1 [Heval2 Heq]]]].
          ∃ t1'', t2''. split; [| split]; auto.
          destruct Heval2. split; auto. econstructor; eauto.
        + destruct (IHHsteps Hval) as [t2' [Hsteps2 Hval2]].
          ∃ t2'. split; simpl; auto. transitivity t'; auto.
          econstructor; eauto. reflexivity.
        + destruct (IHHsteps Hval) as [t1' [Hsteps1 Hval1]].
          ∃ t1'. split; simpl; auto. transitivity t'; auto.
          econstructor; eauto. reflexivity.
        + destruct (IHHsteps Hval) as [t1' [Hsteps1 Hval1]].
          destruct Hsteps1. ∃ t1'. split; auto. split; auto. transitivity t'; auto.
          econstructor; eauto. reflexivity.
        + destruct (IHHsteps Hval) as [t1' [Hsteps1 Hval1]].
          destruct Hsteps1. ∃ t1'. split; auto. split; auto. transitivity t'; auto.
          econstructor; eauto. reflexivity.
        + left. ∃ t. split; split; auto. reflexivity.
        + right. ∃ t. split; split; auto. reflexivity.
        + destruct (IHHsteps Hval)
            as [[t'' [[Hstep1 Hval1] Heval2]] | [t'' [[Hstep1 Hval1] Heval2]]];
            [left | right].
          × ∃ t''. split; [split|]; auto. transitivity t'; auto.
            econstructor; eauto. reflexivity.
          × ∃ t''. split; [split|]; auto. transitivity t'; auto.
            econstructor; eauto. reflexivity.
    }
  - { intro H. destruct t; try contradiction.
      - destruct H as [t1' [[Hsteps1 Hval1] [Hsteps2 Hval2]]]. split; auto.
        transitivity (Let t1' t2); auto using steps_congruence_Let.
        econstructor; eauto.
      - subst. split; constructor.
      - destruct H as [t1' [t2' [[Hsteps1 Hval1] [[Hsteps2 Hval2] [Hsteps3 Hval3]]]]].
        split; auto.
        transitivity (App (Lam t1') t2); auto using steps_congruence_App_left.
        transitivity (App (Lam t1') t2'); auto using steps_congruence_App_right.
        transitivity (open t1' t2'); auto.
        econstructor; eauto. reflexivity.
      - subst. split.
        + reflexivity.
        + simpl. trivial.
      - destruct H as [t1' [t2' [[Hsteps1 Hval1] [[Hsteps2 Hval2] Heq]]]]. subst.
        split; simpl; auto.
        transitivity (Pair t1' t2);
          auto using steps_congruence_Pair_left, steps_congruence_Pair_right.
      - destruct H as [t2' [Hsteps2 [Hval1 Hval2]]]. split; auto.
        transitivity (Fst (Pair v t2')); auto using steps_congruence_Fst.
        econstructor; eauto. reflexivity.
      - destruct H as [t1' [Hsteps1 [Hval1 Hval2]]]. split; auto.
        transitivity (Snd (Pair t1' v)); auto using steps_congruence_Snd.
        econstructor; eauto. reflexivity.
      - destruct H as [t1' [[Hsteps1 Hval1] Heq]]. subst.
        split; auto using steps_congruence_InjL.
      - destruct H as [t1' [[Hsteps1 Hval1] Heq]]. subst.
        split; auto using steps_congruence_InjR.
      - destruct H
          as [[t' [[Hsteps1 Hval1] [Hsteps2 Hval2]]] | [t' [[Hsteps1 Hval1] [Hsteps2 Hval2]]]].
        + split; auto.
          transitivity (Match (InjL t') t2 t3); auto using steps_congruence_Match.
          econstructor; eauto.
        + split; auto.
          transitivity (Match (InjR t') t2 t3); auto using steps_congruence_Match.
          econstructor; eauto.
    }
Qed.

eval cannot produce a value from a term of the form App (Var x) t.
Lemma eval_App_Var_elim x t v:
  ∀ (P: Prop), eval (App (Var x) t) v → P.
Proof.
  intros P H. apply eval_iff in H.
  destruct H as [t1' [t2' [Heval1 [Heval2 Heval3]]]].
  apply eval_iff in Heval1.
  contradiction.
Qed.

eval cannot produce a value from a term of the form App (BVar n) t.
Lemma eval_App_BVar_elim n t v:
  ∀ (P: Prop), eval (App (BVar n) t) v → P.
Proof.
  intros P H. apply eval_iff in H.
  destruct H as [t1' [t2' [Heval1 [Heval2 Heval3]]]].
  apply eval_iff in Heval1.
  contradiction.
Qed.

eval cannot produce a value from a term of the form App Unit t.
Lemma eval_App_Unit_elim t v:
  ∀ (P: Prop), eval (App Unit t) v → P.
Proof.
  intros P H. apply eval_iff in H.
  destruct H as [t1' [t2' [Heval1 [Heval2 Heval3]]]].
  apply eval_iff in Heval1.
  discriminate.
Qed.

eval cannot produce a value from a term of the form App (Pair t1 t2) t.
Lemma eval_App_Pair_elim t1 t2 t3 v:
  ∀ (P: Prop), eval (App (Pair t1 t2) t3) v → P.
Proof.
  intros P H. apply eval_iff in H.
  destruct H as [t1' [t2' [Heval1 [Heval2 Heval3]]]].
  apply eval_iff in Heval1.
  destruct Heval1 as [t1'' [t2'' [Heval1' [Heval2' Heq]]]].
  discriminate.
Qed.

eval cannot produce a value from a term of the form App (InjL t1) t.
Lemma eval_App_InjL_elim t1 t2 v:
  ∀ (P: Prop), eval (App (InjL t1) t2) v → P.
Proof.
  intros P H. apply eval_iff in H.
  destruct H as [t1' [t2' [Heval1 [Heval2 Heval3]]]].
  apply eval_iff in Heval1.
  destruct Heval1 as [t1'' [Heval1' Heq]].
  discriminate.
Qed.

eval cannot produce a value from a term of the form App (InjR t1) t.
Lemma eval_App_InjR_elim t1 t2 v:
  ∀ (P: Prop), eval (App (InjR t1) t2) v → P.
Proof.
  intros P H. apply eval_iff in H.
  destruct H as [t1' [t2' [Heval1 [Heval2 Heval3]]]].
  apply eval_iff in Heval1.
  destruct Heval1 as [t1'' [Heval1' Heq]].
  discriminate.
Qed.

eval cannot produce a value from a term of the form Fst (Var x).
Lemma eval_Fst_Var_elim x v:
  ∀ (P: Prop), eval (Fst (Var x)) v → P.
Proof.
  intros P H. apply eval_iff in H.
  destruct H as [t' Heval'].
  apply eval_iff in Heval'.
  contradiction.
Qed.

eval cannot produce a value from a term of the form Fst (BVar n).
Lemma eval_Fst_BVar_elim n v:
  ∀ (P: Prop), eval (Fst (BVar n)) v → P.
Proof.
  intros P H. apply eval_iff in H.
  destruct H as [t' Heval'].
  apply eval_iff in Heval'.
  contradiction.
Qed.

eval cannot produce a value from a term of the form Fst (Lam t).
Lemma eval_Fst_Lam_elim t v:
  ∀ (P: Prop), eval (Fst (Lam t)) v → P.
Proof.
  intros P H. apply eval_iff in H.
  destruct H as [t' Heval'].
  apply eval_iff in Heval'.
  discriminate.
Qed.

eval cannot produce a value from a term of the form Fst (InjL t).
Lemma eval_Fst_InjL_elim t v:
  ∀ (P: Prop), eval (Fst (InjL t)) v → P.
Proof.
  intros P H. apply eval_iff in H.
  destruct H as [t' Heval'].
  apply eval_iff in Heval'.
  destruct Heval' as [t'' [Heval'' Heq]].
  discriminate.
Qed.

eval cannot produce a value from a term of the form Fst (InjR t).
Lemma eval_Fst_InjR_elim t v:
  ∀ (P: Prop), eval (Fst (InjR t)) v → P.
Proof.
  intros P H. apply eval_iff in H.
  destruct H as [t' Heval'].
  apply eval_iff in Heval'.
  destruct Heval' as [t'' [Heval'' Heq]].
  discriminate.
Qed.

eval cannot produce a value from a term of the form Snd (Var x).
Lemma eval_Snd_Var_elim x v:
  ∀ (P: Prop), eval (Snd (Var x)) v → P.
Proof.
  intros P H. apply eval_iff in H.
  destruct H as [t' Heval'].
  apply eval_iff in Heval'.
  contradiction.
Qed.

eval cannot produce a value from a term of the form Snd (BVar n).
Lemma eval_Snd_BVar_elim n v:
  ∀ (P: Prop), eval (Snd (BVar n)) v → P.
Proof.
  intros P H. apply eval_iff in H.
  destruct H as [t' Heval'].
  apply eval_iff in Heval'.
  contradiction.
Qed.

eval cannot produce a value from a term of the form Snd (Lam t).
Lemma eval_Snd_Lam_elim t v:
  ∀ (P: Prop), eval (Snd (Lam t)) v → P.
Proof.
  intros P H. apply eval_iff in H.
  destruct H as [t' Heval'].
  apply eval_iff in Heval'.
  discriminate.
Qed.

eval cannot produce a value from a term of the form Snd (InjL t).
Lemma eval_Snd_InjL_elim t v:
  ∀ (P: Prop), eval (Snd (InjL t)) v → P.
Proof.
  intros P H. apply eval_iff in H.
  destruct H as [t' Heval'].
  apply eval_iff in Heval'.
  destruct Heval' as [t'' [Heval'' Heq]].
  discriminate.
Qed.

eval cannot produce a value from a term of the form Snd (InjR t).
Lemma eval_Snd_InjR_elim t v:
  ∀ (P: Prop), eval (Snd (InjR t)) v → P.
Proof.
  intros P H. apply eval_iff in H.
  destruct H as [t' Heval'].
  apply eval_iff in Heval'.
  destruct Heval' as [t'' [Heval'' Heq]].
  discriminate.
Qed.

eval cannot produce a value from a term of the form Match (Var x) u1 u2.
Lemma eval_Match_Var_elim x t1 t2 v:
  ∀ (P: Prop), eval (Match (Var x) t1 t2) v → P.
Proof.
  intros P H. apply eval_iff in H.
  destruct H as [[t' [Heval1 Heval2]] | [t' [Heval1 Heval2]]];
    apply eval_iff in Heval1;
    contradiction.
Qed.

eval cannot produce a value from a term of the form Match (BVar n) u1 u2.
Lemma eval_Match_BVar_elim n t1 t2 v:
  ∀ (P: Prop), eval (Match (BVar n) t1 t2) v → P.
Proof.
  intros P H. apply eval_iff in H.
  destruct H as [[t' [Heval1 Heval2]] | [t' [Heval1 Heval2]]];
    apply eval_iff in Heval1;
    contradiction.
Qed.

eval cannot produce a value from a term of the form Match (Lam t) u1 u2.
Lemma eval_Match_Lam_elim t1 t2 t3 v:
  ∀ (P: Prop), eval (Match (Lam t1) t2 t3) v → P.
Proof.
  intros P H. apply eval_iff in H.
  destruct H as [[t' [Heval1 Heval2]] | [t' [Heval1 Heval2]]];
    apply eval_iff in Heval1;
    discriminate.
Qed.

eval cannot produce a value from a term of the form Match Unit u1 u2.
Lemma eval_Match_Unit_elim t1 t2 v:
  ∀ (P: Prop), eval (Match Unit t1 t2) v → P.
Proof.
  intros P H. apply eval_iff in H.
  destruct H as [[t' [Heval1 Heval2]] | [t' [Heval1 Heval2]]];
    apply eval_iff in Heval1;
    discriminate.
Qed.

eval cannot produce a value from a term of the form Match (Pair t1 t2) u1 u2.
Lemma eval_Match_Pair_elim t1 t2 t3 t4 v:
  ∀ (P: Prop), eval (Match (Pair t1 t2) t3 t4) v → P.
Proof.
  intros P H. apply eval_iff in H.
  destruct H as [[t' [Heval1 Heval2]] | [t' [Heval1 Heval2]]];
    apply eval_iff in Heval1;
    destruct Heval1 as [t1'' [t2'' [Heval1' [Heval2' Heq]]]];
    discriminate.
Qed.