dk_domain.dk 2.24 KB
Newer Older
1
#NAME dk_domain.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
2
3
4
5
6
7
8
9

uT := pts.uT.
eT := pts.eT.
Arrow := pts.Arrow.

Bool := dk_bool.Bool.
true : Bool := dk_bool.true.
false : Bool := dk_bool.false.
10
not : Bool -> Bool := dk_bool.not.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
11
12
or : Bool -> Bool -> Bool
   := dk_bool.or.
13
14
15

Prop := dk_logic.Prop.
proof := dk_logic.eP.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
Istrue := dk_logic.Istrue.
tt : Istrue true := dk_logic.I.

bool_or_intro2 := dk_logic.bool_or_intro2.

(; Labels ;)
Label := dk_string.String.
label_eq : Label -> Label -> Bool := dk_string.equal.
(; Correctness of label_eq ;)
label_eq_rect := dk_string.eq_rect.

(; Dependant if with equality ;)
if_label_eq := dk_string.if_eq.


Domain : Type.
nil : Domain.
cons : Label -> Domain -> Domain.
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50

(; Membership as predicate. ;)

position : Label -> Domain -> uT.
Position : Label -> Domain -> Type.
[ l : Label, D : Domain ] Position l D --> eT (position l D).
Position_head : l : Label -> d : Domain -> Position l (cons l d).
Position_tail : l : Label ->
                l2 : Label ->
                d : Domain ->
                Position l d ->
                Position l (cons l2 d).

Subset : Domain -> Domain -> Type.
[ A : Domain,
  B : Domain ]
    Subset A B
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
51
      -->
52
53
54
    l : Label ->
    Position l A ->
    Position l B.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
55

56
57
58
59
60
61
62
63
(; Position and membership ;)
mem : l : Label -> d : Domain -> Bool.
[ l : Label ] mem l nil --> false
[ l1 : Label, l2 : Label, d : Domain ]
    mem l1 (cons l2 d)
      -->
    or (label_eq l1 l2)
       (mem l1 d).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
64

65
mem_diff : l1 : Label ->
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
66
67
           l2 : Label ->
           D : Domain ->
68
69
70
           Istrue (not (label_eq l1 l2)) ->
           Istrue (mem l1 (cons l2 D)) ->
           Istrue (mem l1 D).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
71
72
73
[ l1 : Label,
  l2 : Label,
  D : Domain,
74
75
76
77
78
79
80
81
82
  H1 : Istrue (not (label_eq l1 l2)),
  H12 : Istrue (mem l1 (cons l2 D)) ]
    mem_diff l1 l2 D H1 H12
      -->
    dk_logic.bool_or_elim1 (label_eq l1 l2) (mem l1 D) H1 H12.

mem_pos : l : Label -> d : Domain -> Istrue (mem l d) -> Position l d.
[ l1 : Label, l2 : Label, d : Domain, H : Istrue (mem l1 (cons l2 d)) ]
    mem_pos l1 (cons l2 d) H
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
83
      -->
84
85
86
87
88
89
90
91
    dk_string.if_eq_diff
      (l : Label => position l1 (cons l d))
      l1
        l2
        (Position_head l1 d)
        (Hdiff : Istrue (not (label_eq l2 l1)) =>
         Position_tail l1 l2 d
         (mem_pos l1 d (mem_diff l1 l2 d (dk_string.diff_sym l2 l1 Hdiff) H))).