Module Multiplicity

Set Implicit Arguments.
Require Import List.
Require Import MyTactics.
Require Import Resources.

-------------------------------------------------------------------------

A multiplicity is zero, one, or infinity.

A variable that has multiplicity zero can be thought of as absent; its use is forbidden. It is convenient to remember that this variable exists, though, so as to keep de de Bruijn machinery in sync.

A variable that has multiplicity one can be thought of as linear; it must be used once (or at most once, if we take linear to mean affine).

A variable that has multiplicity infinity can be thought of as duplicable; it can be used as many times as desired, including zero and one.

Inductive multiplicity :=
| MZero : multiplicity
| MOne : multiplicity
| MInfinity : multiplicity.

-------------------------------------------------------------------------

Addition of multiplicities.

If one were to view multiplicities as integers, then it would seem natural for addition to be a total function, with the same behavior as integer addition. However, if one thinks of a multiplicity as an indication that a variable belongs in the intuitionistic context, in the linear context, or in neither, then one finds that the laws of addition must reflect the combination of contexts, and fewer cases are allowed. The law 1 + infinity = infinity, for instance, makes intuitive sense; yet, this law would allow a duplicable variable to degenerate into a linear variable on one side, thus allowing implicit dereliction. Similarly, the law 0 + infinity = infinity would allow a duplicable variable to degenerate into an absent variable on one side, thus allowing implicit weakening. These behaviors seem undesirable, so we rule them out and view addition as a three-place relation, where only a few cases are defined.

Inductive mstar : multiplicity -> multiplicity -> multiplicity -> Prop :=
| MStarZero:
    mstar MZero MZero MZero
| MStarOneLeft:
    mstar MOne MZero MOne
| MStarOneRight:
    mstar MZero MOne MOne
| MStarInfinity:
    mstar MInfinity MInfinity MInfinity.

Hint Constructors mstar.

-------------------------------------------------------------------------

The total function madd underlies mstar.

Fixpoint madd m1 m2 :=
  match m1, m2 with
  | MZero, m
  | m, MZero
    => m
  | MInfinity, MInfinity
    => MInfinity

the rest is irrelevant, but must satisfy commutativity and associativity; we choose to implement a maximum function.

  | MInfinity, _
  | _, MInfinity =>
      MInfinity
  | MOne, MOne =>
      MOne
  end.

-------------------------------------------------------------------------

The total function mneutral maps a multiplicity m to its unit.

Definition mneutral (m : multiplicity) : multiplicity :=
  match m with
  | MZero =>
      MZero
  | MOne =>
      MZero
  | MInfinity =>
      MInfinity
  end.

-------------------------------------------------------------------------

Multiplicities form a separation algebra.

Thus, by adopting trivial relations rxo and rio, we can argue that multiplicities form a monotonic separation algebra, i.e. they are an instance of the type class STAR.

Program Instance multiplicity_resource : STAR multiplicity := {

  star := mstar;
  add := madd;
  neutral := mneutral;
  rxo m1 m2 := m1 = m2;
  rio m1 m2 := m1 = m2

}.

Next Obligation.

inversion 1; eauto.
Qed.

Next Obligation.

inversion 1; inversion 1; eauto.
Qed.

Next Obligation.

destruct R1; destruct R2; destruct R; inversion 1; auto.
Qed.

Next Obligation.

destruct R1; destruct R2; auto.
Qed.

Next Obligation.

destruct R1; destruct R2; destruct R3; simpl; auto.
Qed.

Next Obligation.

inversion 1; inversion 1; simpl; subst; eauto.
Qed.

Next Obligation.

destruct R; auto.
Qed.

Next Obligation.

inversion 1; auto.
Qed.

Next Obligation.

inversion 1; eauto.
Qed.

Next Obligation.

destruct R1; destruct R2; destruct R; inversion 1; auto.
Qed.

-------------------------------------------------------------------------

Nonzero multiplicities.

Inductive nonzero : multiplicity -> Prop :=
| NonzeroOne: nonzero MOne
| NonzeroInfinity: nonzero MInfinity.

Hint Constructors nonzero.

If a summand is non-zero, then the sum is non-zero.

Lemma nonzero_star:
  forall m1 m2 m,
  nonzero m1 ->
  star m1 m2 m ->
  nonzero m.

Proof.

unfold star; simpl.
introv h1 h2; dependent destruction h1; dependent destruction h2; constructor.
Qed.

-------------------------------------------------------------------------

A multiplicity environment is a list of multiplicities.

Notation menv :=
(list multiplicity).

Multiplicity environments form a separation algebra. There is nothing to say; this is a consequence of the ``list'' instance of separation algebras.

-------------------------------------------------------------------------

Repeat the definition of star, and some of its consequences, before making it opaque. (The definition of star is made opaque in ResourcesContinued.

Lemma StarZero:
star MZero MZero MZero.

Proof.

simpl; eauto.
Qed.

Lemma StarOneLeft:
star MOne MZero MOne.

Proof.

simpl; eauto.
Qed.

Lemma StarOneRight:
star MZero MOne MOne.

Proof.

simpl; eauto.
Qed.

Lemma StarInfinity:
star MInfinity MInfinity MInfinity.

Proof.

simpl; eauto.
Qed.

Hint Resolve StarZero StarOneLeft StarOneRight StarInfinity.

Lemma menv_star_nil:
star (nil : menv) nil nil.

Proof.

simpl. eauto.
Qed.

Lemma menv_star_cons:
  forall (M1 M2 M : menv) m1 m2 m,
  star M1 M2 M ->
  star m1 m2 m ->
  star (m1 :: M1) (m2 :: M2) (m :: M).

Proof.

simpl. eauto.
Qed.

Hint Resolve menv_star_nil menv_star_cons.

If M1 + M2 = nil, then M1 = M2 = nil.

Lemma invert_menv_star_nil:
  forall M1 M2 : menv,
  star M1 M2 nil ->
  M1 = nil /\ M2 = nil.

Proof.

simpl. inversion 1. eauto.
Qed.

Ltac nil :=
  match goal with h: star ?M1 ?M2 nil |- _ =>
    unpack (invert_menv_star_nil h); clear h; subst M1; subst M2
  end.

Repeat the definition of neutral, and some of its consequences, before making it opaque. (The definition of neutral is made opaque in ResourcesContinued.

neutral preserves length.

Lemma neutral_length:
forall M : menv,
length (neutral M) = length M.

Proof.

intros. simpl. apply map_length.
Qed.

Lemma le_length_neutral:
  forall k (M : menv),
  k <= length M ->
  k <= length (neutral M).

Proof.

intros. rewrite neutral_length. assumption.
Qed.

-------------------------------------------------------------------------

TEMPORARY nettoyer?

This tactic simplifies the context by removing redundant requirements of the form nil = nil or nil ~= nil.

Ltac nilnil :=
  repeat match goal with
  | h: _ = nil -> _ |- _ => generalize (h eq_refl); clear h; intro h
  | h: _ ~= nil -> _ |- _ => generalize (h JMeq_refl); clear h; intro h
  end.

Hints for proving that two multiplicity environments join. These hints are used, for instance, in the proof of j_multiplicity_weakening.

Hint Extern 1 (@star menv _ _ _ _) => eapply menv_star_cons.

Hint Extern 1 (@star menv _ _ _ (neutral _)) =>
  match goal with
  | h: star _ _ ?M |- star _ _ (neutral ?M) =>
      eapply star_neutral_map
  | _ =>
      apply duplicable_neutral
  end.