Commit cc687fd9 authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

[Coq formalisation] put the properties about lists of strings before the

definition of types
parent 1cf4aa30
......@@ -26,49 +26,8 @@ End String_dec.
Module String_UIP := Eqdep_dec.DecidableEqDep (String_dec).
Section pretypes.
(* Object types are records of types, we define them as association lists *)
Inductive pretype :=
| Empty_pretype
| Cons_pretype : string -> pretype -> pretype -> pretype.
End pretypes.
Section preassoc.
Fixpoint preassoc A l :=
match A with
| Empty_pretype => Empty_pretype
| Cons_pretype l2 B C =>
match string_dec l l2 with
| left _ => B
| right _ => preassoc C l
end
end.
Lemma assoc_hd A1 A2 l : preassoc (Cons_pretype l A1 A2) l = A1.
Proof.
simpl.
case (string_dec l l); intuition.
Qed.
End preassoc.
(* Scope of object types *)
Bind Scope obj_type_scope with pretype.
Delimit Scope obj_type_scope with ty.
(* Scope of object type fields (pairs of strings and types) *)
Delimit Scope type_field_scope with tf.
Section domains.
Fixpoint predomain A :=
match A with
| Empty_pretype => nil
| Cons_pretype l _ C => cons l (predomain C)
end.
(* We will often need to test wether a label is in a domain
so we reimplement the decidable membership test on lists of strings. *)
......@@ -146,8 +105,8 @@ End domains.
(* Properties of *)
Notation "l ∈ d" := (In_dom l d%ty) (at level 60).
Notation "l ∉ d" := (Not_in_dom l d%ty) (at level 60).
Notation "l ∈ d" := (In_dom l d) (at level 60).
Notation "l ∉ d" := (Not_in_dom l d) (at level 60).
Definition in_cons_hd l d : l cons l d.
Proof.
......@@ -222,6 +181,49 @@ Proof.
apply in_dom_irrel.
Qed.
Section pretypes.
(* Object types are records of types, we define them as association lists *)
Inductive pretype :=
| Empty_pretype
| Cons_pretype : string -> pretype -> pretype -> pretype.
End pretypes.
Section preassoc.
Fixpoint predomain A :=
match A with
| Empty_pretype => nil
| Cons_pretype l _ C => cons l (predomain C)
end.
Fixpoint preassoc A l :=
match A with
| Empty_pretype => Empty_pretype
| Cons_pretype l2 B C =>
match string_dec l l2 with
| left _ => B
| right _ => preassoc C l
end
end.
Lemma assoc_hd A1 A2 l : preassoc (Cons_pretype l A1 A2) l = A1.
Proof.
simpl.
case (string_dec l l); intuition.
Qed.
End preassoc.
(* Scope of object types *)
Bind Scope obj_type_scope with pretype.
Delimit Scope obj_type_scope with ty.
(* Scope of object type fields (pairs of strings and types) *)
Delimit Scope type_field_scope with tf.
Section subtyping.
Notation "A ⊙ l" := (preassoc A%ty l%string) (at level 50).
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment