coq_obj.v 24.4 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
22
23
24
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
25

26
27
28
29
30
31
32
33
34
35
36
37
38
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
39
  Proof.
40
41
    simpl.
    case (string_dec l l); intuition.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
42
43
  Qed.

44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
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
78
  Proof.
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
    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
98
99
  Qed.

100
  Fixpoint in_dom_irrel l d {struct d}: forall H1 H2 : In_dom l d, H1 = H2.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
101
  Proof.
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
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
    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.

  Fixpoint not_in_dom_irrel l d {struct d}: forall H1 H2 : Not_in_dom l d, H1 = H2.
  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.

End domains.

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

(* Properties of  *)

Definition in_cons_hd l d : l  (cons l d).
Proof.
  simpl.
  case (string_dec l l); intuition.
Qed.

Lemma in_cons_tl l1 l2 d : l1  d -> l1  (cons l2 d).
Proof.
  simpl.
  case (string_dec l1 l2); intuition.
Qed.

Lemma in_cons_diff l1 l2 d : l1 <> l2 -> l1  (cons l2 d) -> l1  d.
Proof.
  intro diff.
  simpl.
  case (string_dec l1 l2); intuition.
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
162
163
  Qed.

164
165
166
167
168
169
170
171
172
173
  (* 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
174
    end.
175
176
177
178

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

  Fixpoint subtype_dec A B : {A <: B} + {~ A <: B}.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
179
  Proof.
180
181
182
183
184
185
186
    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
187
188
  Qed.

189
  Lemma subtype_empty A : Empty_pretype <: A -> A = Empty_pretype.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
190
  Proof.
191
192
193
194
    destruct A.
    - trivial.
    - simpl.
      case (in_dom_dec s nil); contradiction.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
195
196
  Qed.

197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
  Lemma subtype_cons_weaken A B l C :
    A <: B ->
         l  predomain A ->
         Cons_pretype l C A <: B.
  Proof.
    rewrite Not_not_in_dom.
    induction B.
    - intuition.
    - simpl.
      case (string_dec s l); intro Hsl;
      case (subtype_dec A B2);
      case (in_dom_dec s (predomain A));
      case (pretype_dec B1 (preassoc A s));
      case (pretype_dec B1 C);
      intuition.
      destruct Hsl.
      intuition.
  Qed.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
215

216
  Section subtype_reflexivity.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
217

218
219
220
221
222
223
224
225
226
    (* 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
227

228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
    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.

    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.

    Fixpoint well_formed_irrel A (H1 H2 : well_formed_type A) {struct A} : H1 = H2.
    Proof.
      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.

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

    Lemma wf_decide_spec A : well_formed_type A <-> wf_decide A = true.
    Proof.
      unfold wf_decide.
      case (well_formed_dec); intuition; discriminate.
    Qed.

    Lemma wf_decide_true A : wf_decide A = true -> well_formed_type A.
    Proof.
      rewrite wf_decide_spec.
      trivial.
    Qed.

    Theorem subtype_refl_eq B : forall A, A = B -> well_formed_type A -> A <: B.
    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.
        refine (subtype_cons_weaken _ _ _ _ _ _);
          [ refine (IH2 B2 eq_refl _) | ];
          intuition.
    Defined.

    Definition subtype_refl A : well_formed_type A -> A <: A
      := subtype_refl_eq A A eq_refl.

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

    Theorem well_formed_preassoc A l : well_formed_type A -> well_formed_type (preassoc A l).
    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
316

317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
    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. *)

  Lemma predomain_subtype A B l : A <: B -> l  predomain B -> l  predomain A.
  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.
      destruct e; intuition.
  Qed.

  Lemma preassoc_subtype A B l : A <: B -> l  predomain B -> preassoc A l = preassoc B l.
  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 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.

  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).
    apply (sigT_eq _ _ _ _ _ _ H).
    apply well_formed_irrel.
  Defined.

  Theorem subtype_trans A B C : A <: B -> B <: C -> A <: C.
  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.
                rewrite (preassoc_subtype A B s HAB sdB).
                assumption.
            + contradiction.
          }
        * intros n e HAB _.
          rewrite Not_not_in_dom in n.
          apply n.
          apply (predomain_subtype A B s HAB).
          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.
Definition insert (lA : string * type) (A2 : type) : type.
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.

(* Notations for object pretypes:
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
420
421
422
423
   [ "l₁" : A ; "l₂" : A ;  ; "lₙ" : A ]
 *)
Notation "l : A" := (l%string, A) (at level 50) : type_field_scope.
Notation "[ x1 ; .. ; xn ]" :=
424
425
  (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
426
427
428

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

432
   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
433
    - in each ς binder
434
    - to pretype each t
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
435
436
437
    - to list the labels

   Since we cannot construct an object without breaking the invariant, we define
438
   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
439
440
441

   *)

442
  (* We have to axiomatize the pretype of methods because
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
443
444
445
446
447
448
   Method A B := Obj A -> Obj B has a negative occurence of Obj which blocks
   the recursive definition
   *)

  Parameter Method : type -> type -> Type.

449
450
451
  Inductive Preobject (A : type) (f : string -> type) : list string -> Type :=
  | poempty : Preobject A f nil
  | pocons : forall d (l : string),
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
452
453
454
455
               Method A (f l) ->
               Preobject A f d ->
               Preobject A f (cons l d).

456
  Definition Obj (A : type) := Preobject A (assoc A) (domain A).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
457

458
459
  (* 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
460

461
462
463
464
465
466
467
  Definition Obj_to_expr A : Obj A -> Expr A.
  Proof.
    exists A.
    split.
    - assumption.
    - apply subtype_refl_wf.
  Defined.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
468
469

  (* End of the axiomatisation of methods: Method A B is equivalent to Obj A -> Obj B. *)
470
471
  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.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
472
473
474
475
  Axiom beta : forall A B f a, Eval_meth A B (Make_meth A B f) a = f a.

End objects.

476
477
Hint Rewrite beta : objects.

Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
478
479
480
481
482
483
Delimit Scope object_scope with obj.
Delimit Scope method_scope with meth.

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

484
Infix "⊙" := assoc (at level 50).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
485
Notation "l = 'ς' ( x !: A ) m" :=
486
487
488
  (existT (fun l2 => (prod (l2  domain A) (Method A%ty (A%ty  l2))))
          l%string
          (I, (Make_meth A%ty (A%ty  l) (fun x => m%obj))))
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
489
490
    (at level 50) : method_scope.

491
Notation "o ↑ A" := (Obj_to_expr A o) (at level 100).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
492
493
494

Section semantics.
  (* Selection and update go inside objects so they have to be defined on preobjects first. *)
495
  Definition coerce B C : B <: C -> Expr B -> Expr C.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
496
  Proof.
497
498
499
500
501
502
    intros HBC (A, (a, st)).
    exists A.
    split.
    - exact a.
    - apply (subtype_trans <<A>> <<B>> <<C>>); assumption.
  Qed.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
503

504
505
  Definition empty_object : Obj Empty_type := poempty Empty_type (assoc Empty_type).
  Definition empty_expression : Expr Empty_type := Obj_to_expr Empty_type empty_object.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
506
507

  Fixpoint preselect l A f d (po : Preobject A f d) :
508
    l  d -> Method A (f l).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
509
  Proof.
510
    destruct po as [ | d l2 m tail ].
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
511
    - intro H.
512
      destruct H.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
513
514
515
516
517
518
519
520
521
522
    - simpl.
      case (string_dec l l2).
      + intros e _.
        destruct e.
        assumption.
      + intro.
        apply preselect.
        assumption.
  Defined.

523
524
525
526
527
528
529
530
531
532
  Definition select l A (e : Expr A) (H : l  (domain A)) : Expr (assoc A l).
    destruct e as (A', (a', st)).
    rewrite <- (preassoc_subtype_wf A' A l st H).
    exact (Eval_meth _ _ (preselect l A'
                                    (assoc A')
                                    (domain A')
                                    a'
                                    (predomain_subtype <<A'>> <<A>> l st H))
                     (Obj_to_expr _ a')).
  Defined.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
533

534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
  Fixpoint preupdate l A f d (po : Preobject A f d) :
    Method A (f l) -> l  d -> Preobject A f d.
  Proof.
    destruct po as [ | d l2 m2 tail ].
    - intros _ H.
      destruct H.
    - intros m H.
      case (string_dec l l2).
      + intro e.
        destruct e.
        exact (pocons _ _ _ _ m tail).
      + intro n.
        refine (pocons _ _ _ _ m2 (preupdate l _ _ _ tail m _)).
        apply (in_cons_diff l l2); assumption.
  Defined.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
549

550
551
  Definition obj_update l A (a : Obj A) m H : Obj A :=
    preupdate l A (assoc A) (domain A) a m H.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
552

553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
  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.
    - apply (obj_update l A' a').
      apply Make_meth.
      intro self.
      rewrite (preassoc_subtype_wf A' A l st H).
      apply (Eval_meth A _ m).
      apply (coerce A' A st).
      exact self.
      exact (predomain_subtype <<A'>> <<A>> l st H).
    - assumption.
  Defined.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
568

569
570
571
  (* Specification of select: *)
  Theorem presel_cons_eq l1 l2 A f d m1 po :
    forall H, forall e : l2 = l1, preselect l2 A f (cons l1 d) (pocons A f d l1 m1 po) H = rew <- (f_equal f e) in m1.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
572
573
  Proof.
    simpl.
574
575
576
577
578
579
580
    case (string_dec l2 l1).
    + intros e _ e'.
      assert (He : e = e') by apply String_UIP.UIP.
      destruct He.
      destruct e.
      reflexivity.
    + intros; intuition.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
581
582
  Qed.

583
584
585
  Definition presel_cons l A f d m1 po H : preselect l A f (cons l d) (pocons A f d l m1 po) H = m1
    := presel_cons_eq l l A f d m1 po H eq_refl.

Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
586
587
588
589
590
591
  Theorem presel_cons_diff l l2 A f d m1 po H :
    l <> l2 ->
    preselect l A f (cons l2 d) (pocons A f d l2 m1 po) (in_cons_tl l l2 d H)
    = preselect l A f d po H.
  Proof.
    intro diff.
592
    generalize (in_cons_tl l l2 d H).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
593
    simpl.
594
595
596
597
    case (string_dec l l2); intros eqdiff H2.
    - destruct (diff eqdiff).
    - apply f_equal.
      apply in_dom_irrel.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
598
599
600
601
  Qed.

  (* Specification of update: *)

602
  Theorem preup_irrel A f d l p m H1 H2 : preupdate l A f d p m H1 = preupdate l A f d p m H2.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
603
  Proof.
604
605
    apply f_equal.
    apply in_dom_irrel.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
606
607
  Qed.

608
609
610
  Theorem preup_cons_eq A f d l1 l2 po m1 m2 :
    forall e : l2 = l1, forall H,
      preupdate l2 A f (cons l1 d) (pocons A f d l1 m1 po) m2 H = pocons A f d l1 (rew (f_equal f e) in m2) po.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
611
  Proof.
612
613
614
615
616
617
618
619
620
    intros e H.
    simpl.
    case (string_dec l2 l1).
    - intro el.
      assert (He : e = el) by apply String_UIP.UIP.
      destruct He.
      destruct e.
      reflexivity.
    - intro n; destruct (n e).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
621
622
  Qed.

623
624
625
626
  Definition preup_cons_eq2 A f d l po m1 m2 : forall H, preupdate l A f (cons l d) (pocons A f d l m1 po) m2 H = pocons A f d l m2 po
    := preup_cons_eq A f d l l po m1 m2 eq_refl.

  Theorem preup_cons_diff A f d l l2 m1 m2 po H1 H2:
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
627
    l <> l2 ->
628
629
    preupdate l A f (cons l2 d) (pocons A f d l2 m1 po) m2 H1
    = pocons A f d l2 m1 (preupdate l A f d po m2 H2).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
630
  Proof.
631
    simpl.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
632
633
634
635
636
    intro diff.
    case (string_dec l l2).
    - intro eq.
      destruct (diff eq).
    - intro diff2.
637
638
639
      apply f_equal.
      apply f_equal.
      apply in_dom_irrel.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
640
641
642
  Qed.
End semantics.

643
644
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 A%ty (A%ty  l) (fun x => m)) I) (at level 50).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
645

646
647
648
(* 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
649
Section init.
650
651
652
653
654

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

  Fixpoint preinit A d :
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
655
    (forall l, l  d -> l  domain A) ->
656
657
658
659
660
661
662
663
664
665
666
667
668
669
    Preobject A (assoc A) d :=
    match d return
          (forall l, l  d -> l  domain A) -> Preobject A (assoc A) d
    with
      | nil => fun _ => poempty A (assoc A)
      | cons l d =>
        fun H =>
          pocons A (assoc A) d l
                 (loop_method A l (H l (in_cons_hd l d)))
                 (preinit A d (fun l1 H1 =>
                                    H l1 (in_cons_tl l1 l d H1)))
    end.

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

671
  Definition init A : Expr A := Obj_to_expr A (obj_init A).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
672
673
End init.

674
675
676
677
678
679
680
681
(* Definition of objects without respecting the order of labels given by the pretype. *)
Definition pocons_3 A (lm : sigT (fun l2 =>
                                    ((l2  domain A) * Method A (assoc A l2))%type))
           (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
682
683
684

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

685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
Notation "[[ l = 'ς' ( x !: A ) m ; p ]]" := (pocons A _ _ l (Make_meth A _ (fun x => m)) p) (at level 50) : object_scope.

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



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
754
755
Section examples.
  (* Encodding of booleans *)
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
  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.

  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
810
811
812
813

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

814
815
  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
816

817
818
  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
819

820
821
822
823
  (* 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
824
825
End examples.

826
827
828
829
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).