Set Implicit Arguments.
Require Import MyTactics.
Require Import DeBruijn.
Require Import Layers.
Require Import Coercions.
The measure of a coercion counts 1 at contractive constructors,
such as CoArrow, and counts 1 plus the measure of the children
at non-contractive constructors, such as CoSeq and CoForall.
Indeed, when a CoArrow coercion reduces, its children become
buried under a lambda-abstraction, so their measure does not
matter.
Fixpoint measure_coercion (
c :
coercion) :
nat :=
match c with
|
CoVar _
|
CoTensorExchange _ =>
0
|
CoId
|
CoForallIntro
|
CoForallElim
|
CoExistsIntro
|
CoExistsLeftIntro
|
CoExistsElim
|
CoDereliction
|
CoBangIdempotent
|
CoPairBang
|
CoBangPair
|
CoUnitBang
|
CoBangRef
|
CoBangRegionCap
|
CoBangRegionCapPunched
|
CoAtBang
|
CoDistrib
|
CoSingletonToGroup
|
CoForallPair
|
CoForallBang
|
CoForallRef
|
CoForallRegionCap
|
CoForallRegionCapPunched
|
CoSingletonRegionCapExists
|
CoPairExistsLeft
|
CoPairExistsRight
|
CoBangExists
|
CoRefExists
|
CoDefocus _
|
CoDefocusGroup
|
CoStarCommutative
|
CoStarAssociative
|
CoStarRef
|
CoRefStar
|
CoStarSingleton
|
CoSingletonStar
|
CoArrow _ _
|
CoPair Physical Physical _ _
|
CoRef _ =>
1
|
CoSeq c1 c2
|
CoPair _ _ c1 c2 =>
1 +
measure_coercion c1 +
measure_coercion c2
|
CoForall c
|
CoExists c
|
CoBang c
|
CoRegionCap c
|
CoRegionCapPunched c
|
CoMu c =>
1 +
measure_coercion c
end.
Unfolding a well-formed coercion does not affect its measure.
As a result, the measure of cunfold c is strictly less than the measure
of CoMu c.
Lemma measure_subst_co:
forall k c,
ccontractive k c ->
forall d,
measure_coercion c =
measure_coercion (
subst_co d k c).
Proof.
induction 1; simpl; intro; layers; eauto.
unfold subst_var; by_cases; easy.
Qed.
Lemma measure_cunfold:
forall c,
ccontractive 0
c ->
measure_coercion c =
measure_coercion (
cunfold c).
Proof.