coq_obj.v 26.9 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
37
38
39
40
41
42
43
44
45
46
47
48
Module String_dec.
  Definition U := string.
  Definition eq_dec := string_dec.
End String_dec.

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

  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
49
  Proof.
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
    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
69
70
  Qed.

71
  Fixpoint in_dom_irrel l d : isProp (In_dom l d).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
72
  Proof.
73
74
75
76
77
78
79
80
81
82
83
84
    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.

85
  Fixpoint not_in_dom_irrel l d : isProp (Not_in_dom l d).
86
87
88
89
90
91
92
93
94
95
96
97
98
  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.

99
100
101
102
103
(* 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).

104
105
End domains.

106
107
(* Properties of  *)

108
109
Notation "l ∈ d" := (In_dom l d) (at level 60).
Notation "l ∉ d" := (Not_in_dom l d) (at level 60).
110

111
Definition in_cons_hd l d : l  cons l d.
112
113
114
Proof.
  simpl.
  case (string_dec l l); intuition.
115
Defined.
116

117
Lemma in_cons_tl {l1} l2 {d} : l1  d -> l1  cons l2 d.
118
119
120
Proof.
  simpl.
  case (string_dec l1 l2); intuition.
121
Defined.
122

123
Lemma in_cons_diff {l1} l2 {d} : l1 <> l2 -> l1  cons l2 d -> l1  d.
124
125
126
127
Proof.
  intro diff.
  simpl.
  case (string_dec l1 l2); intuition.
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
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.
182
183
Qed.

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
223
224
225
226


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.

227
228
229
230
231
232
233
234
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
235
236
  Qed.

237
238
239
240
241
242
243
244
245
246
  (* 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
247
    end.
248
249
250
251

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

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

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

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

290
  Section subtype_reflexivity.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
291

292
293
294
295
296
297
298
299
300
    (* 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
301

302
303
304
305
306
307
    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.

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

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

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

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

355
356
357
    Definition wf_decide A : bool :=
      if well_formed_dec A then true else false.

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

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

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

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

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

396
397
    Theorem well_formed_preassoc {A} l :
      well_formed_type A -> well_formed_type (preassoc A l).
398
399
400
401
402
403
404
405
406
407
    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
408

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

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

434
435
  Lemma preassoc_subtype {A} {B} {l} :
    A <: B -> l  predomain B -> preassoc A l = preassoc B l.
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
  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).
456
    apply (sigT_eq H).
457
458
459
    apply well_formed_irrel.
  Defined.

460
  Theorem subtype_trans {A} B {C} : A <: B -> B <: C -> A <: C.
461
462
463
464
465
466
467
468
469
470
471
472
473
474
  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.
475
                rewrite (preassoc_subtype HAB sdB).
476
477
478
479
480
481
                assumption.
            + contradiction.
          }
        * intros n e HAB _.
          rewrite Not_not_in_dom in n.
          apply n.
482
          apply (predomain_subtype s HAB).
483
484
485
486
487
488
489
490
491
          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.
492
493

Fixpoint insert (lA : string * type) (A2 : type) : type.
494
495
496
497
498
499
500
501
502
503
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.

504
      (* Notations for object pretypes:
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
505
506
507
508
   [ "l₁" : A ; "l₂" : A ;  ; "lₙ" : A ]
 *)
Notation "l : A" := (l%string, A) (at level 50) : type_field_scope.
Notation "[ x1 ; .. ; xn ]" :=
509
510
  (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
511
512
513

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

517
   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
518
    - in each ς binder
519
    - to pretype each t
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
520
521
522
    - to list the labels

   Since we cannot construct an object without breaking the invariant, we define
523
   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
524
525
526

   *)

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

  Parameter Method : type -> type -> Type.

534
535
536
  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
537
               Method A (f l) ->
538
539
               Preobject d ->
               Preobject (cons l d).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
540

541
542
  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
543

544
545
  (* 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).
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
  Definition expr_type {B : type} (e : Expr B) : type.
  Proof.
    destruct e as (A, _).
    exact A.
  Defined.
  Definition expr_obj {B : type} (e : Expr B) : Obj (expr_type e).
  Proof.
    destruct e as (A, (a, st)).
    unfold expr_type.
    assumption.
  Defined.
  Definition expr_st {B : type} (e : Expr B) : (expr_type e) <: B.
  Proof.
    destruct e as (A, (a, st)).
    unfold expr_type.
    assumption.
  Defined.
563
  Definition Obj_to_expr {A} : Obj A -> Expr A.
564
565
566
567
568
569
  Proof.
    exists A.
    split.
    - assumption.
    - apply subtype_refl_wf.
  Defined.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
570
571

  (* End of the axiomatisation of methods: Method A B is equivalent to Obj A -> Obj B. *)
572
573
574
  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
575
576
577
578
579
580
581
582
583

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.

584
Infix "⊙" := assoc (at level 50).
585
586
587
588
589
590
591
592
593

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
594
Notation "l = 'ς' ( x !: A ) m" :=
595
  (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
596

597
Notation "o ↑ A" := (@Obj_to_expr A%ty o) (at level 100).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
598
599
600

Section semantics.
  (* Selection and update go inside objects so they have to be defined on preobjects first. *)
601
  Definition coerce {B} {C} (HBC : B <: C) : Expr B -> Expr C.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
602
  Proof.
603
    intros (A, (a, st)).
604
605
606
    exists A.
    split.
    - exact a.
607
    - apply (subtype_trans <<B>>); assumption.
608
  Qed.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
609

610
611
612
613
614
615
616
617
618
619
620
621
  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
622

623
624
625
  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
626
  Proof.
627
628
629
630
631
632
633
634
635
636
637
638
639
    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
640
641
  Defined.

642
  Definition select l {A} (e : Expr A) (H : l  (domain A)) : Expr (assoc A l).
643
644
645
646
    (* destruct e as (A', (a', st)). *)
    rewrite <- (preassoc_subtype_wf (expr_type e) A l (expr_st e) H).
    exact (Eval_meth (preselect l (expr_obj e) (predomain_subtype l (expr_st e) H))
                     (Obj_to_expr (expr_obj e))).
647
  Defined.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
648

649
650
651
  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).
652
  Proof.
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
    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.
673
  Defined.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
674

675
676
  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
677

678
679
  Definition update l A (e : Expr A) (m : Method A (assoc A l)) (H : l  domain A) : Expr A.
  Proof.
680
681
    (* destruct e as (A', (a', st)). *)
    exists (expr_type e).
682
    split.
683
    - apply (obj_update l (expr_obj e)).
684
685
      apply Make_meth.
      intro self.
686
      rewrite (preassoc_subtype_wf (expr_type e) A l (expr_st e) H).
687
      apply (Eval_meth m).
688
      apply (coerce (expr_st e)).
689
      exact self.
690
691
      exact (predomain_subtype l (expr_st e) H).
    - exact (expr_st e).
692
  Defined.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
693

694
  (* Specification of select: *)
695
696
  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
697
  Proof.
698
699
700
701
702
703
704
705
    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.
706
      reflexivity.
707
    - intro e; destruct (n e).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
708
709
  Qed.

710
711
  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.
712

713
  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
714
    l <> l2 ->
715
716
    preselect l (pocons l2 m1 po) (in_cons_tl l2 H)
    = preselect l po H.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
717
718
  Proof.
    intro diff.
719
720
721
722
723
724
725
726
    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
727
728
729
730
  Qed.

  (* Specification of update: *)

731
732
  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
733
  Proof.
734
735
    apply f_equal.
    apply in_dom_irrel.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
736
737
  Qed.

738
  Theorem preup_cons_eq {A f d} l1 l2 (po : Preobj A f d) m1 m2 :
739
    forall e : l2 = l1, forall H,
740
      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
741
  Proof.
742
743
    intros e H.
    simpl.
744
745
746
747
748
    generalize (in_dom_pos l1 H); intro H2.
    destruct H2.
    - simpl.
      assert (He : e = eq_refl) by apply String_UIP.UIP.
      rewrite He.
749
      reflexivity.
750
    - destruct (n e).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
751
752
  Qed.

753
754
  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.
755

756
  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
757
    l <> l2 ->
758
759
    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
760
  Proof.
761
    simpl.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
762
    intro diff.
763
764
765
766
    generalize (in_dom_pos l2 H1); intro H3;
    destruct H3.
    - destruct (diff eq_refl).
    - simpl.
767
768
      apply f_equal.
      apply f_equal.
769
      apply pos_irrel.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
770
771
772
  Qed.
End semantics.

773
774
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
775

776
777
778
(* 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
779
Section init.
780

781
782
  Definition loop_method A l H: Method A (A  l) :=
    Make_meth (fun a => @select l A a H).
783
784

  Fixpoint preinit A d :
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
785
    (forall l, l  d -> l  domain A) ->
786
    Preobj A (assoc A) d :=
787
    match d return
788
          (forall l, l  d -> l  domain A) -> Preobj A (assoc A) d
789
    with
790
      | nil => fun _ => poempty
791
792
      | cons l d =>
        fun H =>
793
          pocons l
794
795
                 (loop_method A l (H l (in_cons_hd l d)))
                 (preinit A d (fun l1 H1 =>
796
                                    H l1 (in_cons_tl l H1)))
797
798
799
    end.

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

801
  Definition init A : Expr A := Obj_to_expr (obj_init A).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
802
803
End init.

804
(* Definition of objects without respecting the order of labels given by the pretype. *)
805
806
807
808
809
810
811
812
813
814
815
816
817
Definition lmeth_label A (lm : Lmethod A) :=
  let (l, _) := lm in l.
Definition lmeth_meth A (lm : Lmethod A) : Method A (A  (lmeth_label A lm)).
  destruct lm as (l, (H, m)).
  unfold lmeth_label.
  assumption.
Defined.
Definition lmeth_H A (lm : Lmethod A) : (lmeth_label A lm)  domain A.
  destruct lm as (l, (H, m)).
  unfold lmeth_label.
  assumption.
Defined.

818
Definition pocons_3 A (lm : Lmethod A)
819
820
           (a : Expr A) :
  Expr A :=
821
  update (lmeth_label A lm) A a (lmeth_meth A lm) (lmeth_H A lm).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
822
823
824

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

825
Notation "[[ l = 'ς' ( x ) m ; p ]]" := (pocons l (Make_meth (fun x => m)) p) (at level 50) : object_scope.
826
827
828
829
830
831

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



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
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
(* 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. *)
893

Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
894
895
Section examples.
  (* Encodding of booleans *)
896
897
898
899
900
901
902
903
904
  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.

905
906
  Eval compute in (fun A => A <: (BoolT A  "then")).

907
908
909
910
911
912
913
914
915
916
917
918
  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. *)
  (* Qed. *)

  (* Theorem if_false A b c : Ifthenelse A (falseT A) b c = c. *)
  (* Proof. *)
  (* Qed. *)

  (* Encodding of the simply-pretyped λ-calculus *)
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
919
920
921
922

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

923
924
  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
925

926
927
  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
928

929
930
931
  (* Theorem beta_red A B f c : App A B (Lambda A B f) c = f c. *)
  (* Proof. *)
  (* Qed. *)
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
932
933
End examples.

934
935
936
937
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).