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
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).
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
  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.
561
  Definition Obj_to_expr {A} : Obj A -> Expr A.
562
563
564
565
566
567
  Proof.
    exists A.
    split.
    - assumption.
    - apply subtype_refl_wf.
  Defined.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
568
569

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

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.

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

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

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

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

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

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

640
  Definition select l {A} (e : Expr A) (H : l  (domain A)) : Expr (assoc A l).
641
642
643
644
    (* 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))).
645
  Defined.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
646

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

673
674
  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
675

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

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

708
709
  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.
710

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

  (* Specification of update: *)

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

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

751
752
  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.
753

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

771
772
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
773

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

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

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

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

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

802
(* Definition of objects without respecting the order of labels given by the pretype. *)
803
804
805
806
807
808
809
810
811
812
813
814
815
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.

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

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

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

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



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

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

903
904
  Eval compute in (fun A => A <: (BoolT A  "then")).

905
906
907
908
909
910
911
912
913
914
915
916
  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
917
918
919
920

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

921
922
  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
923

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

927
928
929
  (* 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
930
931
End examples.

932
933
934
935
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).