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

[coq_obj] reformulate definition of Expr closer to the paper

parent 2b14b9db
......@@ -40,19 +40,6 @@ Require Eqdep_dec.
Require EqdepFacts.
Import EqNotations.
Axiom fun_ext : forall A B (f g : A -> B),
(forall x, f x = g x) -> f = g.
Lemma sigT_eq {U} {P} {A B : U} {HA : P A} {HB : P B} :
forall e : A = B, (rew e in HA) = HB ->
existT P A HA = existT P B HB.
Proof.
intros e He.
destruct e.
destruct He.
reflexivity.
Defined.
Inductive Istrue : bool -> Prop :=
| Istrue_true : Istrue true.
......@@ -412,7 +399,7 @@ Section subtyping.
+ rewrite <- (assoc_subtype stAB lC HdBC).
assumption.
+ intuition.
Qed.
Defined.
End subtyping.
Infix "<:" := Subtype (at level 60).
......@@ -462,39 +449,40 @@ Section objects.
(* An expression of type B is an object of type A <: B coerced to type B. *)
Inductive Expr (B : type) :=
| Eobj : Obj B -> Expr B
| Ecoerce A : Expr A -> (A <: B) -> Expr B.
| Eobj A : Obj A -> (A <: B) -> Expr B.
(* type, object and prooj of subtyping underlying an ecpression *)
Fixpoint expr_type {A : type} (e : Expr A) : type.
Definition expr_type {A : type} (e : Expr A) : type.
Proof.
destruct e as [ o | A' e ].
- exact A.
- exact (expr_type A' e).
destruct e as (A', o, H).
- exact A'.
Defined.
Fixpoint expr_obj {A : type} (e : Expr A) : Obj (expr_type e).
Definition expr_obj {A : type} (e : Expr A) : Obj (expr_type e).
Proof.
destruct e as [ o | A' e ].
- exact o.
- exact (expr_obj A' e).
destruct e.
unfold expr_type.
assumption.
Defined.
Fixpoint expr_st {A : type} (e : Expr A) : (expr_type e) <: A.
Definition expr_st {A : type} (e : Expr A) : (expr_type e) <: A.
Proof.
destruct e as [ o | A' e ].
- apply subtype_refl.
- apply (subtype_trans A' (expr_st A' e) s).
destruct e.
unfold expr_type.
assumption.
Defined.
Definition Obj_to_expr {A} : Obj A -> Expr A := Eobj A.
Definition Obj_to_expr {A} (a : Obj A) : Expr A := Eobj A A a (subtype_refl A).
Definition Expr_coerce {A} B (a : Expr A) (H : A <: B): Expr B
:=
match a with
| Eobj A' o HA => Eobj B A' o (subtype_trans _ HA H)
end.
(* End of the axiomatisation of methods: Method A B is equivalent to Obj A -> Obj B. *)
Parameter Eval_meth : forall {A} {B}, Method A B -> Expr A -> Expr B.
Parameter Make_meth : forall {A} {B}, (Expr A -> Expr B) -> Method A B.
Axiom beta : forall {A B} (f : Expr A -> Expr B) a, Eval_meth (Make_meth f) a = f a.
(* Destruction principle for non-empty lists *)
Definition iscons (d : list string) := match d with nil => False | cons _ _ => True end.
......@@ -582,7 +570,7 @@ Notation "o ↑ A" := (@Obj_to_expr A%ty o) (at level 100).
Section semantics.
(* Selection and update go inside objects so they have to be defined on preobjects first. *)
Definition empty_expression : Expr Empty_type := Eobj Empty_type (poempty).
Definition empty_expression : Expr Empty_type := @Obj_to_expr Empty_type (poempty).
Fixpoint preselect l {A d} (po : Preobj A d)
(H : l d) {struct H} : Method A (assoc A l (po_sub po l H)).
......@@ -615,7 +603,7 @@ Section semantics.
Definition obj_select l {A} (a : Obj A) (H : l domain A) : Expr (assoc A l H).
Proof.
rewrite <- (obj_po_sub l a H).
exact (Eval_meth (preselect l a H) (Eobj A a)).
exact (Eval_meth (preselect l a H) (Obj_to_expr a)).
Defined.
Definition obj_update l {A} (a : Obj A) (H : l domain A) (m : Method A (assoc A l H)) : Obj A.
......@@ -636,12 +624,11 @@ Section semantics.
Definition update l {A} (a : Expr A) (H : l domain A) : Method A (assoc A l H) -> Expr A.
Proof.
intro m.
refine (Ecoerce A (expr_type a) _ (expr_st a)).
apply Eobj.
refine (Eobj A (expr_type a) _ (expr_st a)).
apply (obj_update l (expr_obj a) (domain_subtype (expr_st a) l H)).
apply Make_meth.
intro self.
apply (fun s => Ecoerce A (expr_type a) s (expr_st a)) in self.
apply (fun s => Expr_coerce A s (expr_st a)) in self.
rewrite <- (assoc_subtype (expr_st a) l H).
exact (Eval_meth m self).
Defined.
......
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