Coral.StepsFacts: facts about the steps relation

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

Require Import Infrastructure.
Import Notations.

step produces locally-closed terms from a locally-closed term.
Lemma step_lc t1 t2:
  step t1 t2 →
  lc t1 →
  lc t2.
Proof.
  intros H Hlc. induction H; inversion Hlc; subst; auto with lngen.
  - inversion H2; subst; auto with lngen.
  - inversion H2; subst; auto with lngen.
  - inversion H3; subst; auto with lngen.
  - inversion H3; subst; auto with lngen.
Qed.

steps produces locally-closed terms from a locally-closed term.
Lemma steps_lc t1 t2:
  steps t1 t2 →
  lc t1 →
  lc t2.
Proof.
  intros H Hlc. induction H; eauto using step_lc.
Qed.

step produces terms with less free variables than its input.
Lemma step_fv t1 t2:
  step t1 t2 →
  fv t2 [<=] fv t1.
Proof.
  intro H. induction H; simpl; auto with lngen.
  - rewrite fv_open_upper. fsetdec.
  - rewrite fv_open_upper. fsetdec.
  - rewrite fv_open_upper. fsetdec.
Qed.

steps produces terms with less free variables than its input.
Lemma steps_fv t1 t2:
  steps t1 t2 →
  fv t2 [<=] fv t1.
Proof.
  intro H. induction H.
  - reflexivity.
  - rewrite IHclos_refl_trans_1n. auto using step_fv.
Qed.

A value cannot take a step.
Lemma is_value_normal t:
  is_value t →
  ∀ t', ¬ step t t'.
Proof.
  induction t; simpl; intros H t' Hstep; try contradiction;
    inversion Hstep; subst; intuition eauto.
Qed.

Require Import Relations.Relation_Operators.
Require Import Relations.Operators_Properties.

steps is a reflexive relation.
Lemma steps_refl t: steps t t.
Proof.
  constructor.
Qed.

steps is a transitive relation.
Lemma steps_trans t1 t2 t3:
  steps t1 t2 →
  steps t2 t3 →
  steps t1 t3.
Proof.
  intros H12 H23.
  apply clos_rt_rt1n_iff.
  apply clos_rt_rt1n_iff in H12.
  apply clos_rt_rt1n_iff in H23.
  eapply Relations.Relation_Operators.rt_trans; eauto.
Qed.

Add Parametric Relation: term steps
    reflexivity proved by steps_refl
    transitivity proved by steps_trans
      as steps_rel.

steps is a congruence for the LHS of Let.
Lemma steps_congruence_Let t1 t1' t2:
  steps t1 t1' →
  steps (Let t1 t2) (Let t1' t2).
Proof.
  intro H. induction H.
  - reflexivity.
  - econstructor; eauto.
Qed.

steps is a congruence for the LHS of App.
Lemma steps_congruence_App_left t1 t1' t2:
  steps t1 t1' →
  steps (App t1 t2) (App t1' t2).
Proof.
  intro H. induction H.
  - reflexivity.
  - econstructor; eauto.
Qed.

steps is a congruence for the RHS of App when its LHS is a value.
Lemma steps_congruence_App_right t1 t2 t2':
  is_value t1 →
  steps t2 t2' →
  steps (App t1 t2) (App t1 t2').
Proof.
  intros Hval H. induction H.
  - reflexivity.
  - econstructor; eauto.
Qed.

steps is a congruence for the LHS of Pair.
Lemma steps_congruence_Pair_left t1 t1' t2:
  steps t1 t1' →
  steps (Pair t1 t2) (Pair t1' t2).
Proof.
  intro H. induction H.
  - reflexivity.
  - econstructor; eauto.
Qed.

steps is a congruence for the RHS of Pair when its LHS is a value.
Lemma steps_congruence_Pair_right t1 t2 t2':
  is_value t1 →
  steps t2 t2' →
  steps (Pair t1 t2) (Pair t1 t2').
Proof.
  intros Hval H. induction H.
  - reflexivity.
  - econstructor; eauto.
Qed.

steps is a congruence for Fst.
Lemma steps_congruence_Fst t t':
  steps t t' →
  steps (Fst t) (Fst t').
Proof.
  intro H. induction H.
  - reflexivity.
  - econstructor; eauto.
Qed.

steps is a congruence for Snd.
Lemma steps_congruence_Snd t t':
  steps t t' →
  steps (Snd t) (Snd t').
Proof.
  intro H. induction H.
  - reflexivity.
  - econstructor; eauto.
Qed.

steps is a congruence for InjL.
Lemma steps_congruence_InjL t t':
  steps t t' →
  steps (InjL t) (InjL t').
Proof.
  intro H. induction H.
  - reflexivity.
  - econstructor; eauto.
Qed.

steps is a congruence for InjR.
Lemma steps_congruence_InjR t t':
  steps t t' →
  steps (InjR t) (InjR t').
Proof.
  intro H. induction H.
  - reflexivity.
  - econstructor; eauto.
Qed.

steps is a congruence for the first argument of Match.
Lemma steps_congruence_Match t t' t1 t2:
  steps t t' →
  steps (Match t t1 t2) (Match t' t1 t2).
Proof.
  intro H. induction H.
  - reflexivity.
  - econstructor; eauto.
Qed.