Coral.Perm: permutations of names

Author: Benoît Montagu

Synopsis: Name permutations are lists of name transpositions. Permutations are useful to prove strong induction principles, for which the proofs need generalizations of transpositions as sequences of transpositions.

Require Import Infrastructure.
Import Notations.
Require Import Env.
Require Import Rel.
Require Import Transp.
Require Import EquivarianceFacts.
Require Import SupportFacts.
Require Import RelExtra.

Permutations are lists of pairs of atoms.

Definition perm := list (atom × atom).

Action of permutations on atoms

Definition perm_atom (pi: perm) (x: atom) : atom :=
  List.fold_left (fun acc p ⇒ match p with (x1, x2) ⇒ transp_atom x1 x2 acc end) pi x.

Lemma perm_atom_snoc pi x1 x2 x:
  perm_atom (pi ++ (x1 , x2 ) :: nil) x =
  transp_atom x1 x2 (perm_atom pi x).
Proof.
  apply List.fold_left_app.
Qed.

Action of permutations on sets of atoms

Definition perm_atoms (pi: perm) (S: atoms) : atoms :=
  List.fold_left (fun acc p ⇒ match p with (x1, x2) ⇒ transp_atoms x1 x2 acc end) pi S.

Add Parametric Morphism: perm_atoms
    with signature eq ==> AtomSetImpl.Equal ==> AtomSetImpl.Equal
      as perm_atom_morphism_equiv.
Proof.
  intro pi. env induction pi; intros S1 S2 Hequiv; simpl.
  - assumption.
  - apply IHpi. rewrite Hequiv. reflexivity.
Qed.

Lemma perm_Incl pi S1 S2:
  perm_atoms pi S1 [<=] perm_atoms pi S2 ↔ S1 [<=] S2.
Proof.
  revert S1 S2. env induction pi; intros; simpl.
  - reflexivity.
  - rewrite IHpi. symmetry. apply atoms_incl_equivariant.
Qed.

Lemma perm_add pi x S:
  perm_atoms pi (add x S) [=] add (perm_atom pi x) (perm_atoms pi S).
Proof.
  revert x S. env induction pi; intros; simpl.
  - reflexivity.
  - rewrite <- IHpi. rewrite add_equivariant. reflexivity.
Qed.

Lemma perm_in pi x S:
  perm_atom pi x `in ` perm_atoms pi S ↔ x `in ` S.
Proof.
  revert x S. env induction pi; intros; subst; simpl.
  - reflexivity.
  - rewrite IHpi. symmetry. apply in_equivariant.
Qed.

Lemma perm_notin pi x S:
  perm_atom pi x `notin ` perm_atoms pi S ↔ x `notin ` S.
Proof.
  revert x S. env induction pi; intros; subst; simpl.
  - reflexivity.
  - rewrite IHpi. symmetry. apply notin_equivariant.
Qed.

Action of permutations on terms

Definition perm_term (pi: perm) (t: term) : term :=
  List.fold_left (fun acc p ⇒ match p with (x1, x2) ⇒ transp_term x1 x2 acc end) pi t.

Lemma perm_term_snoc pi x1 x2 t:
  perm_term (pi ++ (x1 , x2 ) :: nil) t =
  transp_term x1 x2 (perm_term pi t).
Proof.
  apply List.fold_left_app.
Qed.

Strong equivariance of term constructors

Lemma perm_Var pi x:
  perm_term pi (Var x) = Var (perm_atom pi x).
Proof.
  revert x. unfold perm_term. env induction pi; intros; simpl; auto.
Qed.

Lemma perm_Let pi t1 t2:
  perm_term pi (Let t1 t2) = Let (perm_term pi t1) (perm_term pi t2).
Proof.
  remember (Let t1 t2) as t. revert t t1 t2 Heqt.
  unfold perm_term. env induction pi; intros; subst; simpl; auto.
Qed.

Lemma perm_Lam pi t:
  perm_term pi (Lam t) = Lam (perm_term pi t).
Proof.
  remember (Lam t) as t'. revert t' t Heqt'.
  unfold perm_term. env induction pi; intros; subst; simpl; auto.
Qed.

Lemma perm_App pi t1 t2:
  perm_term pi (App t1 t2) = App (perm_term pi t1) (perm_term pi t2).
Proof.
  remember (App t1 t2) as t. revert t t1 t2 Heqt.
  unfold perm_term. env induction pi; intros; subst; simpl; auto.
Qed.

Lemma perm_Unit pi:
  perm_term pi Unit = Unit.
Proof.
  unfold perm_term. env induction pi; intros; subst; simpl; auto.
Qed.

Lemma perm_Pair pi t1 t2:
  perm_term pi (Pair t1 t2) = Pair (perm_term pi t1) (perm_term pi t2).
Proof.
  remember (Pair t1 t2) as t. revert t t1 t2 Heqt.
  unfold perm_term. env induction pi; intros; subst; simpl; auto.
Qed.

Lemma perm_Fst pi t:
  perm_term pi (Fst t) = Fst (perm_term pi t).
Proof.
  remember (Fst t) as t'. revert t' t Heqt'.
  unfold perm_term. env induction pi; intros; subst; simpl; auto.
Qed.

Lemma perm_Snd pi t:
  perm_term pi (Snd t) = Snd (perm_term pi t).
Proof.
  remember (Snd t) as t'. revert t' t Heqt'.
  unfold perm_term. env induction pi; intros; subst; simpl; auto.
Qed.

Lemma perm_InjL pi t:
  perm_term pi (InjL t) = InjL (perm_term pi t).
Proof.
  remember (InjL t) as t'. revert t' t Heqt'.
  unfold perm_term. env induction pi; intros; subst; simpl; auto.
Qed.

Lemma perm_InjR pi t:
  perm_term pi (InjR t) = InjR (perm_term pi t).
Proof.
  remember (InjR t) as t'. revert t' t Heqt'.
  unfold perm_term. env induction pi; intros; subst; simpl; auto.
Qed.

Lemma perm_Match pi t1 t2 t3:
  perm_term pi (Match t1 t2 t3) = Match (perm_term pi t1) (perm_term pi t2) (perm_term pi t3).
Proof.
  remember (Match t1 t2 t3) as t. revert t t1 t2 t3 Heqt.
  unfold perm_term. env induction pi; intros; subst; simpl; auto.
Qed.

Other strong equivariance for terms

Lemma perm_lc pi t:
  lc (perm_term pi t) ↔ lc t.
Proof.
  revert t. env induction pi; intros; simpl; auto.
  - reflexivity.
  - rewrite IHpi. apply lc_equivariant.
Qed.

Lemma perm_fv pi t:
  perm_atoms pi (fv t) [=] fv (perm_term pi t).
Proof.
  revert t. env induction pi; intros; simpl.
  - reflexivity.
  - rewrite fv_equivariant. auto.
Qed.

Lemma perm_close pi x t:
  perm_term pi (close x t) = close (perm_atom pi x) (perm_term pi t).
Proof.
  remember (close x t) as t'. revert t' x t Heqt'.
  unfold perm_term. env induction pi; intros; subst; simpl; auto.
  rewrite close_equivariant. auto.
Qed.

Action of permutations on binary relations on terms

Definition perm_vrel (pi: perm) (R: rel term term) : rel term term :=
  List.fold_left (fun acc p ⇒ match p with (x1, x2) ⇒ transp_vrel x1 x2 acc end) pi R.

Add Parametric Morphism: perm_vrel
    with signature eq ==> RelEquiv ==> RelEquiv
      as perm_vrel_morphism_equiv.
Proof.
  intro pi. env induction pi; intros R1 R2 Hequiv; simpl.
  - assumption.
  - apply IHpi. rewrite Hequiv. reflexivity.
Qed.

Action of permutations on relations over substitutions and terms

Definition perm_rel (pi: perm) (R: rel (env term) term) : rel (env term) term :=
  List.fold_left (fun acc p ⇒ match p with (x1, x2) ⇒ transp_rel x1 x2 acc end) pi R.

Add Parametric Morphism: perm_rel
    with signature eq ==> RelEquiv ==> RelEquiv
      as perm_rel_morphism_equiv.
Proof.
  intro pi. env induction pi; intros R1 R2 Hequiv; simpl.
  - assumption.
  - apply IHpi. rewrite Hequiv. reflexivity.
Qed.

Lemma perm_rel_snoc pi x1 x2 R:
  perm_rel (pi ++ (x1 , x2 ) :: nil) R =
  transp_rel x1 x2 (perm_rel pi R).
Proof.
  apply List.fold_left_app.
Qed.

Lemma perm_supported_rel pi S R:
  supported_rel (perm_atoms pi S) (perm_rel pi R) ↔ supported_rel S R.
Proof.
  revert S R. env induction pi; intros; subst; simpl.
  - reflexivity.
  - rewrite IHpi. apply supported_rel_equivariant.
Qed.

Action of permutations on environments of relations

Definition perm_env_rel (pi: perm) (e: env (rel (env term) term)) : env (rel (env term) term) :=
  List.fold_left (fun acc p ⇒ match p with (x1, x2) ⇒ transp_env_rel x1 x2 acc end) pi e.

Lemma perm_env_rel_snoc pi x1 x2 e:
  perm_env_rel (pi ++ (x1 , x2 ) :: nil) e =
  transp_env_rel x1 x2 (perm_env_rel pi e).
Proof.
  apply List.fold_left_app.
Qed.

Lemma perm_env_rel_app pi e1 e2:
  perm_env_rel pi (e1 ++ e2) = perm_env_rel pi e1 ++ perm_env_rel pi e2.
Proof.
  remember (e1 ++ e2) as e. revert e e1 e2 Heqe.
  env induction pi; intros; subst; simpl; auto.
  rewrite transp_env_rel_app. auto.
Qed.

Lemma perm_env_rel_one pi x R:
  perm_env_rel pi (x ¬ R) = perm_atom pi x ¬ perm_rel pi R.
Proof.
  remember (x ¬ R) as e. revert e x R Heqe.
  env induction pi; intros; subst; simpl; auto.
Qed.

Lemma perm_env_rel_nil pi:
  perm_env_rel pi nil = nil.
Proof.
  env induction pi; simpl; auto.
Qed.

Lemma perm_well_supported_env pi E:
  well_supported_env (perm_env_rel pi E) ↔ well_supported_env E.
Proof.
  revert E. env induction pi; intros; subst; simpl.
  - reflexivity.
  - rewrite IHpi. apply well_supported_env_equivariant.
Qed.

Lemma perm_dom pi e:
  perm_atoms pi (dom e) [=] dom (perm_env_rel pi e).
Proof.
  revert e.
  env induction pi; intros; subst; simpl.
  - reflexivity.
  - rewrite dom_equivariant_rel. apply IHpi.
Qed.

Strong equivariance results on relational combinators

Lemma perm_RelInter pi R1 R2:
  RelEquiv (perm_rel pi (RelInter R1 R2)) (RelInter (perm_rel pi R1) (perm_rel pi R2)).
Proof.
  remember (RelInter R1 R2) as R. revert R R1 R2 HeqR.
  env induction pi; intros; subst; simpl.
  - reflexivity.
  - rewrite RelInter_rel_equivariant. apply IHpi. reflexivity.
Qed.

Lemma perm_RelUnion pi R1 R2:
  RelEquiv (perm_rel pi (RelUnion R1 R2)) (RelUnion (perm_rel pi R1) (perm_rel pi R2)).
Proof.
  remember (RelUnion R1 R2) as R. revert R R1 R2 HeqR.
  env induction pi; intros; subst; simpl.
  - reflexivity.
  - rewrite RelUnion_rel_equivariant. apply IHpi. reflexivity.
Qed.

Lemma perm_RelBot pi:
  RelEquiv (perm_rel pi RelBot) RelBot.
Proof.
  env induction pi; intros; subst; simpl.
  - reflexivity.
  - rewrite RelBot_rel_equivariant. apply IHpi.
Qed.

Lemma perm_RelTopEnvVal pi:
  RelEquiv (perm_rel pi RelTopEnvVal) RelTopEnvVal.
Proof.
  env induction pi; intros; subst; simpl.
  - reflexivity.
  - rewrite RelTopEnvVal_rel_equivariant. apply IHpi.
Qed.

Lemma perm_RelSelf pi t:
  RelEquiv (perm_rel pi (RelSelf t)) (RelSelf (perm_term pi t)).
Proof.
  remember (RelSelf t) as R. revert R t HeqR.
  env induction pi; intros; subst; simpl.
  - reflexivity.
  - rewrite RelSelf_rel_equivariant. apply IHpi. reflexivity.
Qed.

Lemma perm_RelGather pi E:
  RelEquiv (perm_rel pi (RelGather E)) (RelGather (perm_env_rel pi E)).
Proof.
  remember (RelGather E) as R. revert R E HeqR.
  env induction pi; intros; subst; simpl.
  - reflexivity.
  - rewrite RelGather_rel_equivariant. apply IHpi. reflexivity.
Qed.

Lemma perm_RelLet pi S x R1 R2:
  RelEquiv (perm_rel pi (RelLet S x R1 R2))
           (RelLet (perm_atoms pi S) (perm_atom pi x) (perm_rel pi R1) (perm_rel pi R2)).
Proof.
  remember (RelLet S x R1 R2) as R. revert R S x R1 R2 HeqR.
  env induction pi; intros; subst; simpl.
  - reflexivity.
  - rewrite RelLet_rel_equivariant. apply IHpi. reflexivity.
Qed.

Lemma perm_RelLam pi S x R1 R2:
  RelEquiv (perm_rel pi (RelLam S x R1 R2))
           (RelLam (perm_atoms pi S) (perm_atom pi x) (perm_rel pi R1) (perm_rel pi R2)).
Proof.
  remember (RelLam S x R1 R2) as R. revert R S x R1 R2 HeqR.
  env induction pi; intros; subst; simpl.
  - reflexivity.
  - rewrite RelLam_rel_equivariant. apply IHpi. reflexivity.
Qed.

Lemma perm_APP pi R1 R2:
  RelEquiv (perm_rel pi (APP R1 R2))
           (APP (perm_rel pi R1) (perm_rel pi R2)).
Proof.
  remember (APP R1 R2) as R. revert R R1 R2 HeqR.
  env induction pi; intros; subst; simpl.
  - reflexivity.
  - rewrite APP_rel_equivariant. apply IHpi. reflexivity.
Qed.

Lemma perm_RelUnitR pi:
  RelEquiv (perm_rel pi RelUnitR) RelUnitR.
Proof.
  env induction pi; intros; subst; simpl.
  - reflexivity.
  - rewrite RelUnitR_rel_equivariant. apply IHpi.
Qed.

Lemma perm_RelPairR pi R1 R2:
  RelEquiv (perm_rel pi (RelPairR R1 R2))
           (RelPairR (perm_rel pi R1) (perm_rel pi R2)).
Proof.
  remember (RelPairR R1 R2) as R. revert R R1 R2 HeqR.
  env induction pi; intros; subst; simpl.
  - reflexivity.
  - rewrite RelPairR_rel_equivariant. apply IHpi. reflexivity.
Qed.

Lemma perm_RelSumR pi R1 R2:
  RelEquiv (perm_rel pi (RelSumR R1 R2))
           (RelSumR (perm_rel pi R1) (perm_rel pi R2)).
Proof.
  remember (RelSumR R1 R2) as R. revert R R1 R2 HeqR.
  env induction pi; intros; subst; simpl.
  - reflexivity.
  - rewrite RelSumR_rel_equivariant. apply IHpi. reflexivity.
Qed.

Lemma perm_RelCompose pi R1 R2:
  RelEquiv (perm_rel pi (RelCompose R1 R2))
           (RelCompose (perm_rel pi R1) (perm_vrel pi R2)).
Proof.
  remember (RelCompose R1 R2) as R. revert R R1 R2 HeqR.
  env induction pi; intros; subst; simpl.
  - reflexivity.
  - rewrite RelCompose_rel_equivariant. apply IHpi. reflexivity.
Qed.

Lemma perm_RelPairL pi R1 R2:
  RelEquiv (perm_vrel pi (RelPairL R1 R2))
           (RelPairL (perm_vrel pi R1) (perm_vrel pi R2)).
Proof.
  remember (RelPairL R1 R2) as R. revert R R1 R2 HeqR.
  env induction pi; intros; subst; simpl.
  - reflexivity.
  - rewrite RelPairL_vrel_equivariant. apply IHpi. reflexivity.
Qed.

Lemma perm_RelSumL pi R1 R2:
  RelEquiv (perm_vrel pi (RelSumL R1 R2))
           (RelSumL (perm_vrel pi R1) (perm_vrel pi R2)).
Proof.
  remember (RelSumL R1 R2) as R. revert R R1 R2 HeqR.
  env induction pi; intros; subst; simpl.
  - reflexivity.
  - rewrite RelSumL_vrel_equivariant. apply IHpi. reflexivity.
Qed.

Lemma perm_RelEqVal pi:
  RelEquiv (perm_vrel pi RelEqVal) RelEqVal.
Proof.
  env induction pi; intros; subst; simpl.
  - reflexivity.
  - rewrite RelEqVal_vrel_equivariant. apply IHpi.
Qed.

Lemma perm_RelTopVal pi:
  RelEquiv (perm_vrel pi RelTopVal) RelTopVal.
Proof.
  env induction pi; intros; subst; simpl.
  - reflexivity.
  - rewrite RelTopVal_vrel_equivariant. apply IHpi.
Qed.

Lemma perm_RelBot_vrel pi:
  RelEquiv (perm_vrel pi RelBot) RelBot.
Proof.
  env induction pi; intros; subst; simpl.
  - reflexivity.
  - rewrite RelBot_vrel_equivariant. apply IHpi.
Qed.