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

[Coq formalisation][HUGE] Also recurse on position for assoc.

Still rely on String_UIP.
parent 7efc8a89
......@@ -17,6 +17,9 @@ Proof.
reflexivity.
Defined.
Inductive Istrue : bool -> Prop :=
| Istrue_true : Istrue true.
Definition isProp A := forall x y : A, x = y.
Module String_dec.
......@@ -28,478 +31,283 @@ Module String_UIP := Eqdep_dec.DecidableEqDep (String_dec).
Section domains.
(* We will often need to test wether a label is in a domain
so we reimplement the decidable membership test on lists of strings. *)
Inductive Position (l : string) : forall (l2 : string) (d : list string), Type :=
| At_head l2 d : l = l2 -> Position l l2 d
| In_tail l2 d : Pos2 l d -> Position l l2 d
with Pos2 (l : string) : forall (d : list string), Type :=
| PCons {hd tl} : Position l hd tl -> Pos2 l (cons hd tl).
Fixpoint In_dom l d :=
Definition PCons2 {l hd tl} : Pos2 l (cons hd tl) -> Position l hd tl.
Proof.
intro H.
inversion H.
assumption.
Defined.
Definition head (d : list string) : string :=
match d with
| nil => False
| cons l2 d =>
if (string_dec l l2) then True else In_dom l d
| nil => ""%string
| cons l _ => l
end.
Fixpoint Not_in_dom l d :=
Definition tail := @List.tail string.
Definition PCons_destr l l2 d H : H = @PCons l l2 d (PCons2 H).
Proof.
refine (match H with PCons l2 d p => _ end).
reflexivity.
Defined.
(* Destruction principle which doesn't destroy d *)
Definition destruct_pos {l l2 d} H (P : Position l l2 d -> Type) :
(forall e, P (At_head l l2 d e)) ->
(forall (H : Pos2 l d),
P (In_tail l l2 d H)) ->
P H.
Proof.
intros IH1 IH2.
induction H.
- apply IH1.
- apply IH2.
Defined.
Fixpoint mem l d :=
match d with
| nil => True
| nil => false
| cons l2 d =>
if (string_dec l l2) then False else Not_in_dom l d
if (string_dec l l2) then true else mem l d
end.
Fixpoint in_dom_dec l d : {In_dom l d} + {Not_in_dom l d}.
Fixpoint mem_pos l d : Istrue (mem l d) -> Pos2 l d.
Proof.
destruct d as [ | l2 d ].
- right. simpl.
intuition.
simpl.
- intro H; inversion H.
- simpl.
case (string_dec l l2).
+ left; intuition.
+ intro; apply in_dom_dec; assumption.
case (string_dec l l2) as [ e | n ].
+ intro.
apply PCons.
apply At_head.
assumption.
+ simpl.
intro H.
apply PCons.
apply In_tail.
apply mem_pos.
assumption.
Defined.
Fixpoint Not_not_in_dom l d : Not_in_dom l d <-> ~ In_dom l d.
Lemma Pos_tail l l2 d : l <> l2 -> Position l l2 d -> Pos2 l d.
Proof.
destruct d as [ | l2 d ].
- simpl.
intuition.
- simpl.
case (string_dec l l2).
+ intuition.
+ intro.
apply Not_not_in_dom.
Qed.
intros n p.
destruct p.
- destruct (n e).
- assumption.
Defined.
Fixpoint in_dom_irrel l d : isProp (In_dom l d).
Fixpoint mem_pos_neg l d {struct d} : Istrue (negb (mem l d)) -> Pos2 l d -> False.
Proof.
destruct d as [ | l2 d ].
- intros H1 H2; destruct H1.
simpl.
- intros _ H; inversion H.
- simpl.
case (string_dec l l2).
+ intros e H1 H2.
destruct H1.
destruct H2.
reflexivity.
+ intros n H1 H2.
apply in_dom_irrel.
Qed.
case (string_dec l l2) as [ e | n ].
+ intro H; inversion H.
+ intro H.
intro p.
apply PCons2 in p.
apply (Pos_tail l l2 d n) in p.
apply (mem_pos_neg l d); assumption.
Defined.
(* Domains without duplicates have unique positions *)
Fixpoint duplicate_free d :=
match d with
| nil => true
| cons l d => negb (mem l d) && duplicate_free d
end.
Definition in_eq l d := isProp (Pos2 l d).
Fixpoint not_in_dom_irrel l d : isProp (Not_in_dom l d).
Fixpoint df_in_eq l d {struct d} : Istrue (duplicate_free d) -> in_eq l d.
Proof.
destruct d as [ | l2 d ].
- simpl. intros H1 H2.
destruct H1; destruct H2.
reflexivity.
destruct d as [ | l2 d].
- intros _ H1 H2.
inversion H1.
- simpl.
case (string_dec l l2).
+ intros e H1 H2.
contradiction.
+ intros n H1 H2.
apply not_in_dom_irrel.
Qed.
(* Membership as a predicate *)
Inductive Position (l : string) : forall l2 : string, forall d : list string, Type :=
| At_head d : Position l l d
| In_tail hd l2 d : Position l hd d -> l <> l2 -> Position l l2 (cons hd d).
case_eq (mem l2 d).
+ intros _ H; inversion H.
+ intro Hm.
assert (Istrue (negb (mem l2 d))) as Hm2 by (rewrite Hm; exact Istrue_true).
simpl.
intro df.
assert (in_eq l d) as IH by intuition.
clear df_in_eq.
intros H1 H2.
rewrite (PCons_destr _ _ _ H1).
rewrite (PCons_destr _ _ _ H2).
apply f_equal.
generalize (PCons2 H1).
generalize (PCons2 H2).
intros H'2 H'1.
destruct H'1; destruct H'2.
* apply f_equal.
apply String_UIP.UIP.
* destruct e.
destruct (mem_pos_neg _ _ Hm2 p).
* destruct e.
destruct (mem_pos_neg _ _ Hm2 p).
* apply f_equal.
apply IH.
Defined.
End domains.
(* Properties of *)
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.
simpl.
case (string_dec l l); intuition.
Defined.
Lemma in_cons_tl {l1} l2 {d} : l1 d -> l1 cons l2 d.
Proof.
simpl.
case (string_dec l1 l2); intuition.
Defined.
Lemma in_cons_diff {l1} l2 {d} : l1 <> l2 -> l1 cons l2 d -> l1 d.
Proof.
intro diff.
simpl.
case (string_dec l1 l2); intuition.
Defined.
Lemma pos_in_dom {l} {l2} {d} : Position l l2 d -> l cons l2 d.
Proof.
intro H.
induction H as [ d | l2 d ].
+ apply in_cons_hd.
+ apply in_cons_tl; assumption.
Defined.
Lemma in_dom_pos {l} l2 {d} : l cons l2 d -> Position l l2 d.
Proof.
generalize l2; clear l2.
induction d as [ | hd d ]; intro l2; simpl; case (string_dec l l2).
* intros e _; destruct e; apply At_head.
* contradiction.
* intros e _; destruct e; apply At_head.
* intros.
apply In_tail.
apply IHd.
assumption.
assumption.
Defined.
Fixpoint pos_pos {l} {l2} {d} (H : Position l l2 d) : H = in_dom_pos l2 (pos_in_dom H).
Proof.
destruct H.
- simpl.
unfold in_cons_hd.
destruct d;
simpl;
(case (string_dec l l);
[ intro e; assert (He : e = eq_refl) by apply String_UIP.UIP;
rewrite He; reflexivity
| intro n; destruct (n eq_refl) ]).
- simpl.
unfold in_cons_tl.
case (string_dec l l2).
+ intro e; destruct (n e).
+ intros n'.
apply f_equal2.
* intuition.
* apply fun_ext.
intro e.
destruct (n e).
Qed.
Lemma pos_irrel {l l2 d} : isProp (Position l l2 d).
Proof.
intros H1 H2.
rewrite (pos_pos H1).
rewrite (pos_pos H2).
apply f_equal.
apply in_dom_irrel.
Qed.
Infix "∈" := (Pos2) (at level 60).
Definition subset d1 d2 : Type := forall l, (l d1) -> (l d2).
Infix "⊂" := subset (at level 60).
Section pretypes.
Section types.
(* Object types are records of types, we define them as association lists *)
Inductive pretype :=
| Empty_pretype
| Cons_pretype : string -> pretype -> pretype -> pretype.
Inductive type :=
| Empty_type
| Cons_type : string -> type -> type -> type.
End pretypes.
End types.
Section preassoc.
Section assoc.
Fixpoint predomain A :=
Fixpoint domain A :=
match A with
| Empty_pretype => nil
| Cons_pretype l _ C => cons l (predomain C)
| Empty_type => nil
| Cons_type l _ C => cons l (domain 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.
Fixpoint assoc A l (H : l domain A) : type.
Proof.
simpl.
case (string_dec l l); intuition.
Qed.
destruct A as [ | lA A1 A2].
- simpl in H.
inversion H.
- simpl in H.
apply PCons2 in H.
apply (destruct_pos H (fun H => type)).
+ intro; exact A1.
+ exact (assoc A2 l).
Defined.
End preassoc.
End assoc.
(* Scope of object types *)
Bind Scope obj_type_scope with pretype.
Bind Scope obj_type_scope with type.
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).
Notation "A ⊙ l" := (assoc A%ty l%string) (at level 50).
Fixpoint pretype_dec (A B : pretype) : {A = B} + {A <> B}.
Fixpoint type_dec (A B : type) : {A = B} + {A <> B}.
Proof.
decide equality.
apply string_dec.
Qed.
(* Definition of the subtyping relation: A <: B if B is a subset of A. *)
Fixpoint Subtype A B {struct B} :=
Fixpoint Subtype A B {struct B} : Type :=
match B with
| Empty_pretype => True
| Cons_pretype l B1 B2 =>
if in_dom_dec l (predomain A) then
if pretype_dec B1 (preassoc A l) then
Subtype A B2
else False
else False
| Empty_type => True
| Cons_type l B1 B2 =>
sigT (fun H => ((assoc A l H = B1) * Subtype A B2)%type)
end.
Infix "<:" := Subtype (at level 60).
Fixpoint subtype_dec A B : {A <: B} + {~ A <: B}.
Proof.
destruct B as [ | l B1 B2 ].
- left. simpl. intuition.
- simpl.
case (in_dom_dec l (predomain A));
case (pretype_dec B1 (preassoc A l));
intros;
(exact (subtype_dec A B2))|| (right; intuition).
Qed.
Lemma subtype_empty {A} : Empty_pretype <: A -> A = Empty_pretype.
Lemma subtype_tail {A} {B} l C :
A <: B ->
Cons_type l C A <: B.
Proof.
destruct A.
- trivial.
- simpl.
case (in_dom_dec s nil); contradiction.
Qed.
induction B as [ | lB B1 B2].
- intuition.
- intros (H, (He, st)).
exists (PCons _ (In_tail lB l (domain A) H)).
split.
+ simpl.
assumption.
+ intuition.
Defined.
Lemma subtype_cons_weaken {A} {B} {l} C :
A <: B ->
l predomain A ->
Cons_pretype l C A <: B.
Lemma subtype_refl A : A <: A.
Proof.
induction B.
induction A as [ | l A HA B HB ].
- intuition.
- simpl.
pose Not_not_in_dom.
pose @in_cons_tl.
case (in_dom_dec s (predomain A));
case (in_dom_dec s (l :: predomain A));
(case_eq (string_dec s l); [ intro sl; destruct sl | intros n H ]);
case (pretype_dec B1 C);
case (pretype_dec B1 (preassoc A s));
try rewrite pos_in_dom in *;
rewrite Not_not_in_dom in *;
intuition.
Qed.
Section subtype_reflexivity.
(* Unfortunately, the theorem forall A, A <: A is false
when A has several occurences of the same label *)
(* Hence we can only prove it for well-formed types: types without duplicates. *)
Fixpoint well_formed_type A :=
match A with
| Empty_pretype => True
| Cons_pretype l A1 A2 =>
l predomain A2 /\ well_formed_type A1 /\ well_formed_type A2
end.
Definition type := sigT well_formed_type.
Definition carrier (A : type) : pretype := let (A', _) := A in A'.
Definition carrier_wf (B : type) :=
let (A, wf) return (well_formed_type (carrier B)) := B in wf.
Definition type_norm A : A = existT well_formed_type (carrier A) (carrier_wf A).
Proof.
destruct A.
exists (PCons _ (At_head l l (domain B) eq_refl)).
simpl.
reflexivity.
Defined.
Fixpoint well_formed_dec A : {well_formed_type A} + {~ well_formed_type A}.
Proof.
destruct A as [ | l A1 A2 ].
- left.
exact I.
- simpl.
destruct (well_formed_dec A2); destruct (well_formed_dec A1).
+ case (in_dom_dec l (predomain A2)); [ right | left ]; intuition.
rewrite Not_not_in_dom in H0.
intuition.
+ right; intuition.
+ right; intuition.
+ right; intuition.
Qed.
Fixpoint well_formed_irrel {A} : isProp (well_formed_type A).
Proof.
intros H1 H2.
destruct A as [ | l A1 A2 ].
- destruct H1.
destruct H2.
reflexivity.
- simpl in *.
destruct H1 as (H1l, (H1A1, H1A2)).
destruct H2 as (H2l, (H2A1, H2A2)).
rewrite (well_formed_irrel A1 H1A1 H2A1).
rewrite (well_formed_irrel A2 H1A2 H2A2).
rewrite (not_in_dom_irrel l (predomain A2) H1l H2l).
reflexivity.
Defined.
Definition type_carrier A B : carrier A = carrier B -> A = B.
Proof.
intro H.
rewrite (type_norm A).
rewrite (type_norm B).
apply (sigT_eq H).
apply well_formed_irrel.
Defined.
Definition wf_decide A : bool :=
if well_formed_dec A then true else false.
Lemma wf_decide_spec {A} : well_formed_type A <-> wf_decide A = true.
Proof.
unfold wf_decide.
case (well_formed_dec); intuition; discriminate.
Qed.
Lemma wf_decide_true {A} : wf_decide A = true -> well_formed_type A.
Proof.
rewrite wf_decide_spec.
trivial.
Qed.
Theorem subtype_refl_eq {B} : forall {A}, A = B -> well_formed_type A -> A <: B.
Proof.
induction B as [ | l B1 IH1 B2 IH2 ].
- reflexivity.
- intros A H wf.
simpl.
case (in_dom_dec l (predomain A)); case (pretype_dec B1 (A l));
rewrite H; try (simpl; case (string_dec l l); intuition).
rewrite H in wf.
simpl in wf.
refine (subtype_cons_weaken _ _ _);
[ refine (IH2 B2 eq_refl _) | ];
intuition.
Defined.
Definition subtype_refl {A} : well_formed_type A -> A <: A
:= subtype_refl_eq eq_refl.
Definition subtype_refl_wf A : carrier A <: carrier A.
Proof.
destruct A as (A', wf).
simpl.
apply subtype_refl.
assumption.
Defined.
Theorem well_formed_preassoc {A} l :
well_formed_type A -> well_formed_type (preassoc A l).
Proof.
induction A.
- trivial.
- simpl.
case (string_dec l s).
+ intuition.
+ intros.
apply IHA2.
intuition.
Defined.
Definition assoc (A : type) (l : string) : type.
Proof.
destruct A as (A', wf).
exists (A' l).
apply well_formed_preassoc.
exact wf.
Defined.
Definition domain (A : type) : list string := predomain (carrier A).
End subtype_reflexivity.
(* Properties of subtyping with respect to predomain and preassoc. *)
Lemma predomain_subtype {A} {B} l : A <: B -> l predomain B -> l predomain A.
Proof.
induction B ; simpl.
- contradiction.
- case (string_dec l s) ; intro; case (in_dom_dec s (predomain A));
case (pretype_dec B1 (preassoc A s));
try intuition.
destruct e.
intuition.
Qed.
split.
+ reflexivity.
+ apply subtype_tail.
assumption.
Defined.
Lemma preassoc_subtype {A} {B} {l} :
A <: B -> l predomain B -> preassoc A l = preassoc B l.
Fixpoint domain_subtype {A} {B} :
A <: B -> domain B domain A.
Proof.
induction B.
- intros _ H0.
simpl in H0.
destruct H0.
- simpl.
case (string_dec l s) ; intro e;
case (in_dom_dec s (predomain A));
case (pretype_dec B1 (preassoc A s)); try intuition.
destruct e.
intuition.
intros st l H.
destruct B as [ | lB B1 B2 ].
- inversion H.
- destruct st as (Ha, (He, Hst)).
apply PCons2 in H.
inversion H as [ l' d Hl Hd | l2 d Hp Hl Hd ].
+ rewrite Hl.
assumption.
+ apply (domain_subtype A B2 Hst l).
assumption.