coq_obj.v

Require Import String.
Require Import Bool.
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.

Definition isProp A := forall x y : A, x = y.

Module String_dec.
  Definition U := string.
  Definition eq_dec := string_dec.
End String_dec.

Module String_UIP := Eqdep_dec.DecidableEqDep (String_dec).

Section domains.

  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).

  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 => ""%string
      | cons l _ => l
    end.

  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 => false
      | cons l2 d =>
        if (string_dec l l2) then true else mem l d
    end.

  Fixpoint mem_pos l d : Istrue (mem l d) -> Pos2 l d.
  Proof.
    destruct d as [ | l2 d ].
    simpl.
    - intro H; inversion H.
    - simpl.
      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.

  Lemma Pos_tail l l2 d : l <> l2 -> Position l l2 d -> Pos2 l d.
  Proof.
    intros n p.
    destruct p.
    - destruct (n e).
    - assumption.
  Defined.

  Fixpoint mem_pos_neg l d {struct d} : Istrue (negb (mem l d)) -> Pos2 l d -> False.
  Proof.
    destruct d as [ | l2 d ].
    simpl.
    - intros _ H; inversion H.
    - simpl.
      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 df_in_eq l d {struct d} : Istrue (duplicate_free d) -> in_eq l d.
  Proof.
    destruct d as [ | l2 d].
    - intros _ H1 H2.
      inversion H1.
    - simpl.
      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.

Infix "∈" := (Pos2) (at level 60).

Definition subset d1 d2 : Type := forall l, (l ∈ d1) -> (l ∈ d2).

Infix "⊂" := subset (at level 60).

Section types.
  (* Object types are records of types, we define them as association lists *)

  Inductive type :=
  | Empty_type
  | Cons_type : string -> type -> type -> type.

End types.

Section assoc.

  Fixpoint domain A :=
    match A with
      | Empty_type => nil
      | Cons_type l _ C => cons l (domain C)
    end.

  Fixpoint assoc A l (H : l ∈ domain A) : type.
  Proof.
    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 assoc.

(* Scope of object types *)
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" := (assoc A%ty l%string) (at level 50).

  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} : Type :=
    match B with
      | 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).

  Lemma subtype_tail {A} {B} l C :
    A <: B ->
         Cons_type l C A <: B.
  Proof.
    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_refl A : A <: A.
  Proof.
    induction A as [ | l A HA B HB ].
    - intuition.
    - simpl.
      exists (PCons _ (At_head l l (domain B) eq_refl)).
      simpl.
      split.
      + reflexivity.
      + apply subtype_tail.
        assumption.
  Defined.

  Fixpoint domain_subtype {A} {B} :
    A <: B -> domain B ⊂ domain A.
  Proof.
    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.
  Defined.

  Fixpoint assoc_subtype {A} {B} (st : A <: B) l H :
    assoc B l H = assoc A l (domain_subtype st l H).
  Proof.
    destruct B as [ | lB B1 B2].
    - inversion H.
    - rewrite (PCons_destr _ _ (domain B2) H).
      simpl in H.
      generalize (PCons2 H).
      intro p.
      clear H.
      apply (destruct_pos p).
      + intro e.
        simpl.
        destruct e.
        destruct st as (Ha, (Heq, Hst)).
        symmetry.
        assumption.
      + intro H.
        simpl.
        destruct st as (Ha, (Heq, Hst)).
        apply (assoc_subtype A B2 _ l H).
  Defined.

  Theorem subtype_trans {A} B {C} : A <: B -> B <: C -> A <: C.
  Proof.
    induction C as [ | lC C1 C2].
    - trivial.
    - intros stAB (HdBC, (HeqBC, HstBC)).
      exists (domain_subtype stAB lC HdBC).
      split.
      + rewrite <- (assoc_subtype stAB lC HdBC).
        assumption.
      + intuition.
  Qed.
End subtyping.

Infix "<:" := Subtype (at level 60).

Definition insert (lA : string * type) (A2 : type) :=
  let (l, A) := lA in Cons_type l A A2.

      (* Notations for object pretypes:
   [ "l₁" : A₁ ; "l₂" : A₂ ; … ; "lₙ" : Aₙ ]
 *)
Notation "l : A" := (l%string, A) (at level 50) : type_field_scope.
Notation "[ x1 ; .. ; xn ]" :=
  (insert x1%tf .. (insert xn%tf Empty_type) ..) : obj_type_scope.
Notation "l : A :: B" := (Cons_type l A B) (at level 100) : type_field_scope.

Section objects.
  (* Objects are records of methods.
   A well-pretyped object of type A = [ lᵢ : Aᵢ ]
   is of the form [ lᵢ = ς(x !: A) tᵢ ] where x : A ⊢ tᵢ : Aᵢ

   The type A appears 3 times in the definition of well-pretyped object of type A :
    - in each ς binder
    - to type each tᵢ
    - to list the labels

   Since we cannot construct an object without breaking the invariant, we define
   preobjects of type (A, f, d) such that Obj A = Preobject (A, assoc A, domain A).

   *)

  (* We have to axiomatize the type of methods because
   Method A B := Obj A -> Obj B has a negative occurence of Obj which blocks
   the recursive definition
   *)

  Parameter Method : type -> type -> Type.

  Inductive Preobject {A : type} : forall (d : list string), Type :=
  | poempty : Preobject nil
  | pocons : forall {d} (l : string) (H : l ∈ domain A) (Hn : Istrue (negb (mem l d))),
               Method A (assoc A l H) ->
               Preobject d ->
               Preobject (cons l d).

  Definition Preobj A d := @Preobject A d.
  Definition Obj (A : type) := Preobj A (domain A).

  (* 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.

  (* type, object and prooj of subtyping underlying an ecpression *)
  Fixpoint expr_type {A : type} (e : Expr A) : type.
  Proof.
    destruct e as [ o | A' e ].
    - exact A.
    - exact (expr_type A' e).
  Defined.

  Fixpoint 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).
  Defined.

  Fixpoint 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).
  Defined.

  Definition Obj_to_expr {A} : Obj A -> Expr A := Eobj A.

  (* 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.
  Lemma list_destr d : iscons d -> cons (head d) (tail d) = d.
  Proof.
    intro H.
    destruct d.
    - contradiction.
    - simpl.
      reflexivity.
  Defined.

  (* Destruction principle for preobjects *)
  Definition po_destr {A d} (po : Preobj A d) (Hnnil : iscons d) :
    sigT (fun H2 => sigT (fun Hn => sigT (fun m => sigT (fun tl =>
      po = rew (list_destr d Hnnil) in pocons (head d) H2 Hn m tl)))).
  Proof.
    destruct d as [ | l d'].
    - contradiction.
    - destruct po.
      + contradiction.
      + exists H.
               exists Hn.
               exists m.
               exists po.
               simpl in Hnnil.
               unfold list_destr.
               reflexivity.
  Defined.

  (* By construction, types of objects are duplication-free *)
  (* And domains of preobjects are included in domains of objects *)
  Fixpoint po_sub {A d} (po : Preobj A d) : d ⊂ domain A.
  Proof.
    destruct po.
    - intros l p.
      inversion p.
    - intros l2 p.
      apply PCons2 in p.
      destruct p.
      + destruct e.
        assumption.
      + exact (po_sub _ d po l2 p).
  Defined.

  Fixpoint po_df {A d} (po : Preobj A d) : Istrue (duplicate_free d).
  Proof.
    destruct d as [ | l d ].
    - reflexivity.
    - destruct (po_destr po I) as (H2, (Hn, (m, (potl, He)))).
      simpl.
      simpl in Hn.
      rewrite Hn.
      rewrite (po_df A d potl).
      reflexivity.
  Defined.

  Definition obj_in_eq A : Obj A -> forall l, in_eq l (domain A)
    := fun a l => df_in_eq l (domain A) (po_df a).

  Definition obj_po_sub l {A} (a : Obj A) (H : l ∈ domain A) : po_sub a l H = H
    := obj_in_eq A a l _ _.

End objects.

Delimit Scope object_scope with obj.
Delimit Scope method_scope with meth.

Bind Scope method_scope with Method.
Bind Scope object_scope with Preobject.

Infix "⊙" := assoc (at level 50).

Definition Lmethod A := sigT (fun l2 =>
                                sigT (fun H => Method A ((A ⊙ l2) H))%type).

Definition Make_lmeth l A H m : Lmethod A :=
  (existT _ l (existT _ H m)).

Notation "l = 'ς' ( x !: A ) m" :=
  (Make_lmeth l A%ty (mem_pos l (domain A%ty) Istrue_true) (Make_meth (fun x : Expr A%ty => m%obj))) (at level 50) : method_scope.

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).

  Fixpoint preselect l {A d} (po : Preobj A d)
           (H : l ∈ d) {struct H} : Method A (assoc A l (po_sub po l H)).
  Proof.
    destruct H as [ hd tl ].
    destruct (po_destr po I) as (H2, (Hn, (m, (potl, He)))).
    rewrite He.
    destruct p as [ l' d e | l' d]; simpl.
    - destruct e.
      assumption.
    - apply (preselect l A d potl p).
  Defined.

  Fixpoint preupdate l {A d} (po : Preobj A d)
             (H : l ∈ d) : Method A (assoc A l (po_sub po l H)) -> Preobj A d.
  Proof.
    destruct H as [ hd tl ].
    destruct (po_destr po I) as (H2, (Hn, (m2, (potl, He)))).
    rewrite He.
    destruct p as [ l' d e | l' d ].
    - destruct e.
      intro m.
      refine (pocons l H2 Hn _ potl).
      assumption.
    - intro m.
      apply (pocons l' H2 Hn m2).
      apply (preupdate l A d potl p m).
  Defined.

  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)).
  Defined.

  Definition obj_update l {A} (a : Obj A) (H : l ∈ domain A) (m : Method A (assoc A l H)) : Obj A.
  Proof.
    rewrite <- (obj_po_sub l a H) in m.
    exact (preupdate l a H m).
  Defined.

  Definition select l {A} (a : Expr A) (H : l ∈ domain A) : Expr (assoc A l H).
  Proof.
    rewrite (assoc_subtype (expr_st a) l H).
    exact (obj_select l (expr_obj a) (domain_subtype (expr_st a) l H)).
  Defined.

  Definition mem_select l {A} a (H : Istrue (mem l (domain A))) :=
    select l a (mem_pos l (domain A) H).

  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.
    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.
    rewrite <- (assoc_subtype (expr_st a) l H).
    exact (Eval_meth m self).
  Defined.

End semantics.

Notation "a # l" := (mem_select l%string a%obj Istrue_true) (at level 50) : object_scope.
Notation "o ## l ⇐ 'ς' ( x !: A ) m" := (@update l%string A%ty o (mem_pos l (domain A%ty) Istrue_true) (Make_meth (fun x : Expr A%ty => m))) (at level 50).

(* It is often practical to let some methods undefined.
   An easy way to do so is to define an initial object
   of each type and define some methods by update. *)
Section init.

  Definition loop_method A l H: Method A ((A ⊙ l) H) :=
    Make_meth (fun a => @select l A a H).

  Fixpoint preinit A d (Hsub : d ⊂ domain A) (df : Istrue (duplicate_free d)) {struct d} :
    Preobj A d.
  Proof.
    destruct d as [ | l d ].
    - apply poempty.
    - apply (pocons l (Hsub l (PCons _ (At_head l l d eq_refl)))).
      + simpl in df.
        generalize df.
        case (mem l d); intuition.
      + apply loop_method.
      + apply preinit.
        * intros l2 H2.
          apply Hsub.
          apply PCons.
          apply In_tail.
          apply H2.
        * simpl in df.
          generalize df.
          case (mem l d); intuition.
          simpl in df0.
          inversion df0.
  Defined.

  Definition obj_init A : Istrue (duplicate_free (domain A)) -> Obj A :=
    preinit A (domain A) (fun _ H => H).

  Definition init A : Istrue (duplicate_free (domain A)) -> Expr A :=
    fun df => Obj_to_expr (obj_init A df).
End init.

(* Definition of objects without respecting the order of labels given by the type. *)
Definition lmeth_label A (lm : Lmethod A) :=
  let (l, _) := lm in l.
Definition lmeth_H A (lm : Lmethod A) : (lmeth_label A lm) ∈ domain A.
  destruct lm as (l, (H, m)).
  unfold lmeth_label.
  assumption.
Defined.
Definition lmeth_meth A (lm : Lmethod A) : Method A ((A ⊙ (lmeth_label A lm)) (lmeth_H A lm)).
  destruct lm as (l, (H, m)).
  unfold lmeth_label.
  unfold lmeth_H.
  assumption.
Defined.

Definition pocons_3 A (lm : Lmethod A)
           (a : Expr A) :
  Expr A :=
  update (lmeth_label A lm) a (lmeth_H A lm) (lmeth_meth A lm).

Notation "[ m1 ; .. ; mn ]" := (pocons_3 _ m1%meth (.. (pocons_3 _ mn%meth (init _ Istrue_true)) .. )) : object_scope.

Notation "[[ l = 'ς' ( x ) m ; p ]]" := (pocons l (Make_meth (fun x => m)) p) (at level 50) : object_scope.

(* Notation "a < b > .# l" := (preselect l%string _ _ _ a%obj _ b%obj) (at level 50) : object_scope. *)
Notation "o .## l ⇐ 'ς' ( x !: A ) m" := (preupdate l%string A%ty _ _ o (Make_meth A%ty _ (fun x => m))) (at level 50).

Section examples.
  (* Encodding of booleans *)
  Definition BoolT A : type :=
    [ "else" : A ; "if" : A ; "then" : A ]%ty.

  Definition init_bool A : Expr (BoolT A) := init (BoolT A) Istrue_true.

  Definition trueT A : Expr (BoolT A) :=
    pocons_3 _ ("if" = ς(x !: BoolT A) (x # "then"))%meth (init_bool A).

  Definition falseT A : Expr (BoolT A) :=
    pocons_3 _ ("if" = ς(x !: BoolT A) (x # "else"))%meth (init_bool A).

  Definition Ifthenelse A b (t e : Expr A) : Expr A :=
    (((b##"then" ⇐ ς(x !: BoolT A) t)##"else" ⇐ ς(x !: BoolT A) e)#"if")%obj.

  (* Encodding of the simply-pretyped λ-calculus *)

  Definition Arrow A B :=
    [ "arg" : A ; "val" : B ]%ty.

  Definition init_arr A B := init (Arrow A B) Istrue_true.

  Definition Lambda A B (f : Expr A -> Expr B) : Expr (Arrow A B) :=
    pocons_3 _ ("val" = ς(x !: Arrow A B) (f (x#"arg")))%meth (init_arr A B).

  Definition App A B (f : Expr (Arrow A B)) (a : Expr A) : Expr B :=
    ((f##"arg" ⇐ ς(x !: Arrow A B) a)#"val")%obj.
End examples.

Notation "'ifT' b 'then' t 'else' e" := (Ifthenelse _ b t e) (at level 50) : object_scope.
Infix "→" := Arrow (at level 50).
Notation "'λ' ( x !: A ) b" := (Lambda A _ (fun x : Expr A => b)) (at level 50).
Infix "@" := (App _ _) (at level 50).