Module ValueReductionTerminates

Set Implicit Arguments.
Require Import Coq.Arith.Max.
Require Import Coq.Wellfounded.Inclusion.
Require Import Coq.Wellfounded.Inverse_Image.
Require Import Lexicographic.
Require Import Setoid.
Require Import MyTactics.
Require Import DeBruijn.
Require Import Coercions.
Require Import CoercionMeasure.
Require Import Layers.
Require Import Programs.
Require Import ValueLists.
Require Import Canonical.
Require Import PathSemantics.
Require Import SemanticsValues.

This file proves that the reduction of values terminates.

The argument is rather complex. The presence of recursive coercions, together with the reduction rule RedCoMu, means that coercions are effectively infinite terms, and the reduction of values terminates only because values are finite. The presence of RedCoMu makes it impossible or difficult to use standard techniques based on, say, recursive path orderings.

As a result, our termination argument is based mainly on a multiset of coercion application descriptors, where a coercion application descriptor describes the application of some coercion c to some value v. We take coercion application descriptors to be pairs of the weight of the value v and the measure of the coercion c, and consider them to be lexicographically ordered. The weight of a value measures only the contractive constructors, so as to allow non-contractive structure to be moved around without affecting the weight. The measure of a coercion is defined in such a way that unfolding a coercion preserves its measure -- that is, the measure ignores any part of the coercion that is located below a contractive constructor. As a coercion crosses a contractive constructor, its measure appears to increase, but this is fine, because it is now applied to a value of lesser weight. As a coercion crosses a non-contractive constructor, the weight of the value to which it is applied is preserved, but the measure of the coercion itself decreases. Note that the coercion might even create an unbounded number of copies of itself -- e.g., when CoRegionCap c crosses a VRegionCap constructor, it creates an unbounded number of copies of c -- but this is again fine, because we rely on a multiset ordering.

Note that one could also attempt to use a value's height, instead of its weight. In general, weight seems to be a more stable notion -- it is usually preserved when the value is re-arranged -- whereas height is not -- e.g., the associativity of star may affect height. One exception is DefocusDuplicable, which duplicates part of the value, thus increasing the weight, whereas the height is not increased, because the two copies are placed side by side. For the moment, we choose weight. For this reason, we are not able to view DefocusDuplicable as a coercion; we must make it a primitive operation.

The reduction rules for CoTensorExchange do not fit the above pattern, however, because CoTensorExchange is propagated down -- through both contractive and non-contractive constructors -- while its measure remains constant. As a result, we need another criterion to justify that these rules terminate (and we need to argue that they do not disturb the main argument). We arrange for CoTensorExchange to have zero measure, and we arrange to produce an empty multiset of coercion application descriptors in this case, so CoTensorExchange does not disturb the multiset of coercion application descriptors. Then, we use a polynomial interpretation to argue that the reduction rules for CoTensorExchange terminate.

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

The following polynomial interpretation is designed to prove that the CoTensorExchange reduction rules terminate.

This is fairly simple, since the CoTensorExchange reduction rules push a coercion downwards. The factor 2 in the interpretation of VCoApp ensures that pushing VCoApp down towards the leaves causes a decrease in the interpretation.

Fixpoint poly (v : value) :=
  match v with
  | VVar _ => 0
  | VAbs _
  | VUnit _ => 1
  | VPair _ _ v1 v2 => 1 + poly v1 + poly v2
  | VCoApp _ v => 2 * poly v
  | VTyAbs v
  | VPack v
  | VBang v
  | VLoc _ v
  | VInhabitant v => 1 + poly v
  | VRegionCap vs
  | VRegionCapPunched vs => 1 + polys vs
  end

with polys (vs : values) :=
  match vs with
  | VNil =>
      0
  | VCons v vs =>
      1 + poly v + polys vs
  end.

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

Properties of poly.

Lemma polys_vcoapps:
  forall c vs,
  polys (VCoApps c vs) + count vs = 2 * polys vs.
Proof.
  induction vs; simpl; omega.
Qed.

The following lemma helps show that RedCoTensorExchangeVRegionCap causes a decrease in the polynomial interpretation.

Lemma okRedCoTensorExchangeVRegionCap:
  forall c vs,
  S (polys vs + S (polys vs + 0)) >
  S (polys (VCoApps c vs)).
Proof.
  intros. unpack (polys_vcoapps c vs). omega.
Qed.

Hint Resolve okRedCoTensorExchangeVRegionCap : poly.

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

The weight of a value measures only contractive constructors, and only constructors that do not block value reduction.

Fixpoint weight (v : value) : nat :=
  match v with
  | VVar _
  | VAbs _
  | VUnit _
  | VInhabitant _ =>
      0
  | VTyAbs v
  | VPack v
  | VBang v
  | VCoApp _ v =>
      weight v
  | VPair Physical Physical v1 v2 =>
      1 + weight v1 + weight v2
  | VPair _ _ v1 v2 =>
      weight v1 + weight v2
  | VLoc _ v =>
      1 + weight v
  | VRegionCap vs
  | VRegionCapPunched vs =>
      sum_weight vs
  end

with sum_weight (vs : values) : nat :=
  match vs with
  | VNil =>
      0
  | VCons v vs =>
      weight v + sum_weight vs
  end.

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

Plugging preserves weight. This is used in the analysis of CoDefocus.

Lemma plug_preserves_weight:
  forall pi v1 v2 v'1,
  plug pi v1 v2 v'1 ->
  weight v1 + weight v2 >= weight v'1.
Proof.
  induction 1; intros; layers; omega.
Qed.

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

Import our multisets -- we did not do so earlier because they hide some of the notation for natural numbers, such as addition.

Require Import MyMultisets.
Require Import ValueLists.

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

Define how to compute a descriptor for a coercion application.

Definition desc (c : coercion) (v : value) : Multiset :=
  match measure_coercion c with
  | 0 =>
special case for CoTensorExchange
      empty
  | _ =>
      {{ (weight v, measure_coercion c) }}
  end.

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

The function descs maps a value to a multiset of coercion application descriptors.

Fixpoint descs (v : value) : Multiset :=
  match v with
  | VVar _
  | VAbs _
  | VUnit _
  | VInhabitant _ =>
      empty
  | VTyAbs v
  | VPack v
  | VBang v
  | VLoc _ v =>
      descs v
  | VCoApp c v =>
      desc c v +++ descs v
  | VPair _ _ v1 v2 =>
      descs v1 +++ descs v2
  | VRegionCap vs
  | VRegionCapPunched vs =>
      collect_descs vs
  end

with collect_descs (vs : values) : Multiset :=
  match vs with
  | VNil =>
      empty
  | VCons v vs =>
      descs v +++ collect_descs vs
  end.

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

Some properties of sum_weight.

Lemma member_weight:
  forall v vs,
  member v vs ->
  weight v <= sum_weight vs.
Proof.
  unfold member. induction vs; simpl. tauto. intros [ ? | ? ].
  subst. omega.
  eapply le_trans. apply IHvs; auto. omega.
Qed.

Lemma sum_weight_vmap:
  forall f,
  (forall v, weight (f v) = weight v) ->
  forall vs,
  sum_weight (vmap f vs) = sum_weight vs.
Proof.
  induction vs; simpl; auto.
Qed.

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

A few facts about collect_descs (VCoApps c vs).

The following auxiliary function folds desc c over vs.

Fixpoint fold_desc c vs :=
  match vs with
  | VNil =>
      empty
  | VCons v vs =>
      desc c v +++ fold_desc c vs
  end.

This lemma allows simplifying collect_descs (VCoApps c vs).

Lemma collect_descs_vcoapps:
  forall c vs,
  collect_descs (VCoApps c vs) =mul=
  fold_desc c vs +++ collect_descs vs.
Proof.
  induction vs; simpl.
  auto.
  rewrite IHvs. repeat rewrite <- union_assoc. apply eqmul_simplify_left. apply union_comm_assoc.
Qed.

This lemma is the key reason why the multiset of coercion application descriptors decreases when a coercion crosses a non-contractive constructor. The weight is preserved (in the worst case) but the coercion measure decreases. The coercion may be duplicated -- the list vs may have an arbitrary number of elements -- but this is acceptable.

Lemma in_fold_desc:
  forall c vs,
  {{ (sum_weight vs, S (measure_coercion c)) }} >> fold_desc c vs.
Proof.
  intros.
  eapply singleton_multiset_ordering.
  induction vs; simpl; intros [ ? ? ] ?.
  member_empty.
  member_union.
  unfold desc in *. destruct (measure_coercion c). member_empty. in_singleton. gt.
  forwards: IHvs. eassumption. eapply gt_ge_gt. eassumption. eapply ge_intro. maxxomega.
Qed.

A consequence of the above lemmas.

Lemma in_collect_descs_vcoapps:
  forall c vs,
  {{ (sum_weight vs, S (measure_coercion c)) }} +++ collect_descs vs >>
  collect_descs (VCoApps c vs).
Proof.
  intros. rewrite collect_descs_vcoapps. permut_simpl. apply in_fold_desc.
Qed.

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

Canonical values have an empty multiset of descriptors.

This argument is no longer used, because none of the reduction rules for values has a premise of the form canonical v. We keep this lemma and tactic around, just in case.

Lemma canonical_values_have_empty_descs:
(
  forall v,
  canonical v ->
  descs v = empty
) /\ (
  forall vs,
  each_canonical vs ->
  collect_descs vs = empty
).
Proof.
  apply canonical_induction; simpl; intros;
  repeat match goal with
  | h: descs ?v = empty |- _ =>
      rewrite h; clear h
  end;
  auto.
Qed.

Ltac canonical_values_have_empty_descs :=
  repeat match goal with
  | h: canonical ?v |- context[descs ?v] =>
      rewrite (proj1 canonical_values_have_empty_descs v h)
  | h1: each_canonical ?vs, h2: member ?v ?vs |- context[descs ?v] =>
      rewrite (proj1 canonical_values_have_empty_descs v (each_canonical_member v h1 h2))
  end.

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

CoTensorExchange does not contribute to descs.

Lemma collect_descs_vmap:
  forall f,
  (forall v, descs (f v) = descs v) ->
  forall vs,
  collect_descs (vmap f vs) =mul= collect_descs vs.
Proof.
  introv eq. induction vs; simpl; auto. rewrite IHvs. rewrite eq. auto.
Qed.

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

Value reduction preserves weight.

This property is necessary in order for reduction under a VCoApp _ _ context to cause a decrease in the multiset of coercion application descriptors.

Lemma redv_preserves_weight:
(
  forall v1 v2,
  redv v1 v2 ->
  weight v1 >= weight v2
) /\ (
  forall vs1 vs2,
  redvs vs1 vs2 ->
  sum_weight vs1 >= sum_weight vs2
).
Proof.
  apply redv_redvs_ind; simpl; intros; layers;
  try rewrite sum_weight_vmap;
  try rewrite plus_0_r;
  try solve [ omega | eauto 2 using plug_preserves_weight ].
Qed.

Lemma redv_preserves_desc:
  forall c v1 v2,
  redv v1 v2 ->
  MultisetGE gt (desc c v1) (desc c v2).
Proof.
  unfold desc. intros.
Two cases: measure_coercion c may be zero or non-zero.
  destruct (measure_coercion c).
  right. auto.
  eapply ge_singleton_singleton. eapply ge_intro. eapply redv_preserves_weight. eassumption.
Qed.

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

Plugging preserves descs. If we plug v2 into v1 to obtain v'1, then the multiset associated with v'1 is less than or equal to the union of the multisets associated with v1 and v2.

Lemma plug_preserves_descs:
  forall p v1 v2 v'1,
  plug p v1 v2 v'1 ->
  MultisetGE gt (descs v1 +++ descs v2) (descs v'1).
Proof.
  induction 1; simpl; repeat rewrite union_empty_r; eauto.
PlugRoot
  eapply ge_excess.
PlugPairLeft
  rewrite <- union_assoc.
  rewrite union_comm_assoc_variant.
  rewrite union_assoc.
  eauto using ge_covariant_union, MultisetGE_reflexive.
PlugPairRight
  rewrite <- union_assoc.
  eauto using ge_covariant_union, MultisetGE_reflexive.
Qed.

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

The following many little lemmas analyze the behavior of each value reduction rule with respect to desc.

We could dispense with these lemmas and rely on one big tactic to solve all cases of the main theorem automatically, but this seems more readable and robust.

The following tactic is often useful: unfold the definition of desc and simplify.

Ltac ok :=
  unfold desc; intros; simpl; layers; permut_simpl.

The following tactic is useful when the measure of some coercion appears in the goal: then, we typically need to reason by cases, depending on whether the measure is zero or non-zero.

Ltac dm :=
  repeat match goal with
  |- context[measure_coercion ?c] =>
    destruct (measure_coercion c)
  end.

The following tactic proves a goal of the form gt lhs rhs, where lhs is a singleton and rhs is a union of singletons.

Ltac singletons :=
  eapply singleton_multiset_ordering; intros [ ? ? ] ?; repeat member_union; in_singleton; gt.

Here come the lemmas.

Lemma okLeafCoercion:
  forall c v,
  measure_coercion c > 0 ->
  desc c v >> {{}}.
Proof.
  ok. dm. false; omega. ok.
Qed.

Lemma okCoSeq:
  forall c1 c2 v,
  desc (CoSeq c1 c2) v >> desc c2 (VCoApp c1 v) +++ desc c1 v.
Proof.
  ok. dm; ok; singletons.
Qed.

In the case of RedCoPair, a coercion above a pair is turned into coercions within the pair components. If both components are physical, then the measure of CoPair c1 c2 is 1, regardless of c1 and c2. This is where the multiset ordering comes in: we eliminate a coercion of measure 1 at a certain weight, and introduce coercions of arbitrary measure at lower weights. If at least one component is logical, on the other hand, then we eliminate a coercion of measure 1 + m1 + m2 at a certain weight, and introduce two coercions of measure m1 and m2 at the same weight.

Lemma okCoPair:
  forall layer1 layer2 c1 c2 v1 v2,
  desc (CoPair layer1 layer2 c1 c2) (VPair layer1 layer2 v1 v2) >>
  desc c1 v1 +++ desc c2 v2.
Proof.
  ok; dm; ok; singletons.
Qed.

Lemma okCoForall:
  forall c v,
  desc (CoForall c) (VTyAbs v) >> desc c v.
Proof.
  ok. dm; ok; singletons.
Qed.

Lemma okCoExists:
  forall c v,
  desc (CoExists c) (VPack v) >> desc c v.
Proof.
  ok. dm; ok; singletons.
Qed.

Lemma okCoBang:
  forall c v,
 desc (CoBang c) (VBang v) >> desc c v.
Proof.
  ok. dm; ok; singletons.
Qed.

Lemma okCoRegionCap:
  forall c vs,
  desc (CoRegionCap c) (VRegionCap vs) +++ collect_descs vs >>
  collect_descs (VCoApps c vs).
Proof.
  ok. apply in_collect_descs_vcoapps.
Qed.

Lemma okCoRegionCapPunched:
  forall c vs,
  desc (CoRegionCapPunched c) (VRegionCapPunched vs) +++ collect_descs vs >>
  collect_descs (VCoApps c vs).
Proof.
  ok. apply in_collect_descs_vcoapps.
Qed.

Lemma okCoRef:
  forall c l v,
  desc (CoRef c) (VLoc l v) >> desc c v.
Proof.
  ok. dm; ok; singletons.
Qed.

Lemma okCoForallRegionCap:
  forall vs,
  desc CoForallRegionCap (VTyAbs (VRegionCap vs)) +++ collect_descs vs >>
  collect_descs (VTyAbss vs).
Proof.
  intros. rewrite collect_descs_vmap; eauto. ok.
Qed.

Lemma okCoForallRegionCapPunched:
  forall vs,
  desc CoForallRegionCapPunched (VTyAbs (VRegionCapPunched vs)) +++
  collect_descs vs >> collect_descs (VTyAbss vs).
Proof.
  intros. rewrite collect_descs_vmap; eauto. ok.
Qed.

Lemma okCoDefocus:
  forall p v1 v2 v'1,
  plug p v1 v2 v'1 ->
  desc (CoDefocus p) (VMixPair v1 (VRegionCap (VCons v2 VNil))) +++ descs v1 +++ descs v2 >> descs v'1.
Proof.
  ok.
  forwards ppd: plug_preserves_descs. eassumption.
  eapply MultisetGTGE_transitive; [ idtac | eexact ppd ].
  ok.
Qed.

Lemma okCoMu:
  forall c v,
  ccontractive 0 c ->
  desc (CoMu c) v >> desc (cunfold c) v.
Proof.
  ok. rewrite measure_cunfold; eauto. dm; ok; singletons.
Qed.

Hint Resolve okLeafCoercion okCoSeq okCoPair okCoForall okCoExists
  okCoBang okCoRegionCap okCoRegionCapPunched okCoRef
  okCoForallRegionCap okCoForallRegionCapPunched okCoDefocus okCoMu :
  ok.

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

Value reduction is decreasing with respect to the following lexicographic ordering: 1. most rules cause a decrease in descs, with respect to the multiset ordering; 2. the CoTensorExchange reduction rules preserve descs and cause a decrease in poly. Reduction under a VCoApp context is fine because redv preserves weight -- so the inactive coercion remains at the same weight.

Definition vo :=
  lexprod
    (fun m1 m2 => m1 =mul= m2)
    (MultisetGT gt)
    (fun s1 s2 => s1 > s2).

Definition redvo v1 v2 :=
  vo
    (descs v1, poly v1)
    (descs v2, poly v2).

Definition redvso vs1 vs2 :=
  vo
    (collect_descs vs1, polys vs1)
    (collect_descs vs2, polys vs2).

Lemma redv_redvo:
(
  forall v1 v2,
  redv v1 v2 ->
  mark_ih (
  redvo v1 v2
  )
) /\ (
  forall vs1 vs2,
  redvs vs1 vs2 ->
  mark_ih (
  redvso vs1 vs2
  )
).
Proof.
  apply redv_redvs_ind; intros_ih;
  match goal with

Recognize the cases that involve CoTensorExchange. There, prove that there is a decrease in poly.

  | |- context[CoTensorExchange] =>
      solve [
        right; simpl;
        try rewrite collect_descs_vmap;
        eauto with poly
      ]

Set aside the case of RedVCoAppContext.

  | IH: mark_ih _ |- redvo (VCoApp _ _) (VCoApp _ _) =>

      unfold mark_ih, redvso, redvo, vo in IH

Recognize the cases that involve an induction hypothesis, that is, reduction under a context.

  | IH: mark_ih _ |- _ =>

      unfold mark_ih, redvso, redvo, vo in IH;
      depelim IH; [ left | right ]; simpl;
      [
        permut_simpl
      | match goal with h: _ =mul= _ |- _ => rewrite h end; auto
      | omega
      ]

In the remaining cases, there is a decrease in descs.

  | _ =>
      try solve [
        left; simpl; permut_simpl; eauto 4 with ok
      ]

  end.

RedVCoAppContext

By the induction hypothesis, the pair (descs v1, polys v1) is strictly greater than the pair (descs v1, polys v1). Reason by cases: either descs v1 is strictly greater than descs v2, or they are equal and polys v1 is strictly greater than polys v2.
  match goal with h: lexprod _ _ _ _ _ |- _ => depelim h end.
In the former case, because desc c v1 is greater than or equal to desc c v2 -- indeed, the weight of v1 is greater than or equal to the weight of v2 -- there is a strict decrease in descs.
  left. simpl. eapply union_covariant_ge_gt; eauto using redv_preserves_desc.
In the latter case, again desc c v1 is greater than or equal to desc c v2, and we must distinguish two sub-cases, depending on whether this inequality is strict.
  destruct (redv_preserves_desc c r).
In the first sub-case, there is again a strict decrease in descs.
  left. simpl. eapply union_covariant_gt_ge; eauto using MultisetGE_reflexive.
In the last sub-case, descs is preserved, and there is a strict decrease in polys.
  right; simpl. repeat match goal with eq: _ =mul= _ |- _ => rewrite eq; clear eq end. reflexivity. omega.
  
Qed.

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

Value reduction is well-founded.

Lemma redv_wf:
  well_founded (transpose redv).
Proof.
We have a lexicographic ordering.
  apply wf_incl with (R2 := fun v1 v2 =>
    lexprod (fun m1 m2 => m1 =mul= m2) (MultisetLT gt) (fun s1 s2 => s1 < s2)
      (descs v1, poly v1)
      (descs v2, poly v2)
  ).
  intros v2 v1 ?.

Reformulate the lemma redv_redvo.
  forwards f: (proj1 redv_redvo). eassumption.
  unfold mark_ih, redvo, vo in f. depelim f.
  eauto using MultisetGTLT.
  right. auto using meq_sym. omega.

Conclude.
  apply wf_inverse_image. eapply lexprod_wf; eauto using meq_sym, meq_trans, MultisetLT_wf, lt_wf.
Compatibility between MultisetLT and =mul=.
  introv ? eq. eapply MultisetGTLT. rewrite <- eq. eauto.
Qed.

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

This relation represents value reduction at any active position within a term.

Inductive redvt : term -> term -> Prop :=
| RedvtVal:
    forall v1 v2,
    redv v1 v2 ->
    redvt (TVal v1) (TVal v2)
| RedvtAppContextLeft:
    forall v1 v2 t,
    redv v1 v2 ->
    redvt (TApp v1 t) (TApp v2 t)
| RedvtAppContextRight:
    forall t1 t2 v,
    redvt t1 t2 ->
    redvt (TApp v t1) (TApp v t2)
| RedvtMixPairContextLeft:
    forall t1 t2 v,
    redvt t1 t2 ->
    redvt (TMixPair t1 v) (TMixPair t2 v)
| RedvtTTyAbsContext:
    forall t1 t2,
    redvt t1 t2 ->
    redvt (TTyAbs t1) (TTyAbs t2)
| RedvtTCoAppContext:
    forall c t1 t2,
    redvt t1 t2 ->
    redvt (TCoApp c t1) (TCoApp c t2)
| RedvtTLetUnpackContext:
    forall v1 v2 t,
    redv v1 v2 ->
    redvt (TLetUnpack v1 t) (TLetUnpack v2 t)
| RedvtTLetBangContext:
    forall v1 v2 t,
    redv v1 v2 ->
    redvt (TLetBang v1 t) (TLetBang v2 t)
| RedvtTLetPairContext:
    forall layer1 layer2 v1 v2 t,
    redv v1 v2 ->
    redvt (TLetPair layer1 layer2 v1 t) (TLetPair layer1 layer2 v2 t)
| RedvtTPrimAppContext:
    forall p v1 v2,
    redv v1 v2 ->
    redvt (TPrimApp p v1) (TPrimApp p v2).

Hint Constructors redvt.

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

The relation redvt is well-founded. Indeed, this relation does not affect the structure of the term. So, the term can be seen as a big tuple of values, each of which is allowed to reduce according to redv, a well-founded relation. The proof is carried out by induction over the term. At each node, we use a lemma that is proved via symprod_1 or symprod_2. These tactics prove that the symmetric product of one (resp. two) well-founded orderings is itself well-founded. The proof is basically the same as in Coq's Lexicographic_Product library.

Ltac symprod_1 :=
  induction 1;
  constructor; intros ? h;
  unfold transpose in h; dependent destruction h;
  auto.

Ltac symprod_2 :=
  induction 1 as [ ? _ ih ]; induction 1;
  constructor; intros ? h;
  unfold transpose in h; dependent destruction h; solve [
    apply ih; [ auto | constructor; trivial ]
  | auto ].

Lemma redvt_TVal:
  forall v,
  Acc (transpose redv) v ->
  Acc (transpose redvt) (TVal v).
Proof.
  symprod_1.
Qed.

Lemma redvt_TApp:
  forall v,
  Acc (transpose redv) v ->
  forall t,
  Acc (transpose redvt) t ->
  Acc (transpose redvt) (TApp v t).
Proof.
  symprod_2.
Qed.

Lemma redvt_TMixPair:
  forall v,
  Acc (transpose redv) v ->
  forall t,
  Acc (transpose redvt) t ->
  Acc (transpose redvt) (TMixPair t v).
Proof.
  symprod_2.
Qed.

Lemma redvt_TTyAbs:
  forall t,
  Acc (transpose redvt) t ->
  Acc (transpose redvt) (TTyAbs t).
Proof.
  symprod_1.
Qed.

Lemma redvt_TCoApp:
  forall c t,
  Acc (transpose redvt) t ->
  Acc (transpose redvt) (TCoApp c t).
Proof.
  symprod_1.
Qed.

Lemma redvt_TLetUnpack:
  forall v,
  Acc (transpose redv) v ->
  forall t,
  Acc (transpose redvt) (TLetUnpack v t).
Proof.
  symprod_1.
Qed.

Lemma redvt_TLetBang:
  forall v,
  Acc (transpose redv) v ->
  forall t,
  Acc (transpose redvt) (TLetBang v t).
Proof.
  symprod_1.
Qed.

Lemma redvt_TLetPair:
  forall v,
  Acc (transpose redv) v ->
  forall layer1 layer2 t,
  Acc (transpose redvt) (TLetPair layer1 layer2 v t).
Proof.
  symprod_1.
Qed.

Lemma redvt_TPrimApp:
  forall v,
  Acc (transpose redv) v ->
  forall p,
  Acc (transpose redvt) (TPrimApp p v).
Proof.
  symprod_1.
Qed.

Lemma redvt_THide:
  forall v,
  Acc (transpose redv) v ->
  forall t,
  Acc (transpose redvt) (THide v t).
Proof.
  symprod_1.
Qed.

Hint Resolve redv_wf redvt_TVal redvt_TApp redvt_TMixPair redvt_TTyAbs
redvt_TCoApp redvt_TLetUnpack redvt_TLetBang redvt_TLetPair
redvt_TPrimApp redvt_THide : redvt.

Lemma redvt_wf:
  well_founded (transpose redvt).
Proof.
  intro t; induction t; simpl; auto with redvt.
Qed.

Generated by coq2html