Require Import String.
Require Import List.
Require Import RelationClasses.
Require Import Utils.
Require Import ForeignType.
Require Import RType.
Require Import BrandRelation.
Require Export RSubtype.
Section RSubtypeProp.
Context {
ftype:
foreign_type}.
Context {
m:
brand_relation}.
Lemma top_subtype z : ⊤ <:
z ->
z = ⊤.
Proof.
inversion 1; subst; eauto.
Qed.
Lemma subtype_bottom z :
z <: ⊥ ->
z = ⊥.
Proof.
inversion 1; subst; eauto.
Qed.
Ltac simpl_type :=
repeat match goal with
| [
H: ?
z <: ⊥ |-
_] =>
apply subtype_bottom in H;
subst
| [
H: ⊤ <: ?
z |-
_] =>
apply top_subtype in H;
subst
end.
Local Hint Constructors subtype :
qcert.
Instance subtype_trans :
Transitive subtype.
Proof.
red.
intros x y.
revert x.
induction y using rtype_rect;
intros x z sub1 sub2;
inversion sub1;
subst;
simpl_type;
eauto with qcert.
-
inversion sub2;
subst;
eauto with qcert.
rtype_equalizer.
subst;
eauto with qcert.
-
inversion sub2;
subst;
qeauto.
rtype_equalizer.
subst.
constructor.
+
intros s'
r'
lsr'.
destruct (
H5 _ _ lsr')
as [?[
look3 sub3]].
destruct (
H3 _ _ look3)
as [?[??]].
exists x0;
intuition.
generalize (
Forallt_In H (
s',
x)).
simpl;
intros P;
eapply P;
eauto.
apply (
lookup_in string_dec);
trivial.
+
intuition.
-
inversion sub2;
subst;
qeauto.
rtype_equalizer.
subst.
qeauto.
-
rtype_equalizer.
subst.
inversion sub2;
subst;
trivial with qcert.
rtype_equalizer.
subst.
econstructor;
qeauto.
-
inversion sub2;
subst;
trivial with qcert.
apply canon_equiv in H;
apply canon_equiv in H0.
rewrite H in H1.
rewrite H0 in H2.
constructor;
etransitivity;
eassumption.
-
invcs sub2;
qtrivial.
econstructor.
transitivity ft;
trivial.
Qed.
Global Instance subtype_pre :
PreOrder subtype.
Proof.
Lemma Rec_subtype_cons_weaken k s r l₁
pf pf2:
Rec k ((
s,
r) ::
l₁)
pf <:
Rec Open l₁
pf2.
Proof.
Lemma Rec_subtype_cons_inv2 {
k1 k2 s r l₁
l₂
pf pf2}:
Rec k1 l₁
pf <:
Rec k2 ((
s,
r) ::
l₂)
pf2 ->
exists pf',
Rec k1 l₁
pf <:
Rec Open l₂
pf'.
Proof.
Lemma Rec_subtype_cons_inv1_open {
k1 k2 s r l₁
l₂
pf pf2}:
Rec k1 ((
s,
r) ::
l₁)
pf <:
Rec k2 l₂
pf2 ->
lookup string_dec l₂
s =
None ->
k2 =
Open.
Proof.
Lemma Rec_subtype_cons_inv1 {
k1 k2 s r l₁
l₂
pf pf2}:
Rec k1 ((
s,
r) ::
l₁)
pf <:
Rec k2 l₂
pf2 ->
lookup string_dec l₂
s =
None ->
exists pf',
Rec k1 l₁
pf' <:
Rec Open l₂
pf2.
Proof.
intros rt lo.
generalize (
Rec_subtype_cons_inv1_open rt lo);
intros;
subst.
inversion rt;
subst;
rtype_equalizer.
-
destruct l₂;
simpl in H2;
try discriminate.
inversion H2;
subst.
rtype_equalizer.
subst.
destruct p;
simpl in *.
destruct (
string_dec s s);
intuition congruence.
-
subst.
destruct rl1;
simpl in H0;
try discriminate.
inversion H0;
rtype_equalizer.
subst.
destruct p;
simpl in lo |- *.
generalize pf.
rewrite domain_cons,
is_list_sorted_cons;
simpl.
intros [
pf'
_].
exists pf'.
apply SRec_open;
intros s0 r0 ls0.
specialize (
H2 _ _ ls0);
simpl in H2.
destruct (
string_dec s0 s);
eauto.
destruct H2 as [? [
inv _]].
inversion inv;
subst.
congruence.
Qed.
Note that unlike the biased inverses, since we are removing
an element from both sides, it is possible for k2 to be Closed
Lemma Rec_subtype_cons_inv {
k1 k2 s r1 r2 l₁
l₂
pf pf2}:
Rec k1 ((
s,
r1) ::
l₁)
pf <:
Rec k2 ((
s,
r2) ::
l₂)
pf2 ->
exists pf'
pf2',
Rec k1 l₁
pf' <:
Rec k2 l₂
pf2'.
Proof.
intros rt.
inversion rt;
subst;
rtype_equalizer;
subst.
-
repeat (
exists (
is_list_sorted_cons_inv _ pf)).
reflexivity.
-
destruct rl1;
simpl in H0;
try discriminate.
destruct rl2;
simpl in H3;
try discriminate.
inversion H0;
inversion H3;
clear H0;
clear H3.
rtype_equalizer.
subst.
exists (
is_list_sorted_cons_inv _ pf).
exists (
is_list_sorted_cons_inv _ pf2).
generalize (
is_list_sorted_NoDup ODT_lt_dec _ pf).
generalize (
is_list_sorted_NoDup ODT_lt_dec _ pf2).
intros.
constructor.
+
intros.
specialize (
H2 s r').
simpl in H2.
destruct p;
destruct p0;
simpl in *;
subst.
destruct (
string_dec s s0).
*
inversion H;
subst.
apply lookup_in in H1.
apply in_dom in H1.
intuition.
*
auto.
+
intuition;
subst.
destruct p;
destruct p0;
simpl in *;
subst.
specialize (
H5 s).
intuition.
inversion H0;
subst.
intuition.
Qed.
Global Instance subtype_part :
PartialOrder eq subtype.
Proof.
Lemma wf_rtype_subtype_refl τ
pf1 pf2:
exist (
fun τ₀ :
rtype₀ =>
wf_rtype₀ τ₀ =
true) τ
pf1 <:
exist (
fun τ₀ :
rtype₀ =>
wf_rtype₀ τ₀ =
true) τ
pf2.
Proof.
generalize (wf_rtype₀_ext pf1 pf2); intros s.
subst. reflexivity.
Qed.
Lemma Rec_subtype_cons_eq {
k₁
k₂
s r₁
r₂
rl₁
rl₂
pf1 pf2} :
Rec k₁ ((
s,
r₁) ::
rl₁)
pf1 <:
Rec k₂ ((
s,
r₂) ::
rl₂)
pf2 ->
r₁ <:
r₂.
Proof.
inversion 1;
subst;
rtype_equalizer.
subst;
intros.
reflexivity.
destruct rl1;
try discriminate.
destruct rl2;
try discriminate.
destruct p;
destruct p0.
simpl in H1,
H4.
inversion H1;
subst.
inversion H4;
subst.
rtype_equalizer.
subst.
specialize (
H3 s r₂).
simpl in H3.
destruct (
string_dec s s);
intuition.
destruct H0 as [? [
inv sub]].
inversion inv;
subst.
auto.
Qed.
Lemma STop₀
pf τ : τ <:
exist (
fun τ₀ :
rtype₀ =>
wf_rtype₀ τ₀ =
true) ⊤₀
pf.
Proof.
Lemma SBottom₀
pf τ :
exist (
fun τ₀ :
rtype₀ =>
wf_rtype₀ τ₀ =
true) ⊥₀
pf <: τ.
Proof.
Lemma SRefl₀ τ₀
pf :
exist (
fun τ₀ :
rtype₀ =>
wf_rtype₀ τ₀ =
true) τ₀
pf <:
exist (
fun τ₀ :
rtype₀ =>
wf_rtype₀ τ₀ =
true) τ₀
pf.
Proof.
Lemma SColl₀ τ₁
pf₁ τ₂
pf₂ :
exist (
fun τ₀ :
rtype₀ =>
wf_rtype₀ τ₀ =
true) τ₁
pf₁ <:
exist (
fun τ₀ :
rtype₀ =>
wf_rtype₀ τ₀ =
true) τ₂
pf₂ ->
exist (
fun τ₀ :
rtype₀ =>
wf_rtype₀ τ₀ =
true) (
Coll₀ τ₁)
pf₁ <:
exist (
fun τ₀ :
rtype₀ =>
wf_rtype₀ τ₀ =
true) (
Coll₀ τ₂)
pf₂.
Proof.
Lemma SRec₀
k1 rl1 rl2 k2 pf1 pf2 : (
forall s r'
pf',
lookup string_dec rl2 s =
Some r' ->
exists r pf,
lookup string_dec rl1 s =
Some r /\
subtype (
exist _ r pf) (
exist _ r'
pf')) ->
(
k2 =
Closed ->
k1 =
Closed /\
(
forall s,
In s (
domain rl1) ->
In s (
domain rl2))) ->
exist (
fun τ₀ :
rtype₀ =>
wf_rtype₀ τ₀ =
true) (
Rec₀
k1 rl1)
pf1 <:
exist (
fun τ₀ :
rtype₀ =>
wf_rtype₀ τ₀ =
true) (
Rec₀
k2 rl2)
pf2.
Proof.
intros.
destruct (
from_Rec₀
rl1 pf1)
as [
l1' [
pf1' [
eq11 eq12]]].
destruct (
from_Rec₀
rl2 pf2)
as [
l2' [
pf2' [
eq21 eq22]]].
subst.
rewrite <-
eq12, <-
eq22.
apply SRec.
intros.
apply lookup_map_some in H1.
destruct (
H s _ (
proj2_sig r')
H1)
as [
r [
rpf [
l1 s1]]].
exists (
exist _ r rpf).
split.
apply lookup_map_some;
simpl.
auto.
destruct r';
simpl in *;
auto.
intuition.
specialize (
H3 s).
unfold domain in H3;
repeat rewrite map_map in H3.
simpl in H3.
auto.
Qed.
Lemma subtype_Rec_sublist {
k₁
l₁
pf₁
k₂
l₂
pf₂} :
Rec k₁
l₁
pf₁ <:
Rec k₂
l₂
pf₂ ->
sublist (
domain l₂) (
domain l₁).
Proof.
Lemma subtype_Rec_closed_domain {
k₁
l₁
pf₁
l₂
pf₂} :
Rec k₁
l₁
pf₁ <:
Rec Closed l₂
pf₂ -> (
domain l₂) = (
domain l₁).
Proof.
Lemma subtype_Rec_closed2_closed1 {
k1 l1 pf1 l2 pf2}:
Rec k1 l1 pf1 <:
Rec Closed l2 pf2 ->
k1 =
Closed.
Proof.
inversion 1; subst; intuition.
Qed.
Lemma is_list_sorted_in_cons_lookup_none {
B} {
b τ₃
s} (τ₁:
B) {
rl0 rl1 τ₀} (τ₂:
B)
(
pf1 : @
is_list_sorted string _ ODT_lt_dec (
domain ((
b, τ₃) ::
rl1)) =
true)
(
x : @
is_list_sorted string _ ODT_lt_dec (
domain ((
s, τ₁) ::
rl0)) =
true)
(
inn:
In (
b, τ₀)
rl0) :
lookup string_dec ((
b, τ₂) ::
rl1)
s =
None.
Proof.
Lemma Rec_subtype_In {
rl0 pf0 rl1 pf1 b τ₁ τ₂} :
Rec Open rl0 pf0 <:
Rec Open rl1 pf1 ->
In (
b, τ₁)
rl0 ->
In (
b, τ₂)
rl1 -> τ₁ <: τ₂.
Proof.
End RSubtypeProp.