Coral.RelWf: wellformed relations

Author: Benoît Montagu
Copyright © Inria 2020 CeCILL-B License
Synopsis: Wellformed relations.

Require Import Infrastructure.
Require Import Rel.
Require Import Transp.
Require Import RelGood.
Require Import RelStable.
Require Import EquivarianceFacts.
Require Import SupportFacts.
Require Import Env.
Require Import RelExtra.

Wellformed relations

A relation is wellformed for a finite set of atoms S if it is a good relation, it is stable, and it is supported by S. This is Definition 3.3 of the ICFP'20 paper.
Definition wf_rel S R : Prop :=
  good_rel R ∧
  stable_rel R ∧
  supported_rel S R.

Lemma wf_rel_good S R:
  wf_rel S R →
  good_rel R.
Proof.
  intros [? [? ?]]. assumption.
Qed.
Hint Resolve wf_rel_good : core.

Lemma wf_rel_stable S R:
  wf_rel S R →
  stable_rel R.
Proof.
  intros [? [? ?]]. assumption.
Qed.
Hint Resolve wf_rel_stable : core.

Lemma wf_rel_supported S R:
  wf_rel S R →
  supported_rel S R.
Proof.
  intros [? [? ?]]. assumption.
Qed.
Hint Resolve wf_rel_supported : core.

A value relation is wellformed for a finite set of atoms S if it is a good relation on values and if it is supported by S.
Definition wf_vrel S R : Prop :=
  good_vrel R ∧
  supported_vrel S R.

wf_rel is covariant in its set of atoms argument.
Lemma wf_rel_subset S1 S2 R:
  S1 [<=] S2 →
  wf_rel S1 R →
  wf_rel S2 R.
Proof.
  intros HS [? [? HR]]. split; [| split]; auto.
  eapply supported_rel_subset; eauto.
Qed.

wf_rel is equivariant.
Lemma wf_rel_equivariant x y S R :
  wf_rel S R ↔ wf_rel (transp_atoms x y S) (transp_rel x y R).
Proof.
  unfold wf_rel.
  rewrite <- good_rel_equivariant.
  rewrite <- stable_equivariant.
  rewrite supported_rel_equivariant.
  reflexivity.
Qed.

Wellformed environments of relations

An environment of relations is wellformed if its relations are good and stable, and if the environment is well supported in the sense of well_supported_env. This is definition 4.1 of the ICFP'20 paper, without the unicity of bindings, that we have chosen to add as hypothesis of lemmas only when it is needed.
Definition wf_env_rel E : Prop :=
  all_env good_rel E ∧
  all_env stable_rel E ∧
  well_supported_env E.

Lemma wf_env_rel_equivariant x y E :
  wf_env_rel (transp_env_rel x y E) ↔ wf_env_rel E.
Proof.
  unfold wf_env_rel.
  rewrite (all_env_rel_equivariant good_rel);
    [| solve [ intros; symmetry; apply good_rel_equivariant ] ].
  rewrite (all_env_rel_equivariant stable_rel);
    [| solve [ intros; symmetry; apply stable_equivariant ] ].
  rewrite well_supported_env_equivariant.
  reflexivity.
Qed.

Add Parametric Morphism: wf_env_rel
    with signature env_rel_equiv ==> iff
      as wf_env_rel_morphism_equiv.
Proof.
  intros E1 E2 Hequiv. unfold wf_env_rel.
  rewrite (well_supported_env_morphism_equiv _ _ Hequiv).
  erewrite (all_env_morphism_env_rel_equiv _ _ _ good_rel_morphism_equiv _ _ Hequiv).
  erewrite (all_env_morphism_env_rel_equiv _ _ _ stable_morphism_equiv _ _ Hequiv).
  reflexivity.
Qed.

Lemma wf_env_rel_good E:
  wf_env_rel E →
  all_env good_rel E.
Proof.
  intros [? [? ?]]. assumption.
Qed.
Hint Resolve wf_env_rel_good : core.

Lemma wf_env_rel_stable E:
  wf_env_rel E →
  all_env stable_rel E.
Proof.
  intros [? [? ?]]. assumption.
Qed.
Hint Resolve wf_env_rel_stable : core.

Lemma wf_env_rel_supported E:
  wf_env_rel E →
  well_supported_env E.
Proof.
  intros [? [? ?]]. assumption.
Qed.
Hint Resolve wf_env_rel_supported : core.

The empty environment is wellformed.
Lemma wf_env_rel_nil :
  wf_env_rel nil.
Proof.
  split; [| split]; simpl; auto.
Qed.
Hint Resolve wf_env_rel_nil: wf_rel.

If R is a relation that is wellformed for dom E and if E is a wellformed environment, then x ¬ R ++ E is a wellformed environment.
Lemma wf_env_rel_cons x R E :
  wf_rel (dom E) R →
  wf_env_rel E →
  wf_env_rel (x ¬ R ++ E).
Proof.
  intros [? [? ?]] [? [? ?]].
  split; [| split]; simpl; auto.
Qed.
Hint Resolve wf_env_rel_cons: wf_rel.

If E is a wellformed environment, then any relation in E is wellformed in dom E. This is Lemma 4.2 of the ICFP'20 paper.
Lemma wf_env_rel_get E x R:
  wf_env_rel E →
  get x E = Some R →
  wf_rel (dom E) R.
Proof.
  intros [Hgood [Hstable Hsupp]] Hget.
  split; [| split ].
  - eapply all_env_get; eauto.
  - eapply all_env_get; eauto.
  - eapply well_supported_env_get; eauto.
Qed.

Add Parametric Morphism: wf_rel
    with signature AtomSetImpl.Equal ==> (@RelEquiv (env term) term) ==> iff
      as wf_morphism_equiv.
Proof.
  intros S1 S2 HS R1 R2 HR.
  split; intros [? [? ?]]; (split; [| split ]);
    try solve [ rewrite <- HR; assumption
              | rewrite HR; assumption
              | rewrite <- HS; rewrite <- HR; assumption
              | rewrite HS; rewrite HR; assumption
              ].
Qed.

Wellformedness of combinators


Lemma wf_rel_RelBot S: wf_rel S RelBot.
Proof.
  split; [| split];
    auto with good_rel stable_rel supported_rel.
Qed.
Hint Resolve wf_rel_RelBot: wf_rel.

Lemma wf_vrel_RelBot S: wf_vrel S RelBot.
Proof.
  split; auto with good_rel supported_rel.
Qed.
Hint Resolve wf_vrel_RelBot: wf_rel.

Lemma wf_vrel_RelEqVal S: wf_vrel S RelEqVal.
Proof.
  split; auto with good_rel supported_rel.
Qed.
Hint Resolve wf_vrel_RelEqVal: wf_rel.

Lemma wf_rel_RelTopEnvVal S: wf_rel S RelTopEnvVal.
Proof.
  split; [| split];
    auto with good_rel stable_rel supported_rel.
Qed.
Hint Resolve wf_rel_RelTopEnvVal: wf_rel.

Lemma wf_vrel_RelTopVal S: wf_vrel S RelTopVal.
Proof.
  split; auto with good_rel supported_rel.
Qed.
Hint Resolve wf_vrel_RelTopVal: wf_rel.

Lemma wf_rel_RelInter S R1 R2:
  wf_rel S R1 →
  wf_rel S R2 →
  wf_rel S (RelInter R1 R2).
Proof.
  intros [? [? ?]] [? [? ?]].
  split; [| split]; auto with good_rel stable_rel supported_rel.
Qed.
Hint Resolve wf_rel_RelInter: wf_rel.

Lemma wf_vrel_RelInter S R1 R2:
  wf_vrel S R1 →
  wf_vrel S R2 →
  wf_vrel S (RelInter R1 R2).
Proof.
  intros [? ?] [? ?].
  split; auto with good_rel stable_rel supported_rel.
Qed.
Hint Resolve wf_vrel_RelInter: wf_rel.

Lemma wf_rel_RelUnion S R1 R2:
  wf_rel S R1 →
  wf_rel S R2 →
  wf_rel S (RelUnion R1 R2).
Proof.
  intros [? [? ?]] [? [? ?]].
  split; [| split]; auto with good_rel stable_rel supported_rel.
Qed.
Hint Resolve wf_rel_RelUnion: wf_rel.

Lemma wf_vrel_RelUnion S R1 R2:
  wf_vrel S R1 →
  wf_vrel S R2 →
  wf_vrel S (RelUnion R1 R2).
Proof.
  intros [? ?] [? ?].
  split; auto with good_rel stable_rel supported_rel.
Qed.
Hint Resolve wf_vrel_RelUnion: wf_rel.

This is the wellformedness of composition that is mentioned on page 11 of the ICFP'20 paper.
Lemma wf_rel_RelCompose S R1 R2:
  wf_rel S R1 →
  wf_vrel S R2 →
  wf_rel S (RelCompose R1 R2).
Proof.
  intros [? [? ?]] [? ?].
  split; [| split]; auto with good_rel stable_rel supported_rel.
Qed.
Hint Resolve wf_rel_RelCompose: wf_rel.

Lemma wf_vrel_RelCompose S R1 R2:
  wf_vrel S R1 →
  wf_vrel S R2 →
  wf_vrel S (RelCompose R1 R2).
Proof.
  intros [? ?] [? ?].
  split; auto with good_rel supported_rel.
Qed.
Hint Resolve wf_vrel_RelCompose: wf_rel.

Lemma wf_rel_RelUnitR S:
  wf_rel S RelUnitR.
Proof.
  split; [| split]; auto with good_rel stable_rel supported_rel.
Qed.
Hint Resolve wf_rel_RelUnitR: wf_rel.

Lemma wf_rel_RelPairR S R1 R2:
  wf_rel S R1 →
  wf_rel S R2 →
  wf_rel S (RelPairR R1 R2).
Proof.
  intros [? [? ?]] [? [? ?]].
  split; [| split]; auto with good_rel stable_rel supported_rel.
Qed.
Hint Resolve wf_rel_RelPairR: wf_rel.

Lemma wf_vrel_RelPairR S R1 R2:
  wf_vrel S R1 →
  wf_vrel S R2 →
  wf_vrel S (RelPairR R1 R2).
Proof.
  intros [? ?] [? ?].
  split; auto with good_rel supported_rel.
Qed.
Hint Resolve wf_vrel_RelPairR: wf_rel.

Lemma wf_vrel_RelPairL S R1 R2:
  wf_vrel S R1 →
  wf_vrel S R2 →
  wf_vrel S (RelPairL R1 R2).
Proof.
  intros [? ?] [? ?].
  split; auto with good_rel supported_rel.
Qed.
Hint Resolve wf_vrel_RelPairL: wf_rel.

Lemma wf_rel_RelSumR S R1 R2:
  wf_rel S R1 →
  wf_rel S R2 →
  wf_rel S (RelSumR R1 R2).
Proof.
  intros [? [? ?]] [? [? ?]].
  split; auto with good_rel stable_rel supported_rel.
Qed.
Hint Resolve wf_rel_RelSumR: wf_rel.

Lemma wf_vrel_RelSumR S R1 R2:
  wf_vrel S R1 →
  wf_vrel S R2 →
  wf_vrel S (RelSumR R1 R2).
Proof.
  intros [? ?] [? ?].
  split; auto with good_rel supported_rel.
Qed.
Hint Resolve wf_vrel_RelSumR: wf_rel.

Lemma wf_vrel_RelSumL S R1 R2:
  wf_vrel S R1 →
  wf_vrel S R2 →
  wf_vrel S (RelSumL R1 R2).
Proof.
  intros [? ?] [? ?].
  split; auto with good_rel supported_rel.
Qed.
Hint Resolve wf_vrel_RelSumL: wf_rel.

Lemma wf_rel_RelGather S E:
  dom E [<=] S →
  wf_env_rel E →
  wf_rel S (RelGather E).
Proof.
  intros HS [? [? ?]].
  split; [| split]; auto with good_rel stable_rel supported_rel.
  eapply supported_rel_subset; eauto with supported_rel.
Qed.
Hint Resolve wf_rel_RelGather: wf_rel.

This is the wellformedness of "Self" that is mentioned on page 11 of the ICFP'20 paper.
Lemma wf_rel_RelSelf S t:
  fv t [<=] S →
  wf_rel S (RelSelf t).
Proof.
  intro H.
  split; [| split]; auto with good_rel stable_rel.
  eapply supported_rel_subset; eauto with supported_rel.
Qed.
Hint Resolve wf_rel_RelSelf: wf_rel.

Lemma wf_rel_FUN S R1 R2:
  wf_rel S R1 →
  wf_rel S R2 →
  wf_rel S (FUN S R1 R2).
Proof.
  intros [? [? ?]] [? [? ?]].
  split; [| split]; auto with good_rel stable_rel supported_rel.
Qed.
Hint Resolve wf_rel_FUN: wf_rel.

Lemma wf_rel_APP S R1 R2:
  wf_rel S R1 →
  wf_rel S R2 →
  wf_rel S (APP R1 R2).
Proof.
  intros [? [? ?]] [? [? ?]].
  split; [| split]; auto with good_rel stable_rel supported_rel.
Qed.
Hint Resolve wf_rel_APP: wf_rel.

Lemma wf_rel_RelLet_strong S R1 R2:
  supported_family_rel S R1 →
  (∀ x, x `notin` S → good_rel (R1 x)) →
  (∀ x, x `notin` S → stable_rel (R1 x)) →
  wf_rel S R2 →
  wf_rel S (RelLet_strong S R1 R2).
Proof.
  intros ? ? ? [? [? ?]].
  split; [| split]; auto with good_rel stable_rel supported_rel.
Qed.
Hint Resolve wf_rel_RelLet_strong: wf_rel.

This is the wellformedness of Let-bindings that is mentioned on page 11 of the ICFP'20 paper.
Lemma wf_rel_RelLet S x R1 R2 :
  x `notin` S →
  wf_rel S R1 →
  wf_rel (add x S) R2 →
  wf_rel S (RelLet S x R1 R2).
Proof.
  intros ? [? [? ?]] [? [? ?]].
  split; [| split]; auto with good_rel stable_rel supported_rel.
Qed.
Hint Resolve wf_rel_RelLet : wf_rel.

Lemma wf_rel_RelLam S x R1 R2 :
  wf_rel S R1 →
  wf_rel (add x S) R2 →
  wf_rel S (RelLam S x R1 R2).
Proof.
  intros [? [? ?]] [? [? ?]].
  split; [| split]; auto with good_rel stable_rel supported_rel.
Qed.
Hint Resolve wf_rel_RelLam : wf_rel.