Qcert.Basic.TypeSystem.RType
open records allow width subtyping: they can have additional fields not in the type description
| Open
closed records do not allow width subtyping. They must have exactly the specified fields.
Syntax of types. Note that there is no guarantee yet that records are well formed. i.e., having distinct fields.
Context {ftype:foreign_type}.
Inductive rtype₀ : Set :=
| Bottom₀ : rtype₀
| Top₀ : rtype₀
| Unit₀ : rtype₀
| Nat₀ : rtype₀
| Bool₀ : rtype₀
| String₀ : rtype₀
| Coll₀ (r:rtype₀) : rtype₀
| Rec₀ (k:record_kind) (srl:list (string× rtype₀)) : rtype₀
| Either₀ (tl tr:rtype₀) : rtype₀
| Arrow₀ (tin tout : rtype₀) : rtype₀
| Brand₀ : brands → rtype₀
| Foreign₀ (ft:foreign_type_type) : rtype₀.
Notation "⊥₀" := Bottom₀.
Notation "⊤₀" := Top₀.
Definition rtype₀_rect (P : rtype₀ → Type)
(ftop : P ⊤₀)
(fbottom : P ⊥₀)
(funit : P Unit₀)
(fnat : P Nat₀)
(fbool : P Bool₀)
(fstring : P String₀)
(fcol : ∀ t : rtype₀, P t → P (Coll₀ t))
(frec : ∀ (k:record_kind) (r : list (string × rtype₀)), Forallt (fun ab ⇒ P (snd ab)) r → P (Rec₀ k r))
(feither : ∀ l r, P l → P r → P (Either₀ l r))
(farrow : ∀ tin tout, P tin → P tout → P (Arrow₀ tin tout))
(fbrand : ∀ b, P (Brand₀ b))
(fforeign : ∀ ft, P (Foreign₀ ft))
:=
fix F (t : rtype₀) : P t :=
match t as t0 return (P t0) with
| ⊤₀ ⇒ ftop
| ⊥₀ ⇒ fbottom
| Unit₀ ⇒ funit
| Nat₀ ⇒ fnat
| Bool₀ ⇒ fbool
| String₀ ⇒ fstring
| Coll₀ x ⇒ fcol x (F x)
| Rec₀ k x ⇒ frec k x ((fix Frec (r : list (string × rtype₀)) : Forallt (fun ab ⇒ P (snd ab)) r :=
match r as c0 with
| nil ⇒ Forallt_nil _
| cons sd c0 ⇒ @Forallt_cons _ (fun ab ⇒ P (snd ab)) sd c0 (F (snd sd)) (Frec c0)
end) x)
| Either₀ l r ⇒ feither l r (F l) (F r)
| Arrow₀ tin tout ⇒ farrow tin tout (F tin) (F tout)
| Brand₀ b ⇒ fbrand b
| Foreign₀ ft ⇒ fforeign ft
end.
Definition rtype₀_ind (P : rtype₀ → Prop)
(ftop : P ⊤₀)
(fbottom : P ⊥₀)
(funit : P Unit₀)
(fnat : P Nat₀)
(fbool : P Bool₀)
(fstring : P String₀)
(fcol : ∀ t : rtype₀, P t → P (Coll₀ t))
(frec : ∀ (k:record_kind) (r : list (string × rtype₀)), Forall (fun ab ⇒ P (snd ab)) r → P (Rec₀ k r))
(feither : ∀ l r, P l → P r → P (Either₀ l r))
(farrow : ∀ tin tout, P tin → P tout → P (Arrow₀ tin tout))
(fbrand : ∀ b, P (Brand₀ b))
(fforeign : ∀ ft, P (Foreign₀ ft))
:=
fix F (t : rtype₀) : P t :=
match t as t0 return (P t0) with
| ⊤₀ ⇒ ftop
| ⊥₀ ⇒ fbottom
| Unit₀ ⇒ funit
| Nat₀ ⇒ fnat
| Bool₀ ⇒ fbool
| String₀ ⇒ fstring
| Coll₀ x ⇒ fcol x (F x)
| Rec₀ k x ⇒ frec k x ((fix Frec (r : list (string × rtype₀)) : Forall (fun ab ⇒ P (snd ab)) r :=
match r as c0 with
| nil ⇒ Forall_nil _
| cons sd c0 ⇒ @Forall_cons _ (fun ab ⇒ P (snd ab)) sd c0 (F (snd sd)) (Frec c0)
end) x)
| Either₀ l r ⇒ feither l r (F l) (F r)
| Arrow₀ tin tout ⇒ farrow tin tout (F tin) (F tout)
| Brand₀ b ⇒ fbrand b
| Foreign₀ ft ⇒ fforeign ft
end.
Definition rtype₀_rec (P:rtype₀→Set) := rtype₀_rect P.
Global Instance rtype₀_eqdec : EqDec rtype₀ eq.
End rtypes₀.
Notation "⊥₀" := Bottom₀.
Notation "⊤₀" := Top₀.
Section well_formed_rtypes.
Context {ftype:foreign_type}.
Context {br:brand_relation}.
Fixpoint wf_rtype₀ (τ:rtype₀): bool
:= match τ with
| Coll₀ τ' ⇒ wf_rtype₀ τ'
| Rec₀ oc srl ⇒ is_list_sorted ODT_lt_dec (domain srl)
&& forallb (fun ab ⇒ wf_rtype₀ (snd ab)) srl
| Either₀ τl τr ⇒ wf_rtype₀ τl && wf_rtype₀ τr
| Arrow₀ τin τout ⇒ wf_rtype₀ τin && wf_rtype₀ τout
| Brand₀ b ⇒ if is_canon_brands_dec brand_relation_brands b then true else false
| _ ⇒ true
end.
Definition rtype : Set := {τ₀:rtype₀ | wf_rtype₀ τ₀ = true}.
Lemma wf_rtype₀_ext {τ₀:rtype₀} (pf1 pf2:wf_rtype₀ τ₀ = true) : pf1 = pf2.
Lemma rtype_ext {τ₀} (wfτ1 wfτ2:wf_rtype₀ τ₀ = true) :
(exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ₀ = true) τ₀ wfτ1) =
(exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ₀ = true) τ₀ wfτ2).
Lemma rtype_fequal {τ₁ τ₂:rtype} : proj1_sig τ₁ = proj1_sig τ₂ → τ₁ = τ₂.
Lemma rtype_nequal {τ₁ τ₂:rtype} : τ₁ ≠ τ₂ → proj1_sig τ₁ ≠ proj1_sig τ₂.
Lemma map_rtype_fequal r1 r2 :
map
(fun x : string × {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} ⇒
(fst x, proj1_sig (snd x))) r1 =
map
(fun x : string × {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} ⇒
(fst x, proj1_sig (snd x))) r2 →
r1 = r2.
Lemma map_rtype_single_rec_fequal a τ r :
(a, proj1_sig τ)::nil =
map
(fun x : string × {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} ⇒
(fst x, proj1_sig (snd x))) r →
((a, τ)::nil) = r.
Global Instance rtype_eq_dec : EqDec rtype eq.
Lifted versions of the type constructors This is the main type system, and always carries a proofs that the records are well formed
Program Definition Bottom : rtype := Bottom₀.
Program Definition Top : rtype := Top₀.
Program Definition Unit : rtype := Unit₀.
Program Definition Nat : rtype := Nat₀.
Program Definition Bool : rtype := Bool₀.
Program Definition String : rtype := String₀.
Definition Coll (τ:rtype): rtype :=
exist _ (Coll₀ (proj1_sig τ)) (proj2_sig τ).
Program Definition Either (τl τr:rtype) : rtype :=
exist _ (Either₀ (proj1_sig τl) (proj1_sig τr)) _.
Program Definition Arrow (τl τr:rtype) : rtype :=
exist _ (Arrow₀ (proj1_sig τl) (proj1_sig τr)) _.
Program Definition Foreign (ft:foreign_type_type) : rtype
:= Foreign₀ ft.
Program Definition Rec
(k:record_kind)
(srl:list (string× rtype))
(pf_sorted:is_list_sorted ODT_lt_dec (domain srl) = true) : rtype
:= Rec₀ k (map (fun x ⇒ (fst x, proj1_sig (snd x))) srl).
Program Definition Brand b : rtype := Brand₀ (canon_brands brand_relation_brands b).
Global Instance Brand_equiv_proper :
Proper (equiv_brands brand_relation_brands ==> eq) (Brand).
Notation "⊥" := Bottom.
Notation "⊤" := Top.
Definition Option τ := Either τ Unit.
Theorem rtype_rect (P : rtype → Type)
(ftop : P ⊤)
(fbottom : P ⊥)
(funit : P Unit)
(fnat : P Nat)
(fbool : P Bool)
(fstring : P String)
(fcol : ∀ t : rtype, P t → P (Coll t))
(frec : ∀ (k:record_kind) (srl : list (string × rtype))
(pf:is_list_sorted ODT_lt_dec (domain srl) = true),
Forallt (fun ab ⇒ P (snd ab)) srl → P (Rec k srl pf))
(feither : ∀ (τl τr:rtype), P τl → P τr → P (Either τl τr))
(farrow : ∀ (τin τout:rtype), P τin → P τout → P (Arrow τin τout))
(fbrand : ∀ b, P (Brand b))
(fforeign : ∀ ft, P (Foreign ft))
:
∀ (τ:rtype), P τ.
Theorem rtype_ind (P : rtype → Prop)
(ftop : P ⊤)
(fbottom : P ⊥)
(funit : P Unit)
(fnat : P Nat)
(fbool : P Bool)
(fstring : P String)
(fcol : ∀ t : rtype, P t → P (Coll t))
(frec : ∀ (k:record_kind) (srl : list (string × rtype))
(pf:is_list_sorted ODT_lt_dec (domain srl) = true),
Forall (fun ab ⇒ P (snd ab)) srl → P (Rec k srl pf))
(feither : ∀ (τl τr:rtype), P τl → P τr → P (Either τl τr))
(farrow : ∀ (τin τout:rtype), P τin → P τout → P (Arrow τin τout))
(fbrand : ∀ b, P (Brand b))
(fforeign : ∀ ft, P (Foreign ft)) :
∀ (τ:rtype), P τ.
Definition rtype_rec (P:rtype→Set) := rtype_rect P.
Lemma wf_rtype₀_kind_irrel k₁ k₂ l :
wf_rtype₀ (Rec₀ k₁ l) = wf_rtype₀ (Rec₀ k₂ l).
Lemma wf_rtype₀_Brand₀ b :
wf_rtype₀ (Brand₀ b) = true →
is_canon_brands brand_relation_brands b.
Lemma brand_ext b pf : exist _ (Brand₀ b) pf = Brand b.
Lemma wf_rtype₀_cons_tail {k} {a r} :
wf_rtype₀ (Rec₀ k (a::r)) = true →
wf_rtype₀ (Rec₀ k r) = true.
Lemma wf_rtype₀_cons_lt {k s r srl s' r'} :
wf_rtype₀ (Rec₀ k ((s, r) :: srl)) = true →
lookup string_dec srl s' = Some r' →
ODT_lt s s'.
Lemma wf_rtype₀_cons_nin {k s r srl} :
wf_rtype₀ (Rec₀ k ((s, r) :: srl)) = true → lookup string_dec srl s = None.
Lemma wf_rtype₀_cons_wf {k s r srl} :
wf_rtype₀ (Rec₀ k ((s, r) :: srl)) = true →
wf_rtype₀ r = true.
End well_formed_rtypes.
Notation "⊥" := Bottom.
Notation "⊤" := Top.
Lemma to_Rec {ftype:foreign_type} {br:brand_relation} k l pf :
∃ pf2,
exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ₀ = true)
(Rec₀
k (map
(fun x : string × {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} ⇒
(fst x, proj1_sig (snd x))) l)) pf
= Rec k l pf2.
Lemma from_Rec₀ {ftype:foreign_type} {br:brand_relation} {k} (l:list (string × rtype₀)) (pf : wf_rtype₀ (Rec₀ k l) = true) :
{l' | ∃ pf',
l =
(map
(fun x : string × {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} ⇒
(fst x, proj1_sig (snd x))) l')
∧ Rec k l' pf' = exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ₀ = true) (Rec₀ k l) pf}.
Lemma lookup_map_some {ftype:foreign_type} {br:brand_relation} rl2 s x :
lookup string_dec rl2 s = Some x ↔
lookup string_dec
(map
(fun x : string × {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} ⇒
(fst x, proj1_sig (snd x))) rl2) s = Some (proj1_sig x).
Lemma lookup_map_some' {ftype:foreign_type} {br:brand_relation} rl2 s x pf :
lookup string_dec rl2 s = Some (exist _ x pf) ↔
lookup string_dec
(map
(fun x : string × {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} ⇒
(fst x, proj1_sig (snd x))) rl2) s = Some x.
Lemma lookup_map_some_ex {ftype:foreign_type} {br:brand_relation}
(rl2 : list (string × {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true}))
(s : string) (x : rtype₀) :
(∃ pf, lookup string_dec rl2 s =
Some (exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ₀ = true) x pf)) ↔
lookup string_dec
(map
(fun x0 : string × {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} ⇒
(fst x0, proj1_sig (snd x0))) rl2) s = Some x.
Lemma lookup_map_none {ftype:foreign_type} {br:brand_relation} rl2 s :
lookup string_dec rl2 s = None ↔
lookup string_dec
(map
(fun x : string × {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} ⇒
(fst x, proj1_sig (snd x))) rl2) s = None.
End RType.
Section recmaybe.
Context {ftype:foreign_type}.
Context {br:brand_relation}.
Definition RecMaybe (k:record_kind) (lsr:list (string×rtype)) : option rtype.
Defined.
Lemma RecMaybe_some_pf_helper (z:bool) τ f :
(if z as b
return
(z = b → option rtype)
then
fun pf : z = true ⇒
Some (f pf)
else
fun _ : z = false ⇒ None)
eq_refl = Some τ →
{pf : z = true |
τ = f pf}.
Lemma RecMaybe_some_pf {k τ₀ τ} :
RecMaybe k τ₀ = Some τ →
{pf | τ = Rec k τ₀ pf}.
Lemma RecMaybe_pf_some_helper (z:bool) f pf :
z = true →
(if z as b
return
(z = b → option rtype)
then
fun pf : z = true ⇒
f pf
else
fun _ : z = false ⇒ None)
eq_refl = f pf.
Lemma RecMaybe_pf_some k l pf :
RecMaybe k l = Some (Rec k l pf).
Lemma RecMaybe_nil k : RecMaybe k nil = Some (Rec k nil eq_refl).
End recmaybe.
Section other.
Context {ftype:foreign_type}.
Context {br:brand_relation}.
Lemma Rec_inv {k k' x pf1 y pf2} : Rec k x pf1 = Rec k' y pf2 → x = y.
Lemma Rec_kind_inv {k k' x pf1 y pf2} : Rec k x pf1 = Rec k' y pf2 → k = k'.
Lemma Rec_pr_irrel k l1 pf1 pf2 :
Rec k l1 pf1 = Rec k l1 pf2.
Lemma Rec_rewrite {l1 l2} k pf1 pf2 :
l1 = l2 →
Rec k l1 pf1 = Rec k l2 pf2.
Lemma Rec_kind_rewrite k1 k2 l pf :
k1 = k2 →
Rec k1 l pf = Rec k2 l pf.
Lemma Coll_right_inv (τ₁ τ₂:rtype) :
(proj1_sig τ₁) = Coll₀ (proj1_sig τ₂) ↔ τ₁ = Coll τ₂.
Lemma Coll_inside (τ₁:rtype) (τ₂₀:rtype₀) :
(proj1_sig τ₁) = Coll₀ τ₂₀ →
∃ τ₂:rtype, proj1_sig τ₂ = τ₂₀.
Lemma map_rtype_nil x0:
map (fun x2 : string × {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} ⇒
(fst x2, proj1_sig (snd x2))) x0 = nil ↔ x0 = nil.
Lemma Rec₀_eq_proj1_Rec {τ k l} :
proj1_sig τ =
Rec₀
k (map
(fun x : string × {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} ⇒
(fst x, proj1_sig (snd x))) l) →
∃ pf, τ = Rec k l pf.
Lemma Nat_canon pf:
(exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ₀ = true) Nat₀ pf) = Nat.
Lemma String_canon pf:
(exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ₀ = true) String₀ pf) = String.
Lemma Coll_canon x pf:
(exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ₀ = true) (Coll₀ x) pf) = Coll (exist _ x pf).
Lemma Brand_canon x pf:
(exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ₀ = true) (Brand₀ x) pf) = Brand x.
Lemma Foreign_canon ft pf:
(exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ₀ = true) (Foreign₀ ft) pf) = Foreign ft.
Lemma Either₀_wf_inv {l r} :
wf_rtype₀ (Either₀ l r) = true →
wf_rtype₀ l = true ∧ wf_rtype₀ r = true.
Lemma Either_canon l r pf pfl pfr:
(exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ₀ = true) (Either₀ l r) pf) = Either (exist _ l pfl) (exist _ r pfr).
Lemma Either_canon_ex l r pf:
∃ pfl pfr,
(exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ₀ = true) (Either₀ l r) pf) = Either (exist _ l pfl) (exist _ r pfr).
Lemma Arrow₀_wf_inv {l r} :
wf_rtype₀ (Arrow₀ l r) = true →
wf_rtype₀ l = true ∧ wf_rtype₀ r = true.
Lemma Arrow_canon l r pf pfl pfr:
(exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ₀ = true) (Arrow₀ l r) pf) = Arrow (exist _ l pfl) (exist _ r pfr).
Lemma Arrow_canon_ex l r pf:
∃ pfl pfr,
(exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ₀ = true) (Arrow₀ l r) pf) = Arrow (exist _ l pfl) (exist _ r pfr).
Lemma wf_rtype₀_Rec_In {k srl} :
wf_rtype₀ (Rec₀ k srl) = true →
∀ a b, In (a,b) srl → wf_rtype₀ b = true.
Lemma wf_rec_pf_sublist {B} {l l'} :
is_list_sorted ODT_lt_dec (@domain _ B l) = true →
sublist l' l →
is_list_sorted ODT_lt_dec (domain l') = true.
Lemma lift_Rec₀_injective {k₁ k₂ l1 l2} : lift (Rec₀ k₁) l1 = lift (Rec₀ k₂) l2 → l1 = l2.
Lemma some_lift_Rec₀ {k₁ k₂ x y} :
lift (Rec₀ k₁) x = Some (Rec₀ k₂ y) →
x = Some y.
Lemma lift_Coll₀_injective {l1 l2} : lift Coll₀ l1 = lift Coll₀ l2 → l1 = l2.
Lemma some_lift_Coll₀ {x y} :
lift Coll₀ x = Some (Coll₀ y) →
x = Some y.
Lemma lift_Coll_injective {l1 l2} : lift Coll l1 = lift Coll l2 → l1 = l2.
Lemma some_lift_Coll {x y} :
lift Coll x = Some (Coll y) →
x = Some y.
Lemma lift_col₀_some_col₀ {x y} :
lift Coll₀ x = Some y →
{z | y = Coll₀ z}.
Lemma lift_col_some_col {x y} :
lift Coll x = Some y →
{z | y = Coll z}.
Lemma lift_rec₀_some_rec₀ {k x y} :
lift (Rec₀ k) x = Some y →
{z | y = Rec₀ k z}.
Definition isTop (τ:rtype) : bool.
Defined.
Lemma istop τ : {τ = Top} + {isTop τ = false}.
End other.
Notation "⊥₀" := Bottom₀.
Notation "⊤₀" := Top₀.
Notation "⊥" := Bottom.
Notation "⊤" := Top.
Program Definition Top : rtype := Top₀.
Program Definition Unit : rtype := Unit₀.
Program Definition Nat : rtype := Nat₀.
Program Definition Bool : rtype := Bool₀.
Program Definition String : rtype := String₀.
Definition Coll (τ:rtype): rtype :=
exist _ (Coll₀ (proj1_sig τ)) (proj2_sig τ).
Program Definition Either (τl τr:rtype) : rtype :=
exist _ (Either₀ (proj1_sig τl) (proj1_sig τr)) _.
Program Definition Arrow (τl τr:rtype) : rtype :=
exist _ (Arrow₀ (proj1_sig τl) (proj1_sig τr)) _.
Program Definition Foreign (ft:foreign_type_type) : rtype
:= Foreign₀ ft.
Program Definition Rec
(k:record_kind)
(srl:list (string× rtype))
(pf_sorted:is_list_sorted ODT_lt_dec (domain srl) = true) : rtype
:= Rec₀ k (map (fun x ⇒ (fst x, proj1_sig (snd x))) srl).
Program Definition Brand b : rtype := Brand₀ (canon_brands brand_relation_brands b).
Global Instance Brand_equiv_proper :
Proper (equiv_brands brand_relation_brands ==> eq) (Brand).
Notation "⊥" := Bottom.
Notation "⊤" := Top.
Definition Option τ := Either τ Unit.
Theorem rtype_rect (P : rtype → Type)
(ftop : P ⊤)
(fbottom : P ⊥)
(funit : P Unit)
(fnat : P Nat)
(fbool : P Bool)
(fstring : P String)
(fcol : ∀ t : rtype, P t → P (Coll t))
(frec : ∀ (k:record_kind) (srl : list (string × rtype))
(pf:is_list_sorted ODT_lt_dec (domain srl) = true),
Forallt (fun ab ⇒ P (snd ab)) srl → P (Rec k srl pf))
(feither : ∀ (τl τr:rtype), P τl → P τr → P (Either τl τr))
(farrow : ∀ (τin τout:rtype), P τin → P τout → P (Arrow τin τout))
(fbrand : ∀ b, P (Brand b))
(fforeign : ∀ ft, P (Foreign ft))
:
∀ (τ:rtype), P τ.
Theorem rtype_ind (P : rtype → Prop)
(ftop : P ⊤)
(fbottom : P ⊥)
(funit : P Unit)
(fnat : P Nat)
(fbool : P Bool)
(fstring : P String)
(fcol : ∀ t : rtype, P t → P (Coll t))
(frec : ∀ (k:record_kind) (srl : list (string × rtype))
(pf:is_list_sorted ODT_lt_dec (domain srl) = true),
Forall (fun ab ⇒ P (snd ab)) srl → P (Rec k srl pf))
(feither : ∀ (τl τr:rtype), P τl → P τr → P (Either τl τr))
(farrow : ∀ (τin τout:rtype), P τin → P τout → P (Arrow τin τout))
(fbrand : ∀ b, P (Brand b))
(fforeign : ∀ ft, P (Foreign ft)) :
∀ (τ:rtype), P τ.
Definition rtype_rec (P:rtype→Set) := rtype_rect P.
Lemma wf_rtype₀_kind_irrel k₁ k₂ l :
wf_rtype₀ (Rec₀ k₁ l) = wf_rtype₀ (Rec₀ k₂ l).
Lemma wf_rtype₀_Brand₀ b :
wf_rtype₀ (Brand₀ b) = true →
is_canon_brands brand_relation_brands b.
Lemma brand_ext b pf : exist _ (Brand₀ b) pf = Brand b.
Lemma wf_rtype₀_cons_tail {k} {a r} :
wf_rtype₀ (Rec₀ k (a::r)) = true →
wf_rtype₀ (Rec₀ k r) = true.
Lemma wf_rtype₀_cons_lt {k s r srl s' r'} :
wf_rtype₀ (Rec₀ k ((s, r) :: srl)) = true →
lookup string_dec srl s' = Some r' →
ODT_lt s s'.
Lemma wf_rtype₀_cons_nin {k s r srl} :
wf_rtype₀ (Rec₀ k ((s, r) :: srl)) = true → lookup string_dec srl s = None.
Lemma wf_rtype₀_cons_wf {k s r srl} :
wf_rtype₀ (Rec₀ k ((s, r) :: srl)) = true →
wf_rtype₀ r = true.
End well_formed_rtypes.
Notation "⊥" := Bottom.
Notation "⊤" := Top.
Lemma to_Rec {ftype:foreign_type} {br:brand_relation} k l pf :
∃ pf2,
exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ₀ = true)
(Rec₀
k (map
(fun x : string × {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} ⇒
(fst x, proj1_sig (snd x))) l)) pf
= Rec k l pf2.
Lemma from_Rec₀ {ftype:foreign_type} {br:brand_relation} {k} (l:list (string × rtype₀)) (pf : wf_rtype₀ (Rec₀ k l) = true) :
{l' | ∃ pf',
l =
(map
(fun x : string × {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} ⇒
(fst x, proj1_sig (snd x))) l')
∧ Rec k l' pf' = exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ₀ = true) (Rec₀ k l) pf}.
Lemma lookup_map_some {ftype:foreign_type} {br:brand_relation} rl2 s x :
lookup string_dec rl2 s = Some x ↔
lookup string_dec
(map
(fun x : string × {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} ⇒
(fst x, proj1_sig (snd x))) rl2) s = Some (proj1_sig x).
Lemma lookup_map_some' {ftype:foreign_type} {br:brand_relation} rl2 s x pf :
lookup string_dec rl2 s = Some (exist _ x pf) ↔
lookup string_dec
(map
(fun x : string × {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} ⇒
(fst x, proj1_sig (snd x))) rl2) s = Some x.
Lemma lookup_map_some_ex {ftype:foreign_type} {br:brand_relation}
(rl2 : list (string × {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true}))
(s : string) (x : rtype₀) :
(∃ pf, lookup string_dec rl2 s =
Some (exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ₀ = true) x pf)) ↔
lookup string_dec
(map
(fun x0 : string × {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} ⇒
(fst x0, proj1_sig (snd x0))) rl2) s = Some x.
Lemma lookup_map_none {ftype:foreign_type} {br:brand_relation} rl2 s :
lookup string_dec rl2 s = None ↔
lookup string_dec
(map
(fun x : string × {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} ⇒
(fst x, proj1_sig (snd x))) rl2) s = None.
End RType.
Section recmaybe.
Context {ftype:foreign_type}.
Context {br:brand_relation}.
Definition RecMaybe (k:record_kind) (lsr:list (string×rtype)) : option rtype.
Defined.
Lemma RecMaybe_some_pf_helper (z:bool) τ f :
(if z as b
return
(z = b → option rtype)
then
fun pf : z = true ⇒
Some (f pf)
else
fun _ : z = false ⇒ None)
eq_refl = Some τ →
{pf : z = true |
τ = f pf}.
Lemma RecMaybe_some_pf {k τ₀ τ} :
RecMaybe k τ₀ = Some τ →
{pf | τ = Rec k τ₀ pf}.
Lemma RecMaybe_pf_some_helper (z:bool) f pf :
z = true →
(if z as b
return
(z = b → option rtype)
then
fun pf : z = true ⇒
f pf
else
fun _ : z = false ⇒ None)
eq_refl = f pf.
Lemma RecMaybe_pf_some k l pf :
RecMaybe k l = Some (Rec k l pf).
Lemma RecMaybe_nil k : RecMaybe k nil = Some (Rec k nil eq_refl).
End recmaybe.
Section other.
Context {ftype:foreign_type}.
Context {br:brand_relation}.
Lemma Rec_inv {k k' x pf1 y pf2} : Rec k x pf1 = Rec k' y pf2 → x = y.
Lemma Rec_kind_inv {k k' x pf1 y pf2} : Rec k x pf1 = Rec k' y pf2 → k = k'.
Lemma Rec_pr_irrel k l1 pf1 pf2 :
Rec k l1 pf1 = Rec k l1 pf2.
Lemma Rec_rewrite {l1 l2} k pf1 pf2 :
l1 = l2 →
Rec k l1 pf1 = Rec k l2 pf2.
Lemma Rec_kind_rewrite k1 k2 l pf :
k1 = k2 →
Rec k1 l pf = Rec k2 l pf.
Lemma Coll_right_inv (τ₁ τ₂:rtype) :
(proj1_sig τ₁) = Coll₀ (proj1_sig τ₂) ↔ τ₁ = Coll τ₂.
Lemma Coll_inside (τ₁:rtype) (τ₂₀:rtype₀) :
(proj1_sig τ₁) = Coll₀ τ₂₀ →
∃ τ₂:rtype, proj1_sig τ₂ = τ₂₀.
Lemma map_rtype_nil x0:
map (fun x2 : string × {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} ⇒
(fst x2, proj1_sig (snd x2))) x0 = nil ↔ x0 = nil.
Lemma Rec₀_eq_proj1_Rec {τ k l} :
proj1_sig τ =
Rec₀
k (map
(fun x : string × {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} ⇒
(fst x, proj1_sig (snd x))) l) →
∃ pf, τ = Rec k l pf.
Lemma Nat_canon pf:
(exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ₀ = true) Nat₀ pf) = Nat.
Lemma String_canon pf:
(exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ₀ = true) String₀ pf) = String.
Lemma Coll_canon x pf:
(exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ₀ = true) (Coll₀ x) pf) = Coll (exist _ x pf).
Lemma Brand_canon x pf:
(exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ₀ = true) (Brand₀ x) pf) = Brand x.
Lemma Foreign_canon ft pf:
(exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ₀ = true) (Foreign₀ ft) pf) = Foreign ft.
Lemma Either₀_wf_inv {l r} :
wf_rtype₀ (Either₀ l r) = true →
wf_rtype₀ l = true ∧ wf_rtype₀ r = true.
Lemma Either_canon l r pf pfl pfr:
(exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ₀ = true) (Either₀ l r) pf) = Either (exist _ l pfl) (exist _ r pfr).
Lemma Either_canon_ex l r pf:
∃ pfl pfr,
(exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ₀ = true) (Either₀ l r) pf) = Either (exist _ l pfl) (exist _ r pfr).
Lemma Arrow₀_wf_inv {l r} :
wf_rtype₀ (Arrow₀ l r) = true →
wf_rtype₀ l = true ∧ wf_rtype₀ r = true.
Lemma Arrow_canon l r pf pfl pfr:
(exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ₀ = true) (Arrow₀ l r) pf) = Arrow (exist _ l pfl) (exist _ r pfr).
Lemma Arrow_canon_ex l r pf:
∃ pfl pfr,
(exist (fun τ₀ : rtype₀ ⇒ wf_rtype₀ τ₀ = true) (Arrow₀ l r) pf) = Arrow (exist _ l pfl) (exist _ r pfr).
Lemma wf_rtype₀_Rec_In {k srl} :
wf_rtype₀ (Rec₀ k srl) = true →
∀ a b, In (a,b) srl → wf_rtype₀ b = true.
Lemma wf_rec_pf_sublist {B} {l l'} :
is_list_sorted ODT_lt_dec (@domain _ B l) = true →
sublist l' l →
is_list_sorted ODT_lt_dec (domain l') = true.
Lemma lift_Rec₀_injective {k₁ k₂ l1 l2} : lift (Rec₀ k₁) l1 = lift (Rec₀ k₂) l2 → l1 = l2.
Lemma some_lift_Rec₀ {k₁ k₂ x y} :
lift (Rec₀ k₁) x = Some (Rec₀ k₂ y) →
x = Some y.
Lemma lift_Coll₀_injective {l1 l2} : lift Coll₀ l1 = lift Coll₀ l2 → l1 = l2.
Lemma some_lift_Coll₀ {x y} :
lift Coll₀ x = Some (Coll₀ y) →
x = Some y.
Lemma lift_Coll_injective {l1 l2} : lift Coll l1 = lift Coll l2 → l1 = l2.
Lemma some_lift_Coll {x y} :
lift Coll x = Some (Coll y) →
x = Some y.
Lemma lift_col₀_some_col₀ {x y} :
lift Coll₀ x = Some y →
{z | y = Coll₀ z}.
Lemma lift_col_some_col {x y} :
lift Coll x = Some y →
{z | y = Coll z}.
Lemma lift_rec₀_some_rec₀ {k x y} :
lift (Rec₀ k) x = Some y →
{z | y = Rec₀ k z}.
Definition isTop (τ:rtype) : bool.
Defined.
Lemma istop τ : {τ = Top} + {isTop τ = false}.
End other.
Notation "⊥₀" := Bottom₀.
Notation "⊤₀" := Top₀.
Notation "⊥" := Bottom.
Notation "⊤" := Top.
Cases tactic for use with the derived rtypeRectt induction principle
Tactic Notation "rtype_rect_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "Top"%string
| Case_aux c "Bottom"%string
| Case_aux c "Unit"%string
| Case_aux c "Nat"%string
| Case_aux c "Bool"%string
| Case_aux c "String"%string
| Case_aux c "Coll"%string
| Case_aux c "Rec"%string
| Case_aux c "Either"%string
| Case_aux c "Arrow"%string
| Case_aux c "Brand"%string
| Case_aux c "Foreign"%string
].
first;
[ Case_aux c "Top"%string
| Case_aux c "Bottom"%string
| Case_aux c "Unit"%string
| Case_aux c "Nat"%string
| Case_aux c "Bool"%string
| Case_aux c "String"%string
| Case_aux c "Coll"%string
| Case_aux c "Rec"%string
| Case_aux c "Either"%string
| Case_aux c "Arrow"%string
| Case_aux c "Brand"%string
| Case_aux c "Foreign"%string
].