Coral.OkEnv: denotation of an environment of relations as a set of substitutions

Author: Benoît Montagu
Copyright © Inria 2020 CeCILL-B License
Synopsis: Definition and properties of ok_env, that defines the substitutions that are accepted by an environment of relations.

Require Import Infrastructure.
Require Import Env.
Require Import SubstEnv.
Require Import Rel.
Require Import Transp.
Require Import RelStable.
Require Import EquivarianceFacts.

ok_env E is the set of substitutions that are accepted by the environment of relations E. This is Definition 4.4 of the ICFP'20 paper.
Inductive ok_env: env (rel (env term) term) → env term → Prop :=
| ok_envNil: ok_env nil nil
| ok_envCons: ∀ E e x (R: rel (env term) term) v,
    (get x e = None ∨ get x e = Some v) →
    ok_env E e →
    in_rel R e v →
    ok_env (x ¬ R ++ E) (x ¬ v ++ e)
| ok_envLeq: ∀ E e e',
    ok_env E e →
    leq_env e e' →
    all_env good_value e →
    ok_env E e'
.

ok_env E is closed under extensions of substitutions.
Lemma ok_env_leq_env (E: env (rel (env term) term)) (e e': env term):
  all_env good_value e →
  ok_env E e →
  leq_env e e' →
  ok_env E e'.
Proof.
  intros. eapply ok_envLeq; eauto.
Qed.

ok_env is covariant for env_rel_incl
Lemma ok_env_env_rel_incl E E' e:
  env_rel_incl E E' →
  ok_env E e →
  ok_env E' e.
Proof.
  intros Hincl Hok.
  revert E' Hincl.
  induction Hok; intros.
  - destruct E'; simpl in Hincl; try contradiction.
    apply ok_envNil.
  - destruct E' as [| [y R']]; simpl in Hincl; try contradiction.
    destruct Hincl as [Heq [HinclR HinclE]]. subst.
    apply ok_envCons; auto.
  - eapply ok_envLeq; eauto.
Qed.

Add Parametric Morphism: ok_env
    with signature env_rel_equiv ==> eq ==> iff
      as ok_env_morphism_equiv.
Proof.
  intros E1 E2 HE e.
  split; [| symmetry in HE];
    intro H; eapply ok_env_env_rel_incl; eauto using env_rel_incl_refl_equiv.
Qed.

If ok_env E e, then any binding that is absent from e must also be absent from E.
Lemma ok_env_get_None (e: env term) (E: env (rel (env term) term)) x:
  ok_env E e →
  get x e = None → get x E = None.
Proof.
  intro H. revert x. induction H; intros y Hy.
  - auto.
  - destruct (y == x); subst.
    + rewrite get_update_this in Hy. discriminate.
    + rewrite get_update_other; auto.
      rewrite get_update_other in Hy; auto.
  - eapply leq_env_get_None in Hy; eauto.
Qed.

Assume that E contains only stable relations and that e contains only good values. If ok_env E e, then e and get x e are related by get x E. This is Lemma 4.6 of the ICFP'20 paper.
Lemma ok_env_get (e: env term) (E: env (rel (env term) term)) :
  all_env stable_rel E →
  all_env good_value e →
  ok_env E e →
  ∀ x v R,
    get x e = Some v →
    get x E = Some R →
    in_rel R e v.
Proof.
  intros Hwf Hgood H. induction H; intros y vy r Hv HR.
  - simpl in HR. discriminate.
  - assert (stable_rel r) by (eapply all_env_get; eauto).
    destruct (y == x); subst.
    + rewrite get_update_this in Hv. inversion Hv; subst. clear Hv.
      rewrite get_update_this in HR. inversion HR; subst. clear HR.
      eapply Hwf; eauto using leq_env_update.
      destruct H; auto using leq_env_update, leq_env_update2.
    + rewrite get_update_other in Hv; auto.
      rewrite get_update_other in HR; auto.
      apply H2 with (e := e); auto.
      × { eapply IHok_env; eauto.
          - inversion Hwf; subst; auto.
          - simpl in Hgood. tauto.
        }
      × destruct H; auto using leq_env_update, leq_env_update2.
  - assert (stable_rel r) by (eapply all_env_get; eauto).
    assert (get y e = Some vy).
    { case_eq (get y e); intros; auto.
      - eapply H0 in H3; eauto. congruence.
      - eapply ok_env_get_None in H3; eauto. congruence.
    }
    eauto.
Qed.

ok_env is preserved by the addition of a new binding.
Lemma ok_env_update E e x v R:
  ok_env E e →
  get x e = None →
  in_rel R e v →
  ok_env (x ¬ R ++ E) (x ¬ v ++ e).
Proof.
  intros. constructor; auto.
Qed.

The substutions in ok_env E have domains that are larger than E's domain. This is Lemma 4.5 of the ICFP'20 paper.
Lemma ok_env_dom E e:
  ok_env E e →
  dom E [<=] dom e.
Proof.
  intro H. induction H; simpl.
  - fsetdec.
  - fsetdec.
  - apply leq_env_dom in H0. fsetdec.
Qed.

There are more substitution in ok_env (remove_all x E) than in ok_env E.
Lemma ok_env_remove_all x E e:
  all_env good_value e →
  ok_env E e →
  ok_env (remove_all x E) e.
Proof.
  intros Hgood H. induction H; simpl.
  - constructor.
  - simpl in Hgood. destruct Hgood as [Hvgood Hgood].
    destruct (x0 == x); subst; auto.
    + apply ok_envLeq with (e := e); auto.
      simpl_env. destruct H; auto using leq_env_update, leq_env_update2.
    + constructor; auto.
  - econstructor; eauto.
Qed.

Equivariance for ok_env.
Lemma ok_env_equivariant x y E e:
  ok_env E e ↔ ok_env (transp_env_rel x y E) (transp_env_term x y e).
Proof.
  revert E e.
  assert (∀ E e, ok_env E e → ok_env (transp_env_rel x y E) (transp_env_term x y e)).
  { intros E e H.
    induction H; simpl.
    - constructor.
    - rewrite (get_transp_env_term_None_equivariant x y) in H.
      rewrite (get_transp_env_term_Some_equivariant x y) in H.
      assert (in_rel (transp_rel x y R) (transp_env_term x y e) (transp_term x y v)).
      { simpl.
        rewrite transp_env_term_involution.
        rewrite transp_term_involution.
        assumption.
      }
      constructor; auto.
    - apply (leq_env_equivariant x y) in H0.
      apply (all_env_term_equivariant good_value good_value_equivariant x y) in H1.
      econstructor; eauto.
  }
  intros E e. split; intro H'; auto.
  apply H in H'.
  rewrite transp_env_rel_involution in H'.
  rewrite transp_env_term_involution in H'.
  assumption.
Qed.