Set Implicit Arguments.
Require Import Programs.
Require Import ValueLists.
A canonical value is one that does not contain any coercion application,
except under VAbs or VInhabitant.
Inductive canonical :
value ->
Prop :=
|
CanonicalVVar:
forall x,
canonical (
VVar x)
|
CanonicalVAbs:
forall t,
canonical (
VAbs t)
|
CanonicalVPair:
forall layer1 layer2 v1 v2,
canonical v1 ->
canonical v2 ->
canonical (
VPair layer1 layer2 v1 v2)
|
CanonicalVUnit:
forall layer,
canonical (
VUnit layer)
|
CanonicalVTyAbs:
forall v,
canonical v ->
canonical (
VTyAbs v)
|
CanonicalVPack:
forall v,
canonical v ->
canonical (
VPack v)
|
CanonicalVBang:
forall v,
canonical v ->
canonical (
VBang v)
|
CanonicalVRegionCap:
forall vs,
each_canonical vs ->
canonical (
VRegionCap vs)
|
CanonicalVRegionCapPunched:
forall vs,
each_canonical vs ->
canonical (
VRegionCapPunched vs)
|
CanonicalVLoc:
forall l v,
canonical v ->
canonical (
VLoc l v)
|
CanonicalVInhabitant:
forall v,
canonical (
VInhabitant v)
with each_canonical :
values ->
Prop :=
|
EachNil:
each_canonical VNil
|
EachCons:
forall v vs,
canonical v ->
each_canonical vs ->
each_canonical (
VCons v vs).
Hint Constructors canonical each_canonical.
A mutual induction scheme.
Scheme canonical_ind_v :=
Induction for canonical Sort Prop
with canonical_ind_vs :=
Induction for each_canonical Sort Prop.
Combined Scheme canonical_induction from canonical_ind_v,
canonical_ind_vs.
Basic facts about canonical values.
Lemma canonical_lift:
forall v,
canonical v ->
forall k,
canonical (
lift_value k v).
Proof.
induction 1; intro; simpl; eauto.
Qed.
Lemma each_canonical_singleton_inversion:
forall v,
each_canonical (
VCons v VNil) ->
canonical v.
Proof.
inversion 1. auto.
Qed.
Lemma each_canonical_member:
forall v vs,
each_canonical vs ->
member v vs ->
canonical v.
Proof.
unfold member. induction vs; simpl. tauto.
intros h [ ? | ? ]; inversion h; subst; auto.
Qed.
Hint Resolve each_canonical_singleton_inversion each_canonical_member.