coq_obj.v 27 KB
Newer Older
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
1
Require Import String.
2
3
4
5
Require Import Bool.
Require Eqdep_dec.
Require EqdepFacts.
Import EqNotations.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
6

7
8
Axiom fun_ext : forall A B (f g : A -> B),
                  (forall x, f x = g x) -> f = g.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
9

10
11
12
13
14
15
16
17
18
19
20
21
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.

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

22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
Module String_dec.
  Definition U := string.
  Definition eq_dec := string_dec.
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.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
37

38
39
40
41
42
43
44
45
46
47
48
49
50
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.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
51
  Proof.
52
53
    simpl.
    case (string_dec l l); intuition.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
54
55
  Qed.

56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
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. *)

  Fixpoint In_dom l d :=
    match d with
      | nil => False
      | cons l2 d =>
        if (string_dec l l2) then True else In_dom l d
    end.

  Fixpoint Not_in_dom l d :=
    match d with
      | nil => True
      | cons l2 d =>
        if (string_dec l l2) then False else Not_in_dom l d
    end.

  Fixpoint in_dom_dec l d : {In_dom l d} + {Not_in_dom l d}.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
90
  Proof.
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
    destruct d as [ | l2 d ].
    - right. simpl.
      intuition.
    - simpl.
      case (string_dec l l2).
      + left; intuition.
      + intro; apply in_dom_dec; assumption.
  Defined.

  Fixpoint Not_not_in_dom l d : Not_in_dom l d <-> ~ In_dom l d.
  Proof.
    destruct d as [ | l2 d ].
    - simpl.
      intuition.
    - simpl.
      case (string_dec l l2).
      + intuition.
      + intro.
        apply Not_not_in_dom.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
110
111
  Qed.

112
  Fixpoint in_dom_irrel l d : isProp (In_dom l d).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
113
  Proof.
114
115
116
117
118
119
120
121
122
123
124
125
    destruct d as [ | l2 d ].
    - intros H1 H2; destruct H1.
    - simpl.
      case (string_dec l l2).
      + intros e H1 H2.
        destruct H1.
        destruct H2.
        reflexivity.
      + intros n H1 H2.
        apply in_dom_irrel.
  Qed.

126
  Fixpoint not_in_dom_irrel l d : isProp (Not_in_dom l d).
127
128
129
130
131
132
133
134
135
136
137
138
139
  Proof.
    destruct d as [ | l2 d ].
    - simpl. intros H1 H2.
      destruct H1; destruct H2.
      reflexivity.
    - simpl.
      case (string_dec l l2).
      + intros e H1 H2.
        contradiction.
      + intros n H1 H2.
        apply not_in_dom_irrel.
  Qed.

140
141
142
143
144
(* 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).

145
146
End domains.

147
148
(* Properties of  *)

149
150
151
Notation "l ∈ d" := (In_dom l d%ty) (at level 60).
Notation "l ∉ d" := (Not_in_dom l d%ty) (at level 60).

152
Definition in_cons_hd l d : l  cons l d.
153
154
155
Proof.
  simpl.
  case (string_dec l l); intuition.
156
Defined.
157

158
Lemma in_cons_tl {l1} l2 {d} : l1  d -> l1  cons l2 d.
159
160
161
Proof.
  simpl.
  case (string_dec l1 l2); intuition.
162
Defined.
163

164
Lemma in_cons_diff {l1} l2 {d} : l1 <> l2 -> l1  cons l2 d -> l1  d.
165
166
167
168
Proof.
  intro diff.
  simpl.
  case (string_dec l1 l2); intuition.
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
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.
223
224
225
226
227
228
229
230
231
232
Qed.

Section subtyping.

  Notation "A ⊙ l" := (preassoc A%ty l%string) (at level 50).

  Fixpoint pretype_dec (A B : pretype) : {A = B} + {A <> B}.
  Proof.
    decide equality.
    apply string_dec.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
233
234
  Qed.

235
236
237
238
239
240
241
242
243
244
  (* Definition of the subtyping relation: A <: B if B is a subset of A. *)
  Fixpoint Subtype A B {struct B} :=
    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
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
245
    end.
246
247
248
249

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

  Fixpoint subtype_dec A B : {A <: B} + {~ A <: B}.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
250
  Proof.
251
252
253
254
255
256
257
    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).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
258
259
  Qed.

260
  Lemma subtype_empty {A} : Empty_pretype <: A -> A = Empty_pretype.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
261
  Proof.
262
263
264
265
    destruct A.
    - trivial.
    - simpl.
      case (in_dom_dec s nil); contradiction.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
266
267
  Qed.

268
  Lemma subtype_cons_weaken {A} {B} {l} C :
269
270
271
272
273
274
275
    A <: B ->
         l  predomain A ->
         Cons_pretype l C A <: B.
  Proof.
    induction B.
    - intuition.
    - simpl.
276
277
      pose Not_not_in_dom.
      pose @in_cons_tl.
278
      case (in_dom_dec s (predomain A));
279
280
281
282
283
284
285
        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.
286
  Qed.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
287

288
  Section subtype_reflexivity.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
289

290
291
292
293
294
295
296
297
298
    (* 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.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
299

300
301
302
303
304
305
    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.

306
307
308
309
310
311
312
    Definition type_norm A : A = existT well_formed_type (carrier A) (carrier_wf A).
    Proof.
      destruct A.
      simpl.
      reflexivity.
    Defined.

313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
    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.

328
    Fixpoint well_formed_irrel {A} : isProp (well_formed_type A).
329
    Proof.
330
      intros H1 H2.
331
332
333
334
335
336
337
338
339
340
341
342
343
      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.

344
345
346
347
348
349
350
351
352
    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.

353
354
355
    Definition wf_decide A : bool :=
      if well_formed_dec A then true else false.

356
    Lemma wf_decide_spec {A} : well_formed_type A <-> wf_decide A = true.
357
358
359
360
361
    Proof.
      unfold wf_decide.
      case (well_formed_dec); intuition; discriminate.
    Qed.

362
    Lemma wf_decide_true {A} : wf_decide A = true -> well_formed_type A.
363
364
365
366
367
    Proof.
      rewrite wf_decide_spec.
      trivial.
    Qed.

368
    Theorem subtype_refl_eq {B} : forall {A}, A = B -> well_formed_type A -> A <: B.
369
370
371
372
373
374
375
376
377
    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.
378
        refine (subtype_cons_weaken _ _ _);
379
380
381
382
          [ refine (IH2 B2 eq_refl _) | ];
          intuition.
    Defined.

383
384
    Definition subtype_refl {A} : well_formed_type A -> A <: A
      := subtype_refl_eq eq_refl.
385
386
387
388
389
390
391
392
393

    Definition subtype_refl_wf A : carrier A <: carrier A.
    Proof.
      destruct A as (A', wf).
      simpl.
      apply subtype_refl.
      assumption.
    Defined.

394
395
    Theorem well_formed_preassoc {A} l :
      well_formed_type A -> well_formed_type (preassoc A l).
396
397
398
399
400
401
402
403
404
405
    Proof.
      induction A.
      - trivial.
      - simpl.
        case (string_dec l s).
        + intuition.
        + intros.
          apply IHA2.
          intuition.
    Defined.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
406

407
408
409
410
411
412
413
414
415
416
417
418
419
420
    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. *)

421
  Lemma predomain_subtype {A} {B} l : A <: B -> l  predomain B -> l  predomain A.
422
423
424
425
426
427
  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.
428
429
      destruct e.
      intuition.
430
431
  Qed.

432
433
  Lemma preassoc_subtype {A} {B} {l} :
    A <: B -> l  predomain B -> preassoc A l = preassoc B l.
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
  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.
  Defined.

  Lemma preassoc_subtype_wf A B l : carrier A <: carrier B -> l  domain B -> assoc A l = assoc B l.
  Proof.
    destruct A as (A, wfA).
    destruct B as (B, wfB).
    simpl.
    intros st ldom.
    assert (H : A  l = B  l) by (apply preassoc_subtype; assumption).
454
    apply (sigT_eq H).
455
456
457
    apply well_formed_irrel.
  Defined.

458
  Theorem subtype_trans {A} B {C} : A <: B -> B <: C -> A <: C.
459
460
461
462
463
464
465
466
467
468
469
470
471
472
  Proof.
    induction C.
    - trivial.
    - simpl.
      case (in_dom_dec s (predomain B)).
      + case (in_dom_dec s (predomain A)).
        *
          {
            intros sdA sdB HAB.
            case (pretype_dec C1 (preassoc B s)).
            + case (pretype_dec C1 (preassoc A s)).
              * intuition.
              * intros n e _.
                apply n.
473
                rewrite (preassoc_subtype HAB sdB).
474
475
476
477
478
479
                assumption.
            + contradiction.
          }
        * intros n e HAB _.
          rewrite Not_not_in_dom in n.
          apply n.
480
          apply (predomain_subtype s HAB).
481
482
483
484
485
486
487
488
489
          assumption.
      + contradiction.
  Qed.
End subtyping.

Notation "<< A >>" := (carrier A) (at level 0).
Notation "A <: B" := (Subtype <<A>> <<B>>) (at level 60).

Definition Empty_type : type := existT _ Empty_pretype I.
490
491

Fixpoint insert (lA : string * type) (A2 : type) : type.
492
493
494
495
496
497
498
499
500
501
Proof.
  destruct lA as (l, A1).
  case (in_dom_dec l (predomain <<A2>>)).
  - intro; exact A2.
  - intro n.
    exists (Cons_pretype l <<A1>> <<A2>>).
    simpl.
    intuition; apply carrier_wf.
Defined.

502
      (* Notations for object pretypes:
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
503
504
505
506
   [ "l₁" : A ; "l₂" : A ;  ; "lₙ" : A ]
 *)
Notation "l : A" := (l%string, A) (at level 50) : type_field_scope.
Notation "[ x1 ; .. ; xn ]" :=
507
508
  (insert x1%tf .. (insert xn%tf Empty_type) ..) : obj_type_scope.
Notation "l : A :: B" := (Cons_pretype l A B) (at level 100) : type_field_scope.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
509
510
511

Section objects.
  (* Objects are records of methods.
512
   A well-pretyped object of pretype A = [ l : A ]
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
513
514
   is of the form [ l = ς(x !: A) t ] where x : A  t : A

515
   The pretype A appears 3 times in the definition of well-pretyped object of pretype A :
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
516
    - in each ς binder
517
    - to pretype each t
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
518
519
520
    - to list the labels

   Since we cannot construct an object without breaking the invariant, we define
521
   preobjects of pretype (A, f, d) such that Obj A = Preobject (A, preassoc A, predomain A).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
522
523
524

   *)

525
  (* We have to axiomatize the pretype of methods because
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
526
527
528
529
530
531
   Method A B := Obj A -> Obj B has a negative occurence of Obj which blocks
   the recursive definition
   *)

  Parameter Method : type -> type -> Type.

532
533
534
  Inductive Preobject {A : type} {f : string -> type} : forall (d : list string), Type :=
  | poempty : Preobject nil
  | pocons : forall {d} (l : string),
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
535
               Method A (f l) ->
536
537
               Preobject d ->
               Preobject (cons l d).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
538

539
540
  Definition Preobj A f d := @Preobject A f d.
  Definition Obj (A : type) := Preobj A (assoc A) (domain A).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
541

542
543
  (* An expression of pretype B is an object of pretype A <: B coerced to pretype B. *)
  Definition Expr (B : type) := sigT (fun A => ((Obj A) * (A <: B))%type).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
544

545
  Definition Obj_to_expr {A} : Obj A -> Expr A.
546
547
548
549
550
551
  Proof.
    exists A.
    split.
    - assumption.
    - apply subtype_refl_wf.
  Defined.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
552
553

  (* End of the axiomatisation of methods: Method A B is equivalent to Obj A -> Obj B. *)
554
555
556
  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.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
557
558
559
560
561
562
563
564
565

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.

566
Infix "⊙" := assoc (at level 50).
567
568
569
570
571
572
573
574
575

Definition Lmethod A := sigT (fun l2 =>
                                ((l2  domain A) * Method A (A  l2))%type).

Definition Make_lmeth l A m H : Lmethod A :=
  (existT (fun l2 => (prod (l2  domain A) (Method A (A  l2))))
          l
          (H, (Make_meth m))).

Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
576
Notation "l = 'ς' ( x !: A ) m" :=
577
  (Make_lmeth l A%ty (fun x : Expr A%ty => m%obj) I) (at level 50) : method_scope.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
578

579
Notation "o ↑ A" := (@Obj_to_expr A%ty o) (at level 100).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
580
581
582

Section semantics.
  (* Selection and update go inside objects so they have to be defined on preobjects first. *)
583
  Definition coerce {B} {C} (HBC : B <: C) : Expr B -> Expr C.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
584
  Proof.
585
    intros (A, (a, st)).
586
587
588
    exists A.
    split.
    - exact a.
589
    - apply (subtype_trans <<B>>); assumption.
590
  Qed.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
591

592
593
594
595
596
597
598
599
600
601
602
603
  Definition empty_object : Obj Empty_type := poempty.
  Definition empty_expression : Expr Empty_type := Obj_to_expr empty_object.

  Definition pre_head {l} {A} {f} {d} (po : Preobj A f (cons l d)) : Method A (f l) :=
    match po with
      | pocons _ _ m _ => m
    end.

  Definition pre_tail {l} {A} {f} {d} (po : Preobj A f (cons l d)) : Preobject d :=
    match po with
      | pocons _ _ _ tl => tl
    end.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
604

605
606
607
  Fixpoint preselect_cons {l} {A} {f} {l2} {d} (po : Preobj A f (cons l2 d))
           (H : Position l l2 d) :
    Method A (f l).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
608
  Proof.
609
610
611
612
613
614
615
616
617
618
619
620
621
    destruct H.
    + exact (pre_head po).
    + apply (preselect_cons l A f hd d (pre_tail po)).
      assumption.
  Defined.

  Definition preselect l {A} {f} {d} (po : Preobj A f d) (H : l  d) : Method A (f l).
  Proof.
    destruct d as [ | l2 d ].
    - destruct H.
    - apply (preselect_cons po).
      apply in_dom_pos.
      assumption.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
622
623
  Defined.

624
  Definition select l {A} (e : Expr A) (H : l  (domain A)) : Expr (assoc A l).
625
626
    destruct e as (A', (a', st)).
    rewrite <- (preassoc_subtype_wf A' A l st H).
627
628
    exact (Eval_meth (preselect l a' (predomain_subtype l st H))
                     (Obj_to_expr a')).
629
  Defined.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
630

631
632
633
  Fixpoint preupdate_cons l {A} {f} {l2} {d} (po : Preobj A f (cons l2 d))
           (m : Method A (f l)) (H : Position l l2 d)
           : Preobj A f (cons l2 d).
634
  Proof.
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
    destruct H.
    - exact (pocons _ m (pre_tail po)).
    - apply (pocons _ (pre_head po)).
      apply (preupdate_cons l).
      + exact (pre_tail po).
      + exact m.
      + exact H.
  Defined.

  Definition preupdate l {A} {f} {d} (po : Preobj A f d) :
    Method A (f l) -> l  d -> Preobj A f d.
  Proof.
    destruct d as [ | l2 d ].
    - contradiction.
    - intros.
      apply (preupdate_cons l).
      + assumption.
      + assumption.
      + apply in_dom_pos.
        assumption.
655
  Defined.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
656

657
658
  Definition obj_update l {A} (a : Obj A) m H : Obj A :=
    preupdate l a m H.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
659

660
661
662
663
664
  Definition update l A (e : Expr A) (m : Method A (assoc A l)) (H : l  domain A) : Expr A.
  Proof.
    destruct e as (A', (a', st)).
    exists A'.
    split.
665
    - apply (obj_update l a').
666
667
668
      apply Make_meth.
      intro self.
      rewrite (preassoc_subtype_wf A' A l st H).
669
670
      apply (Eval_meth m).
      apply (coerce st).
671
      exact self.
672
      exact (predomain_subtype l st H).
673
674
    - assumption.
  Defined.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
675

676
  (* Specification of select: *)
677
678
  Theorem presel_cons_eq {l1} {l2} {A} {f} {d} (m1 : Method A (f l1)) (po : Preobj A f d) :
    forall H, forall e : l2 = l1, preselect l2 (pocons l1 m1 po) H = rew <- (f_equal f e) in m1.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
679
  Proof.
680
681
682
683
684
685
686
687
    unfold preselect.
    intro H.
    generalize (in_dom_pos l1 H).
    intro H2; destruct H2.
    - intro e.
      simpl.
      assert (He : e = eq_refl) by apply String_UIP.UIP.
      rewrite He.
688
      reflexivity.
689
    - intro e; destruct (n e).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
690
691
  Qed.

692
693
  Definition presel_cons l {A} {f} {d} m1 (po : Preobj A f d) H : preselect l (pocons l m1 po) H = m1
    := presel_cons_eq m1 po H eq_refl.
694

695
  Theorem presel_cons_diff l l2 A f d m1 (po : Preobj A f d) H :
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
696
    l <> l2 ->
697
698
    preselect l (pocons l2 m1 po) (in_cons_tl l2 H)
    = preselect l po H.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
699
700
  Proof.
    intro diff.
701
702
703
704
705
706
707
708
    unfold preselect.
    generalize (in_dom_pos l2 (in_cons_tl l2 H)).
    intro H2.
    destruct H2.
    - destruct (diff eq_refl).
    - simpl.
      apply f_equal.
      apply pos_irrel.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
709
710
711
712
  Qed.

  (* Specification of update: *)

713
714
  Theorem preup_irrel l {A f d} (p : Preobj A f d) m H1 H2 :
    preupdate l p m H1 = preupdate l p m H2.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
715
  Proof.
716
717
    apply f_equal.
    apply in_dom_irrel.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
718
719
  Qed.

720
  Theorem preup_cons_eq {A f d} l1 l2 (po : Preobj A f d) m1 m2 :
721
    forall e : l2 = l1, forall H,
722
      preupdate l2 (pocons l1 m1 po) m2 H = pocons l1 (rew (f_equal f e) in m2) po.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
723
  Proof.
724
725
    intros e H.
    simpl.
726
727
728
729
730
    generalize (in_dom_pos l1 H); intro H2.
    destruct H2.
    - simpl.
      assert (He : e = eq_refl) by apply String_UIP.UIP.
      rewrite He.
731
      reflexivity.
732
    - destruct (n e).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
733
734
  Qed.

735
736
  Definition preup_cons_eq2 {A f d} l (po : Preobj A f d) m1 m2 : forall H, preupdate l (pocons l m1 po) m2 H = pocons l m2 po
    := preup_cons_eq l l po m1 m2 eq_refl.
737

738
  Theorem preup_cons_diff {A f d} l l2 m1 m2 (po : Preobj A f d) H1 H2:
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
739
    l <> l2 ->
740
741
    preupdate l (pocons l2 m1 po) m2 H1
    = pocons l2 m1 (preupdate l po m2 H2).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
742
  Proof.
743
    simpl.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
744
    intro diff.
745
746
747
748
    generalize (in_dom_pos l2 H1); intro H3;
    destruct H3.
    - destruct (diff eq_refl).
    - simpl.
749
750
      apply f_equal.
      apply f_equal.
751
      apply pos_irrel.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
752
753
754
  Qed.
End semantics.

755
756
Notation "a # l" := (select l%string a%obj I) (at level 50) : object_scope.
Notation "o ## l ⇐ 'ς' ( x !: A ) m" := (update l%string A%ty o (Make_meth (fun x : Expr A%ty => @coerce _ (A%ty  l) (subtype_refl_wf (A%ty  l)) m)) I) (at level 50).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
757

758
759
760
(* It is often practical to let some methods undefined.
   An easy way to do so is to define an initial object
   of each pretype and define some methods by update. *)
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
761
Section init.
762

763
764
  Definition loop_method A l H: Method A (A  l) :=
    Make_meth (fun a => @select l A a H).
765
766

  Fixpoint preinit A d :
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
767
    (forall l, l  d -> l  domain A) ->
768
    Preobj A (assoc A) d :=
769
    match d return
770
          (forall l, l  d -> l  domain A) -> Preobj A (assoc A) d
771
    with
772
      | nil => fun _ => poempty
773
774
      | cons l d =>
        fun H =>
775
          pocons l
776
777
                 (loop_method A l (H l (in_cons_hd l d)))
                 (preinit A d (fun l1 H1 =>
778
                                    H l1 (in_cons_tl l H1)))
779
780
781
    end.

  Definition obj_init A : Obj A := preinit A (domain A) (fun _ H => H).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
782

783
  Definition init A : Expr A := Obj_to_expr (obj_init A).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
784
785
End init.

786
(* Definition of objects without respecting the order of labels given by the pretype. *)
787
Definition pocons_3 A (lm : Lmethod A)
788
789
790
791
792
           (a : Expr A) :
  Expr A :=
  let (l, Hm) := lm in
  let (H, m) := Hm in
  update l A a m H.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
793
794
795

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

796
Notation "[[ l = 'ς' ( x ) m ; p ]]" := (pocons l (Make_meth (fun x => m)) p) (at level 50) : object_scope.
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864

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



Ltac reduce_equality :=
  try reflexivity;
  match goal with
    | |- context [Eval_meth _ _ (Make_meth _ _ ?f) ?a] =>
      rewrite beta
    | |- context [pocons_3 _ _ _] => unfold pocons_3
    | |- context [eq_rect ?x _ _ ?x eq_refl] => unfold eq_rect
    | |- pocons ?A ?f ?d ?l ?m _ = pocons ?A ?f ?d ?l ?m _ =>
      apply (f_equal (pocons A f d l m))

    | |- context [ pocons ?A ?f ?d ?l ?m ?p] =>
      let d' := (eval hnf in d) in
      let m' := (eval hnf in m) in
      let p' := (eval hnf in p) in
      let a' := (eval hnf in (pocons A f d' l m' p')) in
      progress change (pocons A f d l m p) with a'

    | |- context [ init _ ] => unfold init
    | |- context [ preinit ?A ?d ?H ] =>
      let d' := (eval hnf in d) in
      let a' := (eval hnf in (preinit A d' H)) in
      progress change (preinit A d H) with a'
    | |- Make_meth ?A ?B _  = Make_meth ?A ?B _ =>
      apply (f_equal (Make_meth A B))

    | |- context [ update ?A ?l ?a ?m] =>
      let m' := (eval hnf in m) in
      let a' := (eval hnf in (update A l a m')) in
      progress change (update A l a m) with a'
    | |- context [ preupdate ?l ?A ?f ?d ?p ?m] =>
      let m' := (eval hnf in m) in
      let a' := (eval hnf in (preupdate l A f d p m')) in
      progress change (preupdate l A f d p m) with a'

    | |- context [select ?l ?A ?p ?H] =>
      let a' := (eval hnf in (select l A p H)) in
      progress change (select l A p H) with a'
    | |- context [preselect ?l ?A ?f ?d ?p ?H ?a] =>
      let a' := (eval hnf in (preselect l A f d p H a)) in
      progress change (preselect l A f d p H a) with a'

    | |- context [ coerce ?A ?B ?H ?a ] =>
      let a' := (eval hnf in a) in
      let b' := (eval hnf in (coerce A B H a')) in
      progress change (coerce A B H a) with b'

    | |- ?f ?a = ?f ?b =>
      let a' := (eval hnf in a) in
      let b' := (eval hnf in b) in
      progress change (f a' = f b')

    | |- (fun _ => _) = (fun _ => _) => apply fun_ext; intro
    | |- (preselect ?l ?A ?f ?d ?p1 eq_refl ?a1) = (preselect ?l ?A ?f ?d ?p2 eq_refl ?a2) =>
      apply (f_equal2 (fun p a => preselect l A f d p eq_refl a))
    | |- (pocons ?A ?f ?d ?l ?m1 ?p1) = (pocons ?A ?f ?d ?l ?m2 ?p2) =>
      apply (f_equal2 (pocons A f d l))
    | |- ?a = ?b =>
      let a' := (eval hnf in a) in
      let b' := (eval hnf in b) in
      progress change (a' = b')
  end.

Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
865
866
Section examples.
  (* Encodding of booleans *)
867
868
869
870
871
872
873
874
875
  Definition BoolT A : type :=
    [ "else" : A ; "if" : A ; "then" : A ]%ty.

  Definition trueT A : Expr (BoolT A) :=
    [ "if" = ς(x !: BoolT A) (x # "then") ]%obj.

  Definition falseT A : Expr (BoolT A) :=
    [ "if" = ς(x !: BoolT A) (x # "else") ]%obj.

876
877
  Eval compute in (fun A => A <: (BoolT A  "then")).

878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
  Definition Ifthenelse A b (t e : Expr A) : Expr A :=
    (((b##"then"  ς(x !: BoolT A) t)##"else"  ς(x !: BoolT A) e)#"if")%obj.

  (* Theorem if_true A b c : Ifthenelse A (trueT A) b c = b. *)
  (* Proof. *)
  (*   transitivity (((["if" = ς (x !: BoolT A)(x # "then")] ## "then"   ς  (_ !: BoolT A)b) *)
  (*               ## "else"   ς  (_ !: BoolT A)c) # "if")%obj. *)
  (*   - reflexivity. *)
  (*   - transitivity ((["if" = ς (x !: BoolT A) (x # "then"); *)
  (*                     "then" = ς (x !: BoolT A) b; *)
  (*                     "else" = ς (x !: BoolT A) c])#"if")%obj. *)
  (*     + reflexivity. *)
  (*     + transitivity ((["if" = ς (x !: BoolT A) (x # "then"); *)
  (*                     "then" = ς (x !: BoolT A) b; *)
  (*                     "else" = ς (x !: BoolT A) c])#"then")%obj. *)
  (*       * unfold preassoc_subtype_wf. *)
  (*         unfold subtype_refl_wf. *)
  (*         unfold subtype_refl. *)
  (*         unfold subtype_refl_eq. *)
  (*       reduce_equality. *)
  (*   reduce_equality. *)
  (*   reduce_equality. *)
  (*   reduce_equality. *)
  (*   reduce_equality. *)
  (*   reduce_equality. *)
  (*   reduce_equality. *)
  (*   reduce_equality. *)
  (*   reduce_equality. *)
  (*   reduce_equality. *)
  (*   reduce_equality. *)
  (*   reduce_equality. *)
  (*   reduce_equality. *)
  (*   reduce_equality. *)
  (*   unfold init. *)
  (*   unfold Obj_to_expr. *)
  (*   simpl. *)
  (*   repeat (reduce_equality || simpl). *)
  (* Qed. *)

  (* Theorem if_false A b c : Ifthenelse A (falseT A) b c = c. *)
  (* Proof. *)
  (*   repeat (reduce_equality || simpl). *)
  (* Qed. *)

  (* Encodding of the simply-pretyped λ-calculus *)
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
923
924
925
926

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

927
928
  Definition Lambda A B (f : Expr A -> Expr B) : Expr (Arrow A B) :=
    [ "val" = ς(x !: Arrow A B) (f (x#"arg")) ]%obj.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
929

930
931
  Definition App A B (f : Expr (Arrow A B)) (a : Expr A) : Expr B :=
    ((f##"arg"  ς(x !: Arrow A B) a)#"val")%obj.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
932

933
934
935
936
  (* Theorem beta_red A B f c : App A B (Lambda A B f) c = f c. *)
  (* Proof. *)
  (*   repeat (reduce_equality || simpl). *)
  (* Qed. *)
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
937
938
End examples.

939
940
941
942
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).