Module ProgressValues

Set Implicit Arguments.
Require Import DeBruijn.
Require Import MyTactics.
Require Import Types.
Require Import TypeEquality.
Require Import TypeContexts.
Require Import FocusPaths.
Require Import Focus.
Require Import Coercions.
Require Import Programs.
Require Import Subtyping.
Require Import DerivedSubtyping.
Require Import Typing.
Require Import DerivedTyping.
Require Import Environments.
Require Import Multiplicity.
Require Import MultiplicityEnvironments.
Require Import Canonical.
Require Import PathSemantics.
Require Import SemanticsValues.
Require Import PreliminaryLemmas.
Require Import TypeSubstitution.
Require Import TermSubstitution.
Require Import CoercionSubstitution.
Require Import InversionClassification.
Require Import Resources.
Require Import ResourcesContinued.
Require Import Monotonicity.
Require Import Closed.
Require Import Erasure.
Require Import ValueLists.
Require Import LittleFacts.

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

Every well-typed value either is canonical or reduces.

Lemma progress_values_preliminary:
(
  forall R M E v T,
  jv R M E v T ->
  M = nil ->
  E = nil ->
  canonical v \/ (exists w, redv v w)
) /\ (
  forall R vs T,
  ji R vs T ->
  each_canonical vs \/ (exists ws, redvs vs ws)
) /\ (
  forall R M E t T,
  jt R M E t T ->
  True
).
Ltac progress_values_ih :=
  match goal with
  | h: _ \/ _ |- _ =>
      destruct h as [ ? | [ ? ? ]]; try here
  end.

Proof.

apply jvit_ind; intros; subst; try nil; nilnil; try solve [ eauto | left; eauto ];

Reduction under certain contexts is permitted.

try solve [ progress_values_ih ];
try solve [ progress_values_ih; progress_values_ih ].

Coercion applications reduce.

right.

If the argument v of the coercion reduces, then the application itself reduces.

progress_values_ih.

So, there only remains the case where v is canonical. Proceed by cases over the coercion c. Dispatch almost all cases by using the classification and inversion lemmas.

  match goal with h: jco _ _ _ |- _ => depelim h end;
  try solve [
    toplevel
  | classify_and_invert; try solve [

CoBangRef, CoBangRegionCap, CoBangRegionCapPunched

These coercions do not have a reduction rule, but that is not a problem, because they can never be applied to a canonical value.

      false; eauto 3 using duplicable_own_location, duplicable_own_region, (@duplicable_split resource)
    | eauto using cwf_mu with resources
    ]
  ].

Two cases are somewhat tough and remain.

CoDefocus

  classify_and_invert.
  forwards: defocus_progress_select; try eassumption.
  forwards: defocus_progress_plug; try eassumption.
    eapply JVRegionCap_flexible_singleton; eauto 2.
  unpack.
  intuition eauto.

CoTensorExchange

CoTensorExchange has a reduction rule for every possible form of closed, canonical value.

match goal with h: canonical _ |- _ => inversion h; subst end; eauto 2.
false; eauto using toplevel_var.
Qed.

Lemma progress_values:
  forall R v T,
  jv R nil nil v T ->
  canonical v \/ (exists w, redv v w).

Proof.

eauto using (pi1 progress_values_preliminary).
Qed.