Set Implicit Arguments.
Require Import DeBruijn.
Require Import MyTactics.
Require Import Types.
Require Import TypeEquality.
Require Import Coercions.
Require Import Programs.
Require Import Subtyping.
Require Import ValueLists.
Require Import RawPrograms.
Require Import Erasure.
Require Import Typing.
Require Import Environments.
Require Import Multiplicity.
Require Import MultiplicityEnvironments.
Require Import Resources.
Require Import ResourcesContinued.
-------------------------------------------------------------------------
The monotonicity lemma: well-typedness is preserved under rio.
Lemma j_rio:
(
forall R1 M E v T,
jv R1 M E v T ->
forall R2,
rio R1 R2 ->
jv R2 M E v T
) /\ (
forall R1 vs T,
ji R1 vs T ->
forall R2,
rio R1 R2 ->
ji R2 vs T
) /\ (
forall R1 M E t T,
jt R1 M E t T ->
forall R2,
rio R1 R2 ->
jt R2 M E t T
).
Proof.
apply jvit_ind;
eauto with resources;
intros;
try solve [
rio_star;
eauto ];
JVRegionCap, JVRegionCapPunched, JVLoc
rio_star;
match goal with ih:
forall R2,
rio ?
R R2 ->
_,
h:
rio ?
R ?
R2 |-
_ =>
unpack (
ih _ h);
clear ih end;
econstructor;
eauto with resources.
Qed.
Lemma j_rio_term:
forall R1 M E t T,
jt R1 M E t T ->
forall R2,
rio R1 R2 ->
jt R2 M E t T.
Proof.
intros.
eapply j_rio;
eauto.
Qed.