Qcert.Basic.TypeSystem.RTypeMeetJoin
Section rtype_meetjoin.
Definition record_kind_rtype_join {B} (k₁ k₂:record_kind) (l₁ l₂:list (string × B))
:= match k₁, k₂ with
| Closed, Closed ⇒
if (domain l₁) == (domain l₂) then Closed else Open
| _, _ ⇒ Open
end.
Lemma record_kind_rtype_join_open_l {B} k l₁ l₂:
@record_kind_rtype_join B Open k l₁ l₂ = Open.
Lemma record_kind_rtype_join_open_r {B} k l₁ l₂:
@record_kind_rtype_join B k Open l₁ l₂ = Open.
Lemma record_kind_rtype_join_closed_inv {B} k₁ k₂ l₁ l₂:
@record_kind_rtype_join B k₁ k₂ l₁ l₂ = Closed →
k₁ = Closed ∧ k₂ = Closed ∧ domain l₁ = domain l₂.
Lemma record_kind_rtype_join_idempotent {B} k l :
@record_kind_rtype_join B k k l l = k.
Lemma record_kind_rtype_join_comm_kind {B} k₁ k₂ l₁ l₂ :
@record_kind_rtype_join B k₁ k₂ l₁ l₂ =
record_kind_rtype_join k₂ k₁ l₁ l₂.
Lemma record_kind_rtype_join_comm_list {B} k₁ k₂ l₁ l₂ :
@record_kind_rtype_join B k₁ k₂ l₁ l₂ =
record_kind_rtype_join k₁ k₂ l₂ l₁.
Lemma record_kind_rtype_join_comm {B} k₁ k₂ l₁ l₂ :
@record_kind_rtype_join B k₁ k₂ l₁ l₂ =
record_kind_rtype_join k₂ k₁ l₂ l₁.
Definition rtype_meet_compatible_records {A B} (k₁ k₂:record_kind)
(l₁:list (string×A)) (l₂:list (string × B)) : Prop
:= match k₁, k₂ with
| Open, Open ⇒ True
| Open, Closed ⇒ sublist (domain l₁) (domain l₂)
| Closed, Open ⇒ sublist (domain l₂) (domain l₁)
| Closed, Closed ⇒ (domain l₂) = (domain l₁)
end.
Lemma rtype_meet_compatible_records_dec {A B} (k₁ k₂:record_kind)
(l₁:list (string×A)) (l₂:list (string × B)) :
{rtype_meet_compatible_records k₁ k₂ l₁ l₂} + {¬ rtype_meet_compatible_records k₁ k₂ l₁ l₂}.
Definition record_kind_rtype_meet (k₁ k₂:record_kind)
:= match k₁, k₂ with
| Open, Open ⇒ Open
| _, _ ⇒ Closed
end.
Lemma rtype_meet_compatible_records_idempotent {B} k₁ k₂ r :
@rtype_meet_compatible_records B B k₁ k₂ r r.
Lemma record_kind_rtype_meet_idempotent k : record_kind_rtype_meet k k = k.
Lemma rtype_meet_compatible_records_commutative {A B} k₁ k₂ r₁ r₂:
@rtype_meet_compatible_records A B k₁ k₂ r₁ r₂ →
@rtype_meet_compatible_records B A k₂ k₁ r₂ r₁.
Lemma record_kind_rtype_meet_commutative k₁ k₂ : record_kind_rtype_meet k₁ k₂ = record_kind_rtype_meet k₂ k₁.
Lemma rtype_meet_compatible_records_domain_eq_l {A B C}
(k₁ k₂:record_kind) (l₁:list (string×A)) (l₁':list (string×B)) (l₂:list (string × C)) :
domain l₁ = domain l₁' →
rtype_meet_compatible_records k₁ k₂ l₁ l₂
= rtype_meet_compatible_records k₁ k₂ l₁' l₂.
Lemma rtype_meet_compatible_records_domain_eq_r {A B C}
(k₁ k₂:record_kind) (l₁:list (string×A)) (l₂:list (string×B)) (l₂':list (string × C)) :
domain l₂ = domain l₂' →
rtype_meet_compatible_records k₁ k₂ l₁ l₂
= rtype_meet_compatible_records k₁ k₂ l₁ l₂'.
Lemma record_kind_rtype_meet_associative k k0 k1 :
record_kind_rtype_meet (record_kind_rtype_meet k k0) k1
= record_kind_rtype_meet k (record_kind_rtype_meet k0 k1).
Section mj.
Context {ftype:foreign_type}.
Context {br:brand_relation}.
Fixpoint rtype_join₀ (τ₁ τ₂:rtype₀) : rtype₀
:= match τ₁, τ₂ with
| ⊥₀, τ ⇒ τ
| τ, ⊥₀ ⇒ τ
| Unit₀, Unit₀ ⇒ Unit₀
| Nat₀, Nat₀ ⇒ Nat₀
| Bool₀, Bool₀ ⇒ Bool₀
| String₀, String₀ ⇒ String₀
| Coll₀ τ₁', Coll₀ τ₂' ⇒ Coll₀ (rtype_join₀ τ₁' τ₂')
| Rec₀ k₁ srl, Rec₀ k₂ srl' ⇒ Rec₀ (record_kind_rtype_join k₁ k₂ srl srl')
((fix map_rtype_join₀ l1 l2 :=
match l1 with
| nil ⇒ nil
| (s,r)::srs ⇒ match lookup string_dec l2 s with
| None ⇒ map_rtype_join₀ srs l2
| Some r' ⇒ (s,rtype_join₀ r r')::(map_rtype_join₀ srs l2)
end
end) srl srl')
| Either₀ τl₁ τr₁, Either₀ τl₂ τr₂ ⇒ Either₀ (rtype_join₀ τl₁ τl₂) (rtype_join₀ τr₁ τr₂)
| Arrow₀ τl₁ τr₁, Arrow₀ τl₂ τr₂ ⇒ Arrow₀ (rtype_meet₀ τl₁ τl₂) (rtype_join₀ τr₁ τr₂)
| Brand₀ b₁, Brand₀ b₂ ⇒ Brand₀ (brand_join brand_relation_brands b₁ b₂)
| Foreign₀ ft₁, Foreign₀ ft₂ ⇒ Foreign₀ (join ft₁ ft₂)
| _, _ ⇒ ⊤₀
end
with rtype_meet₀ (τ₁ τ₂:rtype₀) : rtype₀
:= match τ₁, τ₂ with
| ⊤₀, τ ⇒ τ
| τ, ⊤₀ ⇒ τ
| Unit₀, Unit₀ ⇒ Unit₀
| Nat₀, Nat₀ ⇒ Nat₀
| Bool₀, Bool₀ ⇒ Bool₀
| String₀, String₀ ⇒ String₀
| Coll₀ τ₁', Coll₀ τ₂' ⇒ Coll₀ (rtype_meet₀ τ₁' τ₂')
| Rec₀ k₁ srl, Rec₀ k₂ srl' ⇒
if rtype_meet_compatible_records_dec k₁ k₂ srl srl'
then Rec₀ (record_kind_rtype_meet k₁ k₂)
(rec_concat_sort ((fix map_rtype_meet₀ l1 l2 :=
match l1 with
| nil ⇒ nil
| (s,r)::srs ⇒ match lookup string_dec l2 s with
| None ⇒ (s,r)::map_rtype_meet₀ srs l2
| Some r' ⇒ (s,rtype_meet₀ r r')::(map_rtype_meet₀ srs l2)
end
end) srl srl')
(lookup_diff string_dec srl' srl))
else ⊥₀
| Either₀ τl₁ τr₁, Either₀ τl₂ τr₂ ⇒
Either₀ (rtype_meet₀ τl₁ τl₂) (rtype_meet₀ τr₁ τr₂)
| Arrow₀ τl₁ τr₁, Arrow₀ τl₂ τr₂ ⇒ Arrow₀ (rtype_join₀ τl₁ τl₂) (rtype_meet₀ τr₁ τr₂)
| Brand₀ τ₁, Brand₀ τ₂ ⇒ Brand₀ (brand_meet brand_relation_brands τ₁ τ₂)
| Foreign₀ ft₁, Foreign₀ ft₂ ⇒ Foreign₀ (meet ft₁ ft₂)
| _, _ ⇒ ⊥₀
end.
Lemma map_rtype_join₀_domain_subset r srl x:
In x (domain (((fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r1) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_join₀ r1 r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) r srl))) → In x (domain r) ∧ In x (domain srl).
Lemma map_rtype_join₀_domain_subset_inv r srl x:
In x (domain r) ∧ In x (domain srl) →
In x (domain (((fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r1) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_join₀ r1 r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) r srl))).
Lemma map_rtype_join₀_rtype_joins {r₁ r₂ s τ₁ τ₂} :
lookup string_dec r₁ s = Some τ₁ →
lookup string_dec r₂ s = Some τ₂ →
lookup string_dec (((fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s, r) :: srs ⇒
match lookup string_dec l2 s with
| Some r' ⇒ (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) r₁ r₂)) s = Some (rtype_join₀ τ₁ τ₂).
Lemma NoDup_map_rtype_join₀ {r₁ r₂} :
NoDup (domain r₁) → NoDup (domain
((fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r1) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_join₀ r1 r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) r₁ r₂)).
Lemma map_rtype_meet₀_domain r srl:
(domain (((fix map_rtype_meet₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s,r)::srs ⇒ match lookup string_dec l2 s with
| None ⇒ (s,r)::map_rtype_meet₀ srs l2
| Some r' ⇒ (s,rtype_meet₀ r r')::(map_rtype_meet₀ srs l2)
end
end)
r srl))) = domain r.
Lemma map_rtype_meet₀_rtype_meets {r₁ r₂ s τ₁ τ₂} :
lookup string_dec r₁ s = Some τ₁ →
lookup string_dec r₂ s = Some τ₂ →
lookup string_dec (((fix map_rtype_meet₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s, r) :: srs ⇒
match lookup string_dec l2 s with
| Some r' ⇒ (s, rtype_meet₀ r r') :: map_rtype_meet₀ srs l2
| None ⇒ (s, r)::map_rtype_meet₀ srs l2
end
end) r₁ r₂)) s = Some (rtype_meet₀ τ₁ τ₂).
Lemma map_rtype_meet₀_some_none {r₁ r₂ s τ₁} :
lookup string_dec r₁ s = Some τ₁ →
lookup string_dec r₂ s = None →
lookup string_dec (((fix map_rtype_meet₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s, r) :: srs ⇒
match lookup string_dec l2 s with
| Some r' ⇒ (s, rtype_meet₀ r r') :: map_rtype_meet₀ srs l2
| None ⇒ (s, r)::map_rtype_meet₀ srs l2
end
end) r₁ r₂)) s = Some τ₁.
Lemma map_rtype_meet₀_none {r₁ r₂ s} :
lookup string_dec r₁ s = None →
lookup string_dec (((fix map_rtype_meet₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s, r) :: srs ⇒
match lookup string_dec l2 s with
| Some r' ⇒ (s, rtype_meet₀ r r') :: map_rtype_meet₀ srs l2
| None ⇒ (s, r)::map_rtype_meet₀ srs l2
end
end) r₁ r₂)) s = None.
Lemma map_rtype_meet₀_disjoint r₁ r₂ :
disjoint (domain ((fix map_rtype_meet₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s,r)::srs ⇒ match lookup string_dec l2 s with
| None ⇒ (s,r)::map_rtype_meet₀ srs l2
| Some r' ⇒ (s,rtype_meet₀ r r')::(map_rtype_meet₀ srs l2)
end
end) r₁ r₂)) (domain (lookup_diff string_dec r₂ r₁)).
Lemma NoDup_map_rtype_meet₀_lookup_diff {r₁ r₂} :
NoDup (domain r₁) →
NoDup (domain r₂) →
NoDup (domain
(((fix map_rtype_meet₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s,r)::srs ⇒ match lookup string_dec l2 s with
| None ⇒ (s,r)::map_rtype_meet₀ srs l2
| Some r' ⇒ (s,rtype_meet₀ r r')::(map_rtype_meet₀ srs l2)
end
end) r₁ r₂) ++ (lookup_diff string_dec r₂ r₁))).
Lemma map_rtype_meet₀_cons2_nin a b l1 l2 :
¬ In a (domain l1) →
((fix map_rtype_meet₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s, r2) :: srs ⇒
match lookup string_dec l2 s with
| Some r' ⇒ (s, rtype_meet₀ r2 r') :: map_rtype_meet₀ srs l2
| None ⇒ (s, r2) :: map_rtype_meet₀ srs l2
end
end) l1 ((a,b) :: l2))
=
((fix map_rtype_meet₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s, r) :: srs ⇒
match lookup string_dec l2 s with
| Some r' ⇒ (s, rtype_meet₀ r r') :: map_rtype_meet₀ srs l2
| None ⇒ (s, r) :: map_rtype_meet₀ srs l2
end
end) l1 l2).
Lemma rtype_join₀_meet₀_wf {τ₁ τ₂} :
wf_rtype₀ τ₁ = true →
wf_rtype₀ τ₂ = true →
wf_rtype₀ (rtype_join₀ τ₁ τ₂) = true
∧ wf_rtype₀ (rtype_meet₀ τ₁ τ₂) = true.
Corollary rtype_join₀_wf {τ₁ τ₂} :
wf_rtype₀ τ₁ = true →
wf_rtype₀ τ₂ = true →
wf_rtype₀ (rtype_join₀ τ₁ τ₂) = true.
Corollary rtype_meet₀_wf {τ₁ τ₂} :
wf_rtype₀ τ₁ = true →
wf_rtype₀ τ₂ = true →
wf_rtype₀ (rtype_meet₀ τ₁ τ₂) = true.
This definition does not reduce well. To reduce with it,
use autorewrite using rtype_join.
Program Definition rtype_join (τ₁ τ₂:rtype) : rtype
:= exist _ (rtype_join₀ τ₁ τ₂) (rtype_join₀_wf (proj2_sig τ₁) (proj2_sig τ₂)).
Program Definition rtype_meet (τ₁ τ₂:rtype) : rtype
:= exist _ (rtype_meet₀ τ₁ τ₂) (rtype_meet₀_wf (proj2_sig τ₁) (proj2_sig τ₂)).
Lemma map_rtype_join₀_lookup_none1 {l₁ l₂ s r} :
lookup string_dec l₂ s = None →
(fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r1) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_join₀ r1 r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) ((s, r)::l₁) l₂ =
(fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r1) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_join₀ r1 r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) l₁ l₂.
Lemma map_rtype_join₀_lookup_none2 {l₁ l₂ s r} :
lookup string_dec l₁ s = None →
(fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r1) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_join₀ r1 r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) l₁ ((s, r) :: l₂) =
(fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r1) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_join₀ r1 r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) l₁ l₂.
Lemma map_rtype_join₀_lookup_some2 {l₁ l₂ s τ₁ τ₂} :
lookup string_dec l₁ s = Some τ₁ →
is_list_sorted ODT_lt_dec (domain l₁) = true →
is_list_sorted ODT_lt_dec (domain ((s,τ₂)::l₂)) = true →
(fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r1) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_join₀ r1 r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) l₁ ((s, τ₂) :: l₂) =
(s, rtype_join₀ τ₁ τ₂)
:: (fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r1) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_join₀ r1 r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) l₁ l₂.
Lemma map_rtype_join₀_idempotent' k {rl1} :
∀ (wf1 : wf_rtype₀ (Rec₀ k rl1) = true)
(subH : Forall
(fun ab : string × rtype₀ ⇒
wf_rtype₀ (snd ab) = true →
rtype_join₀ (snd ab) (snd ab) = (snd ab)) rl1),
(fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s, r) :: srs ⇒
match lookup string_dec l2 s with
| Some r' ⇒ (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) rl1 rl1
= rl1.
Lemma rtype_join₀_meet₀_idempotent a :
wf_rtype₀ a = true →
rtype_join₀ a a = a
∧ rtype_meet₀ a a = a.
Corollary rtype_join₀_idempotent a:
∀ (awf:wf_rtype₀ a = true),
rtype_join₀ a a = a.
Corollary rtype_meet₀_idempotent a:
∀ (awf:wf_rtype₀ a = true),
rtype_meet₀ a a = a.
Theorem rtype_join_idempotent: ∀ a, rtype_join a a = a.
Theorem rtype_meet_idempotent a : rtype_meet a a = a.
Lemma map_rtype_join₀_idempotent k {rl1} :
∀ (wf1 : wf_rtype₀ (Rec₀ k rl1) = true),
(fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s, r) :: srs ⇒
match lookup string_dec l2 s with
| Some r' ⇒ (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) rl1 rl1
= rl1.
Lemma map_rtype_join₀_commutative' k₁ k₂ {rl1 rl2} :
∀ (wf1 : wf_rtype₀ (Rec₀ k₁ rl1) = true)
(wf2 : wf_rtype₀ (Rec₀ k₂ rl2) = true)
(subH : Forall
(fun ab : string × rtype₀ ⇒
∀ b : rtype₀,
wf_rtype₀ (snd ab) = true →
wf_rtype₀ b = true → rtype_join₀ (snd ab) b = rtype_join₀ b (snd ab)) rl1),
(fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s, r) :: srs ⇒
match lookup string_dec l2 s with
| Some r' ⇒ (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) rl1 rl2
= (fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s, r) :: srs ⇒
match lookup string_dec l2 s with
| Some r' ⇒ (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) rl2 rl1.
Lemma map_rtype_meet₀_lookup_none1 {l₁ l₂ s r} :
lookup string_dec l₂ s = None →
(fix map_rtype_meet₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r1) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_meet₀ r1 r') :: map_rtype_meet₀ srs l2
| None ⇒ map_rtype_meet₀ srs l2
end
end) ((s, r)::l₁) l₂ =
(fix map_rtype_meet₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r1) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_meet₀ r1 r') :: map_rtype_meet₀ srs l2
| None ⇒ map_rtype_meet₀ srs l2
end
end) l₁ l₂.
Lemma map_rtype_meet₀_lookup_none2 {l₁ l₂ s r} :
lookup string_dec l₁ s = None →
(fix map_rtype_meet₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r1) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_meet₀ r1 r') :: map_rtype_meet₀ srs l2
| None ⇒ map_rtype_meet₀ srs l2
end
end) l₁ ((s, r) :: l₂) =
(fix map_rtype_meet₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r1) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_meet₀ r1 r') :: map_rtype_meet₀ srs l2
| None ⇒ map_rtype_meet₀ srs l2
end
end) l₁ l₂.
Lemma map_rtype_meet₀_lookup_some2 {l₁ l₂ s τ₁ τ₂} :
lookup string_dec l₁ s = Some τ₁ →
is_list_sorted ODT_lt_dec (domain l₁) = true →
is_list_sorted ODT_lt_dec (domain ((s,τ₂)::l₂)) = true →
(fix map_rtype_meet₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r1) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_meet₀ r1 r') :: map_rtype_meet₀ srs l2
| None ⇒ map_rtype_meet₀ srs l2
end
end) l₁ ((s, τ₂) :: l₂) =
(s, rtype_meet₀ τ₁ τ₂)
:: (fix map_rtype_meet₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r1) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_meet₀ r1 r') :: map_rtype_meet₀ srs l2
| None ⇒ map_rtype_meet₀ srs l2
end
end) l₁ l₂.
Lemma rtype_join₀_meet₀_commutative a b:
∀ (awf : wf_rtype₀ a = true)
(bwf : wf_rtype₀ b = true),
rtype_join₀ a b = rtype_join₀ b a
∧ rtype_meet₀ a b = rtype_meet₀ b a.
Corollary rtype_join₀_commutative a b:
∀ (awf : wf_rtype₀ a = true)
(bwf : wf_rtype₀ b = true),
rtype_join₀ a b = rtype_join₀ b a.
Corollary rtype_meet₀_commutative a b:
∀ (awf : wf_rtype₀ a = true)
(bwf : wf_rtype₀ b = true),
rtype_meet₀ a b = rtype_meet₀ b a.
Theorem rtype_join_commutative: ∀ a b, rtype_join a b = rtype_join b a.
Theorem rtype_meet_commutative: ∀ a b, rtype_meet a b = rtype_meet b a.
Lemma map_rtype_join₀_commutative k₁ k₂ {rl1 rl2} :
∀ (wf1 : wf_rtype₀ (Rec₀ k₁ rl1) = true)
(wf2 : wf_rtype₀ (Rec₀ k₂ rl2) = true),
(fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s, r) :: srs ⇒
match lookup string_dec l2 s with
| Some r' ⇒ (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) rl1 rl2
= (fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s, r) :: srs ⇒
match lookup string_dec l2 s with
| Some r' ⇒ (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) rl2 rl1.
Lemma map_rtype_join₀_lookup_rtype_join {l₁ l₂ s τ₁ τ₂} :
lookup string_dec l₁ s = Some τ₁ →
lookup string_dec l₂ s = Some τ₂ →
lookup string_dec (((fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r1) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_join₀ r1 r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) l₁ l₂)) s = Some (rtype_join₀ τ₁ τ₂).
Lemma map_rtype_join₀_lookup_none1_rtype_join {l₁ l₂ s} :
lookup string_dec l₁ s = None →
lookup string_dec (((fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r1) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_join₀ r1 r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) l₁ l₂)) s = None.
Lemma map_rtype_join₀_lookup_none2_rtype_join {l₁ l₂ s} :
lookup string_dec l₂ s = None →
lookup string_dec (((fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r1) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_join₀ r1 r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) l₁ l₂)) s = None.
Lemma map_rtype_join₀_domain_sublist a b :
sublist (domain ((fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} : list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s, r) :: srs ⇒
match lookup string_dec l2 s with
| Some r' ⇒ (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) a b)) (domain a).
Lemma map_rtype_join₀_domain_is_list_sorted {a b} :
is_list_sorted ODT_lt_dec (domain a) = true →
is_list_sorted ODT_lt_dec (domain ((fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s, r) :: srs ⇒
match lookup string_dec l2 s with
| Some r' ⇒ (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) a b)) = true.
Lemma map_rtype_join₀_domain {a b}:
is_list_sorted ODT_lt_dec (domain a) = true →
is_list_sorted ODT_lt_dec (domain b) = true →
domain a = domain b →
domain ((fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s, r) :: srs ⇒
match lookup string_dec l2 s with
| Some r' ⇒ (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) a b) = domain a.
Lemma record_kind_rtype_join_associative {k k0 k1 a b c}:
wf_rtype₀ (Rec₀ k a) = true →
wf_rtype₀ (Rec₀ k0 b) = true →
wf_rtype₀ (Rec₀ k1 c) = true →
(record_kind_rtype_join (record_kind_rtype_join k k0 a b) k1
((fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s, r) :: srs ⇒
match lookup string_dec l2 s with
| Some r' ⇒ (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) a b) c) =
(record_kind_rtype_join k (record_kind_rtype_join k0 k1 b c) a
((fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s, r) :: srs ⇒
match lookup string_dec l2 s with
| Some r' ⇒ (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) b c)).
Lemma domain_map_rtype_meet₀_diff r srl :
domain (rec_concat_sort
((fix map_rtype_meet₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s, r) :: srs ⇒
match lookup string_dec l2 s with
| Some r' ⇒ (s, rtype_meet₀ r r') :: map_rtype_meet₀ srs l2
| None ⇒ (s, r) :: map_rtype_meet₀ srs l2
end
end) r srl) (lookup_diff string_dec srl r)) =
domain (rec_concat_sort r srl).
Lemma NoDup_domain_lookups_Permutation {A B : Type} dec (l l' : list (A×B)) :
NoDup (domain l) →
NoDup (domain l') →
(∀ x : A, lookup dec l x = lookup dec l' x) →
Permutation l l'.
Lemma lookup_nodup_perm {A B : Type}
(dec : ∀ a a' : A, {a = a'} + {a ≠ a'})
(l l' : list (A × B)) (a : A) :
NoDup (domain l) →
Permutation l l' →
lookup dec l a = lookup dec l' a.
Lemma map_rtype_meet₀_domain_rec_concat_sort r srl s :
NoDup (domain r) →
NoDup (domain srl) →
lookup string_dec (rec_concat_sort ((fix map_rtype_meet₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r0) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_meet₀ r0 r') :: map_rtype_meet₀ srs l2
| None ⇒ (s0, r0) :: map_rtype_meet₀ srs l2
end
end) r srl) (lookup_diff string_dec srl r)) s
= lookup string_dec (((fix map_rtype_meet₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r0) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_meet₀ r0 r') :: map_rtype_meet₀ srs l2
| None ⇒ (s0, r0) :: map_rtype_meet₀ srs l2
end
end) r srl) ++ (lookup_diff string_dec srl r)) s.
Lemma map_rtype_join₀_associative' {k k0 k1 a b c}:
Forall
(fun ab : string × rtype₀ ⇒
∀ b c : rtype₀,
wf_rtype₀ (snd ab) = true →
wf_rtype₀ b = true →
wf_rtype₀ c = true →
rtype_join₀ (rtype_join₀ (snd ab) b) c = rtype_join₀ (snd ab) (rtype_join₀ b c)) a →
wf_rtype₀ (Rec₀ k a) = true →
wf_rtype₀ (Rec₀ k0 b) = true →
wf_rtype₀ (Rec₀ k1 c) = true →
rtype_join₀ (rtype_join₀ (Rec₀ k a) (Rec₀ k0 b)) (Rec₀ k1 c) =
rtype_join₀ (Rec₀ k a) (rtype_join₀ (Rec₀ k0 b) (Rec₀ k1 c)).
Lemma rtype_join₀_meet₀_associative {a b c : rtype₀} :
wf_rtype₀ a = true →
wf_rtype₀ b = true →
wf_rtype₀ c = true →
rtype_join₀ (rtype_join₀ a b) c = rtype_join₀ a (rtype_join₀ b c)
∧ rtype_meet₀ (rtype_meet₀ a b) c = rtype_meet₀ a (rtype_meet₀ b c).
Corollary rtype_join₀_associative {a b c : rtype₀} :
wf_rtype₀ a = true →
wf_rtype₀ b = true →
wf_rtype₀ c = true →
rtype_join₀ (rtype_join₀ a b) c = rtype_join₀ a (rtype_join₀ b c).
Corollary rtype_meet₀_associative {a b c : rtype₀} :
wf_rtype₀ a = true →
wf_rtype₀ b = true →
wf_rtype₀ c = true →
rtype_meet₀ (rtype_meet₀ a b) c = rtype_meet₀ a (rtype_meet₀ b c).
Theorem rtype_join_associative : ∀ a b c,
rtype_join (rtype_join a b) c = rtype_join a (rtype_join b c).
Theorem rtype_meet_associative : ∀ a b c,
rtype_meet (rtype_meet a b) c = rtype_meet a (rtype_meet b c).
Lemma map_rtype_join₀_nil_r l₁ :
((fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s, r) :: srs ⇒
match lookup string_dec l2 s with
| Some r' ⇒ (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) l₁ nil) = nil.
End mj.
End rtype_meetjoin.
Section rtype_join_re.
:= exist _ (rtype_join₀ τ₁ τ₂) (rtype_join₀_wf (proj2_sig τ₁) (proj2_sig τ₂)).
Program Definition rtype_meet (τ₁ τ₂:rtype) : rtype
:= exist _ (rtype_meet₀ τ₁ τ₂) (rtype_meet₀_wf (proj2_sig τ₁) (proj2_sig τ₂)).
Lemma map_rtype_join₀_lookup_none1 {l₁ l₂ s r} :
lookup string_dec l₂ s = None →
(fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r1) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_join₀ r1 r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) ((s, r)::l₁) l₂ =
(fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r1) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_join₀ r1 r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) l₁ l₂.
Lemma map_rtype_join₀_lookup_none2 {l₁ l₂ s r} :
lookup string_dec l₁ s = None →
(fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r1) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_join₀ r1 r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) l₁ ((s, r) :: l₂) =
(fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r1) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_join₀ r1 r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) l₁ l₂.
Lemma map_rtype_join₀_lookup_some2 {l₁ l₂ s τ₁ τ₂} :
lookup string_dec l₁ s = Some τ₁ →
is_list_sorted ODT_lt_dec (domain l₁) = true →
is_list_sorted ODT_lt_dec (domain ((s,τ₂)::l₂)) = true →
(fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r1) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_join₀ r1 r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) l₁ ((s, τ₂) :: l₂) =
(s, rtype_join₀ τ₁ τ₂)
:: (fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r1) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_join₀ r1 r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) l₁ l₂.
Lemma map_rtype_join₀_idempotent' k {rl1} :
∀ (wf1 : wf_rtype₀ (Rec₀ k rl1) = true)
(subH : Forall
(fun ab : string × rtype₀ ⇒
wf_rtype₀ (snd ab) = true →
rtype_join₀ (snd ab) (snd ab) = (snd ab)) rl1),
(fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s, r) :: srs ⇒
match lookup string_dec l2 s with
| Some r' ⇒ (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) rl1 rl1
= rl1.
Lemma rtype_join₀_meet₀_idempotent a :
wf_rtype₀ a = true →
rtype_join₀ a a = a
∧ rtype_meet₀ a a = a.
Corollary rtype_join₀_idempotent a:
∀ (awf:wf_rtype₀ a = true),
rtype_join₀ a a = a.
Corollary rtype_meet₀_idempotent a:
∀ (awf:wf_rtype₀ a = true),
rtype_meet₀ a a = a.
Theorem rtype_join_idempotent: ∀ a, rtype_join a a = a.
Theorem rtype_meet_idempotent a : rtype_meet a a = a.
Lemma map_rtype_join₀_idempotent k {rl1} :
∀ (wf1 : wf_rtype₀ (Rec₀ k rl1) = true),
(fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s, r) :: srs ⇒
match lookup string_dec l2 s with
| Some r' ⇒ (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) rl1 rl1
= rl1.
Lemma map_rtype_join₀_commutative' k₁ k₂ {rl1 rl2} :
∀ (wf1 : wf_rtype₀ (Rec₀ k₁ rl1) = true)
(wf2 : wf_rtype₀ (Rec₀ k₂ rl2) = true)
(subH : Forall
(fun ab : string × rtype₀ ⇒
∀ b : rtype₀,
wf_rtype₀ (snd ab) = true →
wf_rtype₀ b = true → rtype_join₀ (snd ab) b = rtype_join₀ b (snd ab)) rl1),
(fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s, r) :: srs ⇒
match lookup string_dec l2 s with
| Some r' ⇒ (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) rl1 rl2
= (fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s, r) :: srs ⇒
match lookup string_dec l2 s with
| Some r' ⇒ (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) rl2 rl1.
Lemma map_rtype_meet₀_lookup_none1 {l₁ l₂ s r} :
lookup string_dec l₂ s = None →
(fix map_rtype_meet₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r1) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_meet₀ r1 r') :: map_rtype_meet₀ srs l2
| None ⇒ map_rtype_meet₀ srs l2
end
end) ((s, r)::l₁) l₂ =
(fix map_rtype_meet₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r1) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_meet₀ r1 r') :: map_rtype_meet₀ srs l2
| None ⇒ map_rtype_meet₀ srs l2
end
end) l₁ l₂.
Lemma map_rtype_meet₀_lookup_none2 {l₁ l₂ s r} :
lookup string_dec l₁ s = None →
(fix map_rtype_meet₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r1) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_meet₀ r1 r') :: map_rtype_meet₀ srs l2
| None ⇒ map_rtype_meet₀ srs l2
end
end) l₁ ((s, r) :: l₂) =
(fix map_rtype_meet₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r1) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_meet₀ r1 r') :: map_rtype_meet₀ srs l2
| None ⇒ map_rtype_meet₀ srs l2
end
end) l₁ l₂.
Lemma map_rtype_meet₀_lookup_some2 {l₁ l₂ s τ₁ τ₂} :
lookup string_dec l₁ s = Some τ₁ →
is_list_sorted ODT_lt_dec (domain l₁) = true →
is_list_sorted ODT_lt_dec (domain ((s,τ₂)::l₂)) = true →
(fix map_rtype_meet₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r1) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_meet₀ r1 r') :: map_rtype_meet₀ srs l2
| None ⇒ map_rtype_meet₀ srs l2
end
end) l₁ ((s, τ₂) :: l₂) =
(s, rtype_meet₀ τ₁ τ₂)
:: (fix map_rtype_meet₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r1) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_meet₀ r1 r') :: map_rtype_meet₀ srs l2
| None ⇒ map_rtype_meet₀ srs l2
end
end) l₁ l₂.
Lemma rtype_join₀_meet₀_commutative a b:
∀ (awf : wf_rtype₀ a = true)
(bwf : wf_rtype₀ b = true),
rtype_join₀ a b = rtype_join₀ b a
∧ rtype_meet₀ a b = rtype_meet₀ b a.
Corollary rtype_join₀_commutative a b:
∀ (awf : wf_rtype₀ a = true)
(bwf : wf_rtype₀ b = true),
rtype_join₀ a b = rtype_join₀ b a.
Corollary rtype_meet₀_commutative a b:
∀ (awf : wf_rtype₀ a = true)
(bwf : wf_rtype₀ b = true),
rtype_meet₀ a b = rtype_meet₀ b a.
Theorem rtype_join_commutative: ∀ a b, rtype_join a b = rtype_join b a.
Theorem rtype_meet_commutative: ∀ a b, rtype_meet a b = rtype_meet b a.
Lemma map_rtype_join₀_commutative k₁ k₂ {rl1 rl2} :
∀ (wf1 : wf_rtype₀ (Rec₀ k₁ rl1) = true)
(wf2 : wf_rtype₀ (Rec₀ k₂ rl2) = true),
(fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s, r) :: srs ⇒
match lookup string_dec l2 s with
| Some r' ⇒ (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) rl1 rl2
= (fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s, r) :: srs ⇒
match lookup string_dec l2 s with
| Some r' ⇒ (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) rl2 rl1.
Lemma map_rtype_join₀_lookup_rtype_join {l₁ l₂ s τ₁ τ₂} :
lookup string_dec l₁ s = Some τ₁ →
lookup string_dec l₂ s = Some τ₂ →
lookup string_dec (((fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r1) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_join₀ r1 r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) l₁ l₂)) s = Some (rtype_join₀ τ₁ τ₂).
Lemma map_rtype_join₀_lookup_none1_rtype_join {l₁ l₂ s} :
lookup string_dec l₁ s = None →
lookup string_dec (((fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r1) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_join₀ r1 r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) l₁ l₂)) s = None.
Lemma map_rtype_join₀_lookup_none2_rtype_join {l₁ l₂ s} :
lookup string_dec l₂ s = None →
lookup string_dec (((fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r1) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_join₀ r1 r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) l₁ l₂)) s = None.
Lemma map_rtype_join₀_domain_sublist a b :
sublist (domain ((fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} : list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s, r) :: srs ⇒
match lookup string_dec l2 s with
| Some r' ⇒ (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) a b)) (domain a).
Lemma map_rtype_join₀_domain_is_list_sorted {a b} :
is_list_sorted ODT_lt_dec (domain a) = true →
is_list_sorted ODT_lt_dec (domain ((fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s, r) :: srs ⇒
match lookup string_dec l2 s with
| Some r' ⇒ (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) a b)) = true.
Lemma map_rtype_join₀_domain {a b}:
is_list_sorted ODT_lt_dec (domain a) = true →
is_list_sorted ODT_lt_dec (domain b) = true →
domain a = domain b →
domain ((fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s, r) :: srs ⇒
match lookup string_dec l2 s with
| Some r' ⇒ (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) a b) = domain a.
Lemma record_kind_rtype_join_associative {k k0 k1 a b c}:
wf_rtype₀ (Rec₀ k a) = true →
wf_rtype₀ (Rec₀ k0 b) = true →
wf_rtype₀ (Rec₀ k1 c) = true →
(record_kind_rtype_join (record_kind_rtype_join k k0 a b) k1
((fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s, r) :: srs ⇒
match lookup string_dec l2 s with
| Some r' ⇒ (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) a b) c) =
(record_kind_rtype_join k (record_kind_rtype_join k0 k1 b c) a
((fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s, r) :: srs ⇒
match lookup string_dec l2 s with
| Some r' ⇒ (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) b c)).
Lemma domain_map_rtype_meet₀_diff r srl :
domain (rec_concat_sort
((fix map_rtype_meet₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s, r) :: srs ⇒
match lookup string_dec l2 s with
| Some r' ⇒ (s, rtype_meet₀ r r') :: map_rtype_meet₀ srs l2
| None ⇒ (s, r) :: map_rtype_meet₀ srs l2
end
end) r srl) (lookup_diff string_dec srl r)) =
domain (rec_concat_sort r srl).
Lemma NoDup_domain_lookups_Permutation {A B : Type} dec (l l' : list (A×B)) :
NoDup (domain l) →
NoDup (domain l') →
(∀ x : A, lookup dec l x = lookup dec l' x) →
Permutation l l'.
Lemma lookup_nodup_perm {A B : Type}
(dec : ∀ a a' : A, {a = a'} + {a ≠ a'})
(l l' : list (A × B)) (a : A) :
NoDup (domain l) →
Permutation l l' →
lookup dec l a = lookup dec l' a.
Lemma map_rtype_meet₀_domain_rec_concat_sort r srl s :
NoDup (domain r) →
NoDup (domain srl) →
lookup string_dec (rec_concat_sort ((fix map_rtype_meet₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r0) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_meet₀ r0 r') :: map_rtype_meet₀ srs l2
| None ⇒ (s0, r0) :: map_rtype_meet₀ srs l2
end
end) r srl) (lookup_diff string_dec srl r)) s
= lookup string_dec (((fix map_rtype_meet₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s0, r0) :: srs ⇒
match lookup string_dec l2 s0 with
| Some r' ⇒ (s0, rtype_meet₀ r0 r') :: map_rtype_meet₀ srs l2
| None ⇒ (s0, r0) :: map_rtype_meet₀ srs l2
end
end) r srl) ++ (lookup_diff string_dec srl r)) s.
Lemma map_rtype_join₀_associative' {k k0 k1 a b c}:
Forall
(fun ab : string × rtype₀ ⇒
∀ b c : rtype₀,
wf_rtype₀ (snd ab) = true →
wf_rtype₀ b = true →
wf_rtype₀ c = true →
rtype_join₀ (rtype_join₀ (snd ab) b) c = rtype_join₀ (snd ab) (rtype_join₀ b c)) a →
wf_rtype₀ (Rec₀ k a) = true →
wf_rtype₀ (Rec₀ k0 b) = true →
wf_rtype₀ (Rec₀ k1 c) = true →
rtype_join₀ (rtype_join₀ (Rec₀ k a) (Rec₀ k0 b)) (Rec₀ k1 c) =
rtype_join₀ (Rec₀ k a) (rtype_join₀ (Rec₀ k0 b) (Rec₀ k1 c)).
Lemma rtype_join₀_meet₀_associative {a b c : rtype₀} :
wf_rtype₀ a = true →
wf_rtype₀ b = true →
wf_rtype₀ c = true →
rtype_join₀ (rtype_join₀ a b) c = rtype_join₀ a (rtype_join₀ b c)
∧ rtype_meet₀ (rtype_meet₀ a b) c = rtype_meet₀ a (rtype_meet₀ b c).
Corollary rtype_join₀_associative {a b c : rtype₀} :
wf_rtype₀ a = true →
wf_rtype₀ b = true →
wf_rtype₀ c = true →
rtype_join₀ (rtype_join₀ a b) c = rtype_join₀ a (rtype_join₀ b c).
Corollary rtype_meet₀_associative {a b c : rtype₀} :
wf_rtype₀ a = true →
wf_rtype₀ b = true →
wf_rtype₀ c = true →
rtype_meet₀ (rtype_meet₀ a b) c = rtype_meet₀ a (rtype_meet₀ b c).
Theorem rtype_join_associative : ∀ a b c,
rtype_join (rtype_join a b) c = rtype_join a (rtype_join b c).
Theorem rtype_meet_associative : ∀ a b c,
rtype_meet (rtype_meet a b) c = rtype_meet a (rtype_meet b c).
Lemma map_rtype_join₀_nil_r l₁ :
((fix map_rtype_join₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s, r) :: srs ⇒
match lookup string_dec l2 s with
| Some r' ⇒ (s, rtype_join₀ r r') :: map_rtype_join₀ srs l2
| None ⇒ map_rtype_join₀ srs l2
end
end) l₁ nil) = nil.
End mj.
End rtype_meetjoin.
Section rtype_join_re.
since rtype_join does not reduce nicely, we define a bunch of reduction equations
these will then be added in to the rtype_join autorewrite database
Lemma rtype_nequal {ftype:foreign_type} {br:brand_relation} {τ₁ τ₂:rtype} : τ₁ ≠ τ₂ → proj1_sig τ₁ ≠ proj1_sig τ₂.
Context {ftype:foreign_type}.
Context {m:brand_relation}.
Lemma rtype_join_Top_l τ :
rtype_join ⊤ τ = ⊤.
Lemma rtype_join_Top_r τ : rtype_join τ ⊤ = ⊤.
Lemma rtype_join_Bottom_r τ : rtype_join τ ⊥ = τ.
Lemma rtype_join_Bottom_l τ : rtype_join ⊥ τ = τ.
Lemma rtype_join_Unit_eq : rtype_join Unit Unit = Unit.
Lemma rtype_join_Unit_neq_l τ: τ ≠ ⊥ → τ ≠ Unit → rtype_join Unit τ = ⊤.
Lemma rtype_join_Unit_neq_r τ: τ ≠ ⊥ → τ ≠ Unit → rtype_join τ Unit = ⊤.
Lemma rtype_join_Nat_eq : rtype_join Nat Nat = Nat.
Lemma rtype_join_Nat_neq_l τ: τ ≠ ⊥ → τ ≠ Nat → rtype_join Nat τ = ⊤.
Lemma rtype_join_Nat_neq_r τ: τ ≠ ⊥ → τ ≠ Nat → rtype_join τ Nat = ⊤.
Lemma rtype_join_Bool_eq : rtype_join Bool Bool = Bool.
Lemma rtype_join_Bool_neq_l τ: τ ≠ ⊥ → τ ≠ Bool → rtype_join Bool τ = ⊤.
Lemma rtype_join_Bool_neq_r τ: τ ≠ ⊥ → τ ≠ Bool → rtype_join τ Bool = ⊤.
Lemma rtype_join_String_eq : rtype_join String String = String.
Lemma rtype_join_String_neq_l τ: τ ≠ ⊥ → τ ≠ String → rtype_join String τ = ⊤.
Lemma rtype_join_String_neq_r τ: τ ≠ ⊥ → τ ≠ String → rtype_join τ String = ⊤.
Lemma rtype_join_Coll_eq τ₁ τ₂ : rtype_join (Coll τ₁) (Coll τ₂) = Coll (rtype_join τ₁ τ₂).
Lemma rtype_join_Coll_neq_l τ τ₃: τ ≠ ⊥ → (∀ τ₂, τ ≠ Coll τ₂) → rtype_join (Coll τ₃) τ = ⊤.
Lemma rtype_join_Coll_neq_r τ τ₃: τ ≠ ⊥ → (∀ τ₂, τ ≠ Coll τ₂) → rtype_join τ (Coll τ₃) = ⊤.
Fixpoint map_rtype_join l1 l2 :=
match l1 with
| nil ⇒ nil
| (s,r)::srs ⇒ match lookup string_dec l2 s with
| None ⇒ map_rtype_join srs l2
| Some r' ⇒ (s,rtype_join r r')::(map_rtype_join srs l2)
end
end.
Lemma map_rtype_join_sublist_l l₁ l₂ : sublist (domain (map_rtype_join l₁ l₂)) (domain l₁).
Lemma map_rtype_join_is_sorted l₁ l₂ :
is_list_sorted ODT_lt_dec (domain l₁) = true
→ is_list_sorted ODT_lt_dec (domain (map_rtype_join l₁ l₂)) = true.
Lemma rtype_join_Rec_eq k₁ rl₁ pf₁ k₂ rl₂ pf₂ :
rtype_join (Rec k₁ rl₁ pf₁) (Rec k₂ rl₂ pf₂) =
Rec (record_kind_rtype_join k₁ k₂ rl₁ rl₂)
(map_rtype_join rl₁ rl₂) (map_rtype_join_is_sorted rl₁ rl₂ pf₁).
Lemma rtype_join_Rec_neq_l τ k rl pf :
τ ≠ ⊥ → (∀ k₂ rl₂ pf₂, τ ≠ Rec k₂ rl₂ pf₂) → rtype_join (Rec k rl pf) τ = ⊤.
Lemma rtype_join_Rec_neq_r τ k rl pf :
τ ≠ ⊥ → (∀ k₂ rl₂ pf₂, τ ≠ Rec k₂ rl₂ pf₂) → rtype_join τ (Rec k rl pf) = ⊤.
Lemma rtype_join_Either_eq τl₁ τr₁ τl₂ τr₂ : rtype_join (Either τl₁ τr₁) (Either τl₂ τr₂) = Either (rtype_join τl₁ τl₂) (rtype_join τr₁ τr₂).
Lemma rtype_join_Either_neq_l τ τl τr: τ ≠ ⊥ → (∀ τl₂ τr₂, τ ≠ Either τl₂ τr₂) → rtype_join (Either τl τr) τ = ⊤.
Lemma rtype_join_Either_neq_r τ τl τr: τ ≠ ⊥ → (∀ τl₂ τr₂, τ ≠ Either τl₂ τr₂) → rtype_join τ (Either τl τr) = ⊤.
Lemma rtype_join_Brand_eq x y : rtype_join (Brand x) (Brand y) = Brand (brand_join brand_relation_brands x y).
Lemma rtype_join_Brand_neq_l τ y: τ ≠ ⊥ → (∀ x, τ ≠ Brand x) → rtype_join (Brand y) τ = ⊤.
Lemma rtype_join_Brand_neq_r τ y: τ ≠ ⊥ → (∀ x, τ ≠ Brand x) → rtype_join τ (Brand y) = ⊤.
Lemma rtype_join_Foreign_eq x y : rtype_join (Foreign x) (Foreign y) = Foreign (join x y).
Lemma rtype_join_Foreign_neq_l τ y: τ ≠ ⊥ → (∀ x, τ ≠ Foreign x) → rtype_join (Foreign y) τ = ⊤.
Lemma rtype_join_Foreign_neq_r τ y: τ ≠ ⊥ → (∀ x, τ ≠ Foreign x) → rtype_join τ (Foreign y) = ⊤.
End rtype_join_re.
Section rtype_meet_re.
since rtype_meet does not reduce nicely, we define a bunch of reduction equations
these will then be added in to the rtype_meet autorewrite database
Context {ftype:foreign_type}.
Context {m:brand_relation}.
Lemma rtype_meet_Top_l τ :
rtype_meet ⊤ τ = τ.
Lemma rtype_meet_Top_r τ : rtype_meet τ ⊤ = τ.
Lemma rtype_meet_Bottom_r τ : rtype_meet τ ⊥ = ⊥.
Lemma rtype_meet_Bottom_l τ : rtype_meet ⊥ τ = ⊥.
Lemma rtype_meet_Unit_eq : rtype_meet Unit Unit = Unit.
Lemma rtype_meet_Unit_neq_l τ: τ ≠ ⊤ → τ ≠ Unit → rtype_meet Unit τ = ⊥.
Lemma rtype_meet_Unit_neq_r τ: τ ≠ ⊤ → τ ≠ Unit → rtype_meet τ Unit = ⊥.
Lemma rtype_meet_Nat_eq : rtype_meet Nat Nat = Nat.
Lemma rtype_meet_Nat_neq_l τ: τ ≠ ⊤ → τ ≠ Nat → rtype_meet Nat τ = ⊥.
Lemma rtype_meet_Nat_neq_r τ: τ ≠ ⊤ → τ ≠ Nat → rtype_meet τ Nat = ⊥.
Lemma rtype_meet_Bool_eq : rtype_meet Bool Bool = Bool.
Lemma rtype_meet_Bool_neq_l τ: τ ≠ ⊤ → τ ≠ Bool → rtype_meet Bool τ = ⊥.
Lemma rtype_meet_Bool_neq_r τ: τ ≠ ⊤ → τ ≠ Bool → rtype_meet τ Bool = ⊥.
Lemma rtype_meet_String_eq : rtype_meet String String = String.
Lemma rtype_meet_String_neq_l τ: τ ≠ ⊤ → τ ≠ String → rtype_meet String τ = ⊥.
Lemma rtype_meet_String_neq_r τ: τ ≠ ⊤ → τ ≠ String → rtype_meet τ String = ⊥.
Lemma rtype_meet_Coll_eq τ₁ τ₂ : rtype_meet (Coll τ₁) (Coll τ₂) = Coll (rtype_meet τ₁ τ₂).
Lemma rtype_meet_Coll_neq_l τ τ₃: τ ≠ ⊤ → (∀ τ₂, τ ≠ Coll τ₂) → rtype_meet (Coll τ₃) τ = ⊥.
Lemma rtype_meet_Coll_neq_r τ τ₃: τ ≠ ⊤ → (∀ τ₂, τ ≠ Coll τ₂) → rtype_meet τ (Coll τ₃) = ⊥.
Fixpoint map_rtype_meet l1 l2 :=
match l1 with
| nil ⇒ nil
| (s,r)::srs ⇒ match lookup string_dec l2 s with
| None ⇒ (s,r)::map_rtype_meet srs l2
| Some r' ⇒ (s,rtype_meet r r')::(map_rtype_meet srs l2)
end
end.
Lemma map_rtype_meet_domain r srl:
domain (map_rtype_meet r srl) = domain r.
Lemma NoDup_map_rtype_meet_lookup_diff {r₁ r₂} :
NoDup (domain r₁) →
NoDup (domain r₂) →
NoDup (domain
((map_rtype_meet r₁ r₂) ++ (lookup_diff string_dec r₂ r₁))).
Lemma map_rtype_meet_sublist_l l₁ l₂ : sublist (domain (map_rtype_meet l₁ l₂)) (domain l₁).
Lemma map_rtype_meet_eq
(rl₁ rl₂ : list (string × rtype)) :
(fix map_rtype_meet₀ (l1 l2 : list (string × rtype₀)) {struct l1} :
list (string × rtype₀) :=
match l1 with
| nil ⇒ nil
| (s, r) :: srs ⇒
match lookup string_dec l2 s with
| Some r' ⇒ (s, rtype_meet₀ r r') :: map_rtype_meet₀ srs l2
| None ⇒ (s, r) :: map_rtype_meet₀ srs l2
end
end)
(map
(fun x : string × {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} ⇒
(fst x, proj1_sig (snd x))) rl₁)
(map
(fun x : string × {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} ⇒
(fst x, proj1_sig (snd x))) rl₂) =
map
(fun x : string × {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} ⇒
(fst x, proj1_sig (snd x))) (map_rtype_meet rl₁ rl₂).
Lemma rtype_meet_Rec_eq k₁ rl₁ pf₁ k₂ rl₂ pf₂ :
rtype_meet (Rec k₁ rl₁ pf₁) (Rec k₂ rl₂ pf₂) =
if rtype_meet_compatible_records_dec k₁ k₂ rl₁ rl₂
then
Rec (record_kind_rtype_meet k₁ k₂)
(rec_concat_sort (map_rtype_meet rl₁ rl₂) (lookup_diff string_dec rl₂ rl₁)) (drec_concat_sort_sorted _ _)
else ⊥.
Lemma rtype_meet_Rec_neq_l τ k rl pf :
τ ≠ ⊤ → (∀ k₂ rl₂ pf₂, τ ≠ Rec k₂ rl₂ pf₂) → rtype_meet (Rec k rl pf) τ = ⊥.
Lemma rtype_meet_Rec_neq_r τ k rl pf :
τ ≠ ⊤ → (∀ k₂ rl₂ pf₂, τ ≠ Rec k₂ rl₂ pf₂) → rtype_meet τ (Rec k rl pf) = ⊥.
Lemma rtype_meet_Either_eq τl₁ τr₁ τl₂ τr₂ : rtype_meet (Either τl₁ τr₁) (Either τl₂ τr₂) = Either (rtype_meet τl₁ τl₂) (rtype_meet τr₁ τr₂).
Lemma rtype_meet_Either_neq_l τ τl τr: τ ≠ ⊤ → (∀ τl₂ τr₂, τ ≠ Either τl₂ τr₂) → rtype_meet (Either τl τr) τ = ⊥.
Lemma rtype_meet_Either_neq_r τ τl τr: τ ≠ ⊤ → (∀ τl₂ τr₂, τ ≠ Either τl₂ τr₂) → rtype_meet τ (Either τl τr) = ⊥.
Lemma rtype_meet_Brand_eq x y : rtype_meet (Brand x) (Brand y) = Brand (brand_meet brand_relation_brands x y).
Lemma rtype_meet_Brand_neq_l τ y: τ ≠ ⊤ → (∀ x, τ ≠ Brand x) → rtype_meet (Brand y) τ = ⊥.
Lemma rtype_meet_Brand_neq_r τ y: τ ≠ ⊤ → (∀ x, τ ≠ Brand x) → rtype_meet τ (Brand y) = ⊥.
Lemma rtype_meet_Foreign_eq x y : rtype_meet (Foreign x) (Foreign y) = Foreign (meet x y).
Lemma rtype_meet_Foreign_neq_l τ y: τ ≠ ⊤ → (∀ x, τ ≠ Foreign x) → rtype_meet (Foreign y) τ = ⊥.
Lemma rtype_meet_Foreign_neq_r τ y: τ ≠ ⊤ → (∀ x, τ ≠ Foreign x) → rtype_meet τ (Foreign y) = ⊥.
End rtype_meet_re.