Coral.SupportFacts: support of relational combinators and definition of well supported environments

Author: Benoît Montagu
Copyright © Inria 2020 CeCILL-B License
Synopsis: Support of relational combinators and definition of well supported environments.

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

Support of relational combinators


Lemma RelBot_supported_rel S:
  supported_rel S RelBot.
Proof.
  intros x y Hx Hy. apply RelBot_rel_equivariant.
Qed.

Hint Resolve RelBot_supported_rel: supported_rel.

Lemma RelBot_supported_vrel S:
  supported_vrel S RelBot.
Proof.
  intros x y Hx Hy. apply RelBot_vrel_equivariant.
Qed.

Hint Resolve RelBot_supported_vrel: supported_rel.

Lemma RelTopEnvVal_supported_rel S:
  supported_rel S RelTopEnvVal.
Proof.
  intros x y Hx Hy. apply RelTopEnvVal_rel_equivariant.
Qed.

Hint Resolve RelTopEnvVal_supported_rel: supported_rel.

Lemma RelTopVal_supported_vrel S:
  supported_vrel S RelTopVal.
Proof.
  intros x y Hx Hy. apply RelTopVal_vrel_equivariant.
Qed.

Hint Resolve RelTopVal_supported_vrel: supported_rel.

Lemma RelEqVal_supported_vrel S:
  supported_vrel S RelEqVal.
Proof.
  intros x y Hx Hy. apply RelEqVal_vrel_equivariant.
Qed.

Hint Resolve RelEqVal_supported_vrel: supported_rel.

Lemma RelInter_supported_rel S R1 R2:
  supported_rel S R1
  supported_rel S R2
  supported_rel S (RelInter R1 R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite RelInter_rel_equivariant.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve RelInter_supported_rel: supported_rel.

Lemma RelInter_supported_vrel S R1 R2:
  supported_vrel S R1
  supported_vrel S R2
  supported_vrel S (RelInter R1 R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite RelInter_vrel_equivariant.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve RelInter_supported_vrel: supported_rel.

Lemma RelUnion_supported_rel S R1 R2:
  supported_rel S R1
  supported_rel S R2
  supported_rel S (RelUnion R1 R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite RelUnion_rel_equivariant.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve RelUnion_supported_rel: supported_rel.

Lemma RelUnion_supported_vrel S R1 R2:
  supported_vrel S R1
  supported_vrel S R2
  supported_vrel S (RelUnion R1 R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite RelUnion_vrel_equivariant.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve RelUnion_supported_vrel: supported_rel.

Lemma RelCompose_supported_rel S R1 R2:
  supported_rel S R1
  supported_vrel S R2
  supported_rel S (RelCompose R1 R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite RelCompose_rel_equivariant.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve RelCompose_supported_rel: supported_rel.

Lemma RelCompose_RelInv_supported_rel S R1 R2:
  supported_rel S R1
  supported_rel S R2
  supported_vrel S (RelCompose (RelInv R1) R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite RelCompose_RelInv_rel_equivariant.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve RelCompose_RelInv_supported_rel: supported_rel.

Lemma RelCompose_supported_vrel S R1 R2:
  supported_vrel S R1
  supported_vrel S R2
  supported_vrel S (RelCompose R1 R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite RelCompose_vrel_equivariant.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve RelCompose_supported_vrel: supported_rel.

Lemma RelUnitR_supported_rel S:
  supported_rel S RelUnitR.
Proof.
  intros x y Hx Hy. apply RelUnitR_rel_equivariant.
Qed.

Hint Resolve RelUnitR_supported_rel: supported_rel.

Lemma RelPairR_supported_rel S R1 R2:
  supported_rel S R1
  supported_rel S R2
  supported_rel S (RelPairR R1 R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite RelPairR_rel_equivariant.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve RelPairR_supported_rel: supported_rel.

Lemma RelPairR_supported_vrel S R1 R2:
  supported_vrel S R1
  supported_vrel S R2
  supported_vrel S (RelPairR R1 R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite RelPairR_vrel_equivariant.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve RelPairR_supported_vrel: supported_rel.

Lemma RelPairL_supported_vrel S R1 R2:
  supported_vrel S R1
  supported_vrel S R2
  supported_vrel S (RelPairL R1 R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite RelPairL_vrel_equivariant.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve RelPairL_supported_vrel: supported_rel.

Lemma RelSumR_supported_rel S R1 R2:
  supported_rel S R1
  supported_rel S R2
  supported_rel S (RelSumR R1 R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite RelSumR_rel_equivariant.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve RelSumR_supported_rel: supported_rel.

Lemma RelSumR_supported_vrel S R1 R2:
  supported_vrel S R1
  supported_vrel S R2
  supported_vrel S (RelSumR R1 R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite RelSumR_vrel_equivariant.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve RelSumR_supported_vrel: supported_rel.

Lemma RelSumL_supported_vrel S R1 R2:
  supported_vrel S R1
  supported_vrel S R2
  supported_vrel S (RelSumL R1 R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite RelSumL_vrel_equivariant.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve RelSumL_supported_vrel: supported_rel.

Lemma RelGather_supported_rel S E:
  supported_env_rel S E
  supported_rel S (RelGather E).
Proof.
  intros HE x y Hx Hy.
  rewrite RelGather_rel_equivariant.
  rewrite (HE _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve RelGather_supported_rel: supported_rel.

Lemma RelSelf_supported_rel t:
  supported_rel (fv t) (RelSelf t).
Proof.
  intros x y Hx Hy.
  rewrite RelSelf_rel_equivariant.
  rewrite transp_term_fresh_eq; auto.
  reflexivity.
Qed.

Hint Resolve RelSelf_supported_rel: supported_rel.

Lemma FUN_supported_rel S R1 R2:
  supported_rel S R1
  supported_rel S R2
  supported_rel S (FUN S R1 R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite FUN_rel_equivariant.
  rewrite transp_atoms_fresh_eq; auto.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve FUN_supported_rel: supported_rel.

Lemma APP_supported_rel S R1 R2:
  supported_rel S R1
  supported_rel S R2
  supported_rel S (APP R1 R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite APP_rel_equivariant.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve APP_supported_rel: supported_rel.

Lemma depFUN_supported_rel S R1 R2:
  supported_rel S R1
  ( x y, x `notin` S y `notin` S
          pointwise RelEquiv
                    (fun vtransp_rel x y (R2 (transp_term x y v)))
                    R2)
  supported_rel S (depFUN S R1 R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite depFUN_rel_equivariant.
  rewrite transp_atoms_fresh_eq; auto.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.
Hint Resolve depFUN_supported_rel: supported_rel.

Lemma RelCompose_RelPush_supported_rel_strong S1 S2 S R1 x v R2:
  supported_rel S1 R1
  supported_rel S2 R2
  fv v [<=] S
  supported_rel (add x (S1 `union` S2 `union` S)) (RelCompose (RelPush R1 x v) R2).
Proof.
  intros Hsupp1 Hsupp2 Hfv.
  intros x1 x2 Hx1 Hx2. intros e t; split; intros [e' [[Heq H1] H2]]; subst.
  - rewrite <- (Hsupp1 x1 x2) in H1; auto.
    simpl in H1. rewrite transp_env_term_involution in H1.
    rewrite transp_term_fresh_eq in H1; [ | fsetdec | fsetdec ].
    rewrite <- (Hsupp2 x1 x2) in H2; auto.
    simpl in H2. rewrite transp_term_involution in H2.
    simpl_env in H2. rewrite transp_env_term_app in H2.
    rewrite transp_env_term_one in H2.
    rewrite transp_atom_other in H2; auto.
    rewrite transp_env_term_involution in H2.
    rewrite transp_term_fresh_eq in H2; [ | fsetdec | fsetdec ].
     (x ¬ v ++ e). split; [ split; [ reflexivity | assumption ] | assumption ].
  - rewrite <- (Hsupp1 x1 x2) in H1; auto.
    simpl in H1.
    rewrite transp_term_fresh_eq in H1; [ | fsetdec | fsetdec ].
    rewrite <- (Hsupp2 x1 x2) in H2; auto.
    simpl in H2.
    simpl_env in H2. rewrite transp_env_term_app in H2.
    rewrite transp_env_term_one in H2.
    rewrite transp_atom_other in H2; auto.
    rewrite (transp_term_fresh_eq x1 x2 v) in H2; [ | fsetdec | fsetdec ].
    simpl.
     (x ¬ v ++ transp_env_term x1 x2 e). split; [ split; [ reflexivity | assumption ] | assumption ].
Qed.

Lemma RelCompose_RelPush_supported_rel S R1 x v R2:
  supported_rel S R1
  supported_rel (add x S) R2
  fv v [<=] empty
  supported_rel (add x S) (RelCompose (RelPush R1 x v) R2).
Proof.
  intros Hsupp1 Hsupp2 Hfv.
  apply (supported_rel_subset (add x (S `union` (add x S) `union` empty))).
  - fsetdec.
  - apply RelCompose_RelPush_supported_rel_strong; assumption.
Qed.
Hint Resolve RelCompose_RelPush_supported_rel: supported_rel.

Lemma RelLet_strong_supported_rel S R1 R2:
  supported_family_rel S R1
  supported_rel S R2
  supported_rel S (RelLet_strong S R1 R2).
Proof.
  intros H1 H2 x y Hx Hy.
  rewrite RelLet_strong_rel_equivariant.
  rewrite transp_atoms_fresh_eq; auto.
  rewrite (H1 _ _ Hx Hy).
  rewrite (H2 _ _ Hx Hy).
  reflexivity.
Qed.

Hint Resolve RelLet_strong_supported_rel: supported_rel.

Well supported environments


Fixpoint well_supported_env (E: env (rel (env term) term)) : Prop :=
  match E with
  | nilTrue
  | (x, R) :: Esupported_rel (dom E) R well_supported_env E
  end.

Add Parametric Morphism: well_supported_env
    with signature env_rel_equiv ==> iff
      as well_supported_env_morphism_equiv.
Proof.
  intros E1 E2 HE. revert E2 HE.
  env induction E1; intros [| [y Ry] E2] HE; simpl in *; try tauto.
  destruct HE as [Heq [H HE]]. subst.
  rewrite H.
  rewrite HE at 1.
  rewrite IHE1; eauto.
  reflexivity.
Qed.

Lemma well_supported_env_equivariant x y E :
  well_supported_env (transp_env_rel x y E) well_supported_env E.
Proof.
  env induction E; simpl.
  - reflexivity.
  - rewrite IHE.
    rewrite <- (supported_rel_equivariant x y (dom xs) a).
    rewrite dom_equivariant_rel.
    reflexivity.
Qed.

Lemma well_supported_env_get E x R:
  well_supported_env E
  get x E = Some R
  supported_rel (dom E) R.
Proof.
  intros Hwf Hget. revert x R Hget.
  env induction E; intros; simpl in *; try discriminate.
  destruct Hwf as [Hsupp Hwf].
  apply (supported_rel_subset (dom xs)); [fsetdec|].
  destruct (x0 == x); subst; eauto.
  inversion Hget; subst. assumption.
Qed.

Lemma well_supported_env_weaken E:
  well_supported_env E
  supported_env_rel (dom E) E.
Proof.
  intro H. env induction E; simpl in ×.
  - intros x R Hx HR. simpl. trivial.
  - destruct H as [Hsupp H].
    apply supported_env_rel_cons. split; [| split]; auto.
    + apply (supported_rel_subset (dom xs)); [fsetdec|]. assumption.
    + apply (supported_env_rel_subset (dom xs)); [fsetdec|]. auto.
Qed.
Hint Resolve well_supported_env_weaken : core.