Module MultiplicityEnvironments

Set Implicit Arguments.
Require Import MyTactics.
Require Import Resources.
Require Import Multiplicity.
Require Import Environments.

This file proves several basic facts about multiplicity environments.

Lemma jenv_neutral:
  forall (M : menv) x m,
  jenv M x m ->
  forall nm,
  nm = neutral m ->
  jenv (neutral M) x nm.

Proof.

simpl; eauto using jenv_map.
Qed.

Lemma jenv_neutral_zero:
  forall M x,
  jenv M x MZero ->
  jenv (neutral M) x MZero.

Proof.

eauto using jenv_neutral.
Qed.

Lemma jenv_neutral_one:
  forall M x,
  jenv M x MOne ->
  jenv (neutral M) x MZero.

Proof.

eauto using jenv_neutral.
Qed.

Lemma jenv_neutral_infinity:
  forall M x,
  jenv M x MInfinity ->
  jenv (neutral M) x MInfinity.

Proof.

eauto using jenv_neutral.
Qed.

Lemma insert_star:
  forall k (m1 m2 m : multiplicity) (M1 M2 M : menv),
  star m1 m2 m ->
  star M1 M2 M ->
  star (insert_env k m1 M1) (insert_env k m2 M2) (insert_env k m M).

Proof.

simpl; induction k; inversion 2; subst; simpl; intros; eauto.
Qed.

If the addition of N1 and N2 is N, and if one decides to weaken N with a new binding, then it is possible to weaken N1 and N2 so as to preserve the addition. Since the new binding is unused, it can be split in an arbitrary way.

Lemma split_as_you_like:
  forall k (N1 N2 M : menv),
  star N1 N2 (remove_env_entry k M) ->
  exists M1 M2,
  star M1 M2 M /\
  N1 = remove_env_entry k M1 /\
  N2 = remove_env_entry k M2.

Proof.

induction k; introv h.

Base case.

First, eliminate a stupid sub-case where everything is nil.

dependent destruction M. inversion h; subst. eauto.

Now, the real base case. We have an unused binding of multiplicity m. We must split it (in an arbitrary way) to obtain an unused binding on either side.

repeat econstructor; eauto. eapply star_neutral.

The general case.

Again, eliminate a stupid sub-case where everything is nil.

dependent destruction M; inversion h; subst. eauto.

Now, the real general case. Just skip a binding.

forwards: IHk. eassumption. unpack.
repeat econstructor; eauto. simpl; congruence. simpl; congruence.
Qed.

M1 + M2 = M implies M1\k + M2\k = M\k.

Lemma split_as_dictated:
  forall k (M1 M2 M : menv),
  star M1 M2 M ->
  star (remove_env_entry k M1) (remove_env_entry k M2) (remove_env_entry k M).

Proof.

simpl; induction k; introv h; dependent destruction M; dependent destruction h; simpl; eauto.
Qed.

Splitting a variable of multiplicity zero yields a variable of multiplicity zero on both sides.

Lemma split_zero:
  forall k M,
  jenv M k MZero ->
  forall M1 M2,
  star M1 M2 M ->
  jenv M1 k MZero /\ jenv M2 k MZero.

Proof.

  simpl.
  introv h; dependent induction h; introv i; dependent destruction i.
  dependent destruction H; eauto.
  unpack (IHh _ _ i); eauto.
Qed.

Splitting a variable of multiplicity one sends it either to the right-hand side or to the left-hand side.

Lemma split_one:
  forall k M,
  jenv M k MOne ->
  forall M1 M2,
  star M1 M2 M ->
  (jenv M1 k MZero /\ jenv M2 k MOne) \/ (jenv M1 k MOne /\ jenv M2 k MZero).

Proof.

  simpl.
  introv h; dependent induction h; introv i; dependent destruction i.
  dependent destruction H; try solve [ right; eauto | left; eauto ].
  generalize (IHh _ _ i); intros [[ ? ? ] | [ ? ? ]]; intuition eauto.
Qed.

Ltac split_one :=
match goal with h1: jenv ?M ?k MOne, h2: star ?M1 ?M2 ?M |- _ =>
generalize (split_one h1 h2); intros [[ ? ? ] | [ ? ? ]] end.

Splitting a variable of multiplicity infinity sends it into both sides.

Lemma split_infinity:
  forall k M,
  jenv M k MInfinity ->
  forall M1 M2,
  star M1 M2 M ->
  jenv M1 k MInfinity /\ jenv M2 k MInfinity.

Proof.

  simpl.
  introv h; dependent induction h; introv i; dependent destruction i.
  dependent destruction H; intuition eauto.
  unpack (IHh _ _ i); intuition eauto.
Qed.

If a variable exists with some multiplicity in M1, then it exists with a greater multiplicity in M1 + M2.

Lemma jenv_star:
  forall (M1 : menv) k m1,
  jenv M1 k m1 ->
  forall M2 M,
  star M1 M2 M ->
  exists m2 m,
  jenv M2 k m2 /\
  jenv M k m /\
  star m1 m2 m.

Proof.

  simpl.
  induction 1; introv h; dependent destruction h. eauto.
  forwards : IHjenv. eassumption. unpack. eauto 7.
Qed.

A variable k is present in a multiplicity environment M if the multiplicity m of k in M is nonzero.

Definition present M k :=
exists m, nonzero m /\ jenv M k m.

Hint Unfold present.

If a variable is present in M1, then it is present in M1 + M2.

Lemma present_star:
  forall M1 k,
  present M1 k ->
  forall M2 M,
  star M1 M2 M ->
  present M k.

Proof.

  introv [ ? [ ? ? ]] ?.
  forwards : jenv_star. eassumption. eassumption. unpack.
  eauto using nonzero_star.
Qed.

Two substitution lemmas: if k is present and we remove x, then k is still present.

Lemma present_substitution_recent:
  forall M k,
  present M k ->
  forall x N P,
  star (remove_env_entry x M) N P ->
  k < x ->
  present P k.

Proof.

  introv [ ? [ ? ? ]] ? ?.
  forwards : jenv_star. apply jenv_substitution_recent; eassumption. eassumption. unpack.
  eauto using nonzero_star.
Qed.

Lemma present_substitution_old:
  forall M k,
  present M k ->
  forall x N P,
  star (remove_env_entry x M) N P ->
  k > x ->
  present P (k - 1).

Proof.

  introv [ ? [ ? ? ]] ? ?.
  forwards : jenv_star. apply jenv_substitution_old; eassumption. eassumption. unpack.
  eauto using nonzero_star.
Qed.

If M1 + M2 = M and M\k + N = P, then M1\k + (M2\k + N) = P.

Lemma rotate_right_remove:
  forall k,
  forall M1 M2 M N P : menv,
  star M1 M2 M ->
  star (remove_env_entry k M) N P ->
  exists M2kN,
  star (remove_env_entry k M2) N M2kN /\
  star (remove_env_entry k M1) M2kN P.

Proof.

introv m p. eapply star_associative. eapply split_as_dictated. eassumption. assumption.
Qed.

Ltac rotate_right_remove :=
match goal with h1: star ?M1 ?M2 ?M, h2: star (remove_env_entry ?k ?M) ?N ?P |- _ =>
unpack (rotate_right_remove _ h1 h2) end.

If M1 + M2 = M and M\k + N = P, then (M1\k + N) + M2\k = P.

Lemma permute_left_remove:
  forall k,
  forall M1 M2 M N P : menv,
  star M1 M2 M ->
  star (remove_env_entry k M) N P ->
  exists M1kN,
  star (remove_env_entry k M1) N M1kN /\
  star M1kN (remove_env_entry k M2) P.

Proof.

  introv m p.
  forwards: rotate_right_remove. apply star_commutative. eexact m. eexact p. unpack.
  eauto using (@star_commutative menv).
Qed.

Ltac permute_left_remove :=
match goal with h1: star ?M1 ?M2 ?M, h2: star (remove_env_entry ?k ?M) ?N ?P |- _ =>
unpack (permute_left_remove _ h1 h2) end.

Commutation between remove_env_entry and neutral.

Lemma neutral_remove:
  forall k,
  forall M : menv,
  neutral (remove_env_entry k M) = remove_env_entry k (neutral M).

Proof.

simpl. eauto using map_remove.
Qed.

If M\k + N = P and N is duplicable, then nM\k + N = nP.

Lemma j_term_substitution_infinity_bang:
  forall k,
  forall M N P : menv,
  star (remove_env_entry k M) N P ->
  duplicable N ->
  star (remove_env_entry k (neutral M)) N (neutral P).

Proof.

  introv ? h.
  rewrite <- neutral_remove.
  rewrite (duplicable_implies_core _ h).
  eapply star_neutral_map. eauto.
Qed.