Set Implicit Arguments.
Require Import Layers.
Require Import Types.
Require Import TypeEquality.
Require Import TypeContexts.
A focus path is an indication of where focus (or defocus) should
take place.
Inductive path :
Set :=
|
PathRoot:
path
|
PathPairLeft:
layer ->
layer ->
path ->
path
|
PathPairRight:
layer ->
layer ->
path ->
path
|
PathRef:
path ->
path
|
PathRegionCapSingleton:
path ->
path
tex: focus paths
.
pi is a focus path for a type context TC if, for every type T,
pi leads from a root value of type TC T down to a sub-value of
type T.
Inductive jpath :
path ->
ty_ctx ->
Prop :=
|
JPathRoot:
jpath PathRoot hole
|
JPathPairLeft:
forall pi TC T2 layer1 layer2,
jpath pi TC ->
wf T2 ->
jpath (
PathPairLeft layer1 layer2 pi) (
TyPair layer1 layer2 TC (
constant T2))
|
JPathPairRight:
forall pi TC T1 layer1 layer2,
jpath pi TC ->
wf T1 ->
jpath (
PathPairRight layer1 layer2 pi) (
TyPair layer1 layer2 (
constant T1)
TC)
|
JPathRef:
forall pi TC,
jpath pi TC ->
jpath (
PathRef pi) (
TyRef TC)
|
JPathRegionCapSingleton:
forall pi TC sigma,
jpath pi TC ->
wf sigma ->
jpath (
PathRegionCapSingleton pi) (
TyRegionCap Singleton (
constant sigma)
TC)
.
Hint Constructors jpath.
Well-formedness.
Lemma jpath_lift:
forall pi TC k,
jpath pi TC ->
jpath pi (
lift_ty_ctx k TC).
Proof.
induction 1;
unfold lift_ty_ctx,
hole,
constant in *;
simpl in *;
eauto;
rewrite <-
lift_lift_ty;
eauto.
Qed.
Lemma jpath_subst:
forall pi TC k U,
jpath pi TC ->
wf U ->
jpath pi (
subst_ty_ctx U k TC).
Proof.
induction 1;
unfold subst_ty_ctx,
hole,
constant in *;
simpl in *;
eauto;
rewrite <-
lift_subst_1_ty;
eauto.
Qed.
Lemma jpath_wf_1:
forall pi TC,
jpath pi TC ->
wf TC.
Proof.
induction 1; unfold fill, hole, constant; simpl; eauto.
Qed.
Lemma jpath_wf_2:
forall TC pi T,
jpath pi TC ->
wf (
fill TC T) ->
wf T.
Proof.
unfold fill; induction 1; simpl; intros; eauto.
Qed.
Hint Resolve jpath_wf_1.