dk_domain.dk 3.74 KB
Newer Older
1
#NAME dk_domain.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
2

Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
(;

Copyright Raphaël Cauderlier (2014)

<raphael.cauderlier@inria.fr>

This software is a computer program whose purpose is to translate object-oriented program written in the simply-typed ς-calculus from Abadi and Cardelli to Dedukti and Coq.

This software is governed by the CeCILL-B license under French law and
abiding by the rules of distribution of free software.  You can use,
modify and/ or redistribute the software under the terms of the CeCILL-B
license as circulated by CEA, CNRS and INRIA at the following URL
"http://www.cecill.info".

As a counterpart to the access to the source code and rights to copy,
modify and redistribute granted by the license, users are provided
only with a limited warranty and the software's author, the holder of
the economic rights, and the successive licensors have only limited
liability.

In this respect, the user's attention is drawn to the risks associated
with loading, using, modifying and/or developing or reproducing the
software by the user in light of its specific status of free software,
that may mean that it is complicated to manipulate, and that also
therefore means that it is reserved for developers and experienced
professionals having in-depth computer knowledge. Users are therefore
encouraged to load and test the software's suitability as regards
their requirements in conditions enabling the security of their
systems and/or data to be ensured and, more generally, to use and
operate it in the same conditions as regards security.

The fact that you are presently reading this means that you have had
knowledge of the CeCILL-B license and that you accept its terms.

37
 ;)
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
38

39
40
41
def uT := pts.uT.
def eT := pts.eT.
def Arrow := pts.Arrow.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
42

43
44
45
46
47
48
def Bool := dk_bool.Bool.
def true : Bool := dk_bool.true.
def false : Bool := dk_bool.false.
def not : Bool -> Bool := dk_bool.not.
def or : Bool -> Bool -> Bool
       := dk_bool.or.
49

50
51
52
53
def Prop := dk_logic.Prop.
def proof := dk_logic.eP.
def Istrue := dk_logic.Istrue.
def tt : Istrue true := dk_logic.I.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
54

55
def bool_or_intro2 := dk_logic.bool_or_intro2.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
56
57

(; Labels ;)
58
59
def Label := dk_string.String.
def label_eq : Label -> Label -> Bool := dk_string.equal.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
60
(; Correctness of label_eq ;)
61
def label_eq_rect := dk_string.eq_rect.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
62
63

(; Dependant if with equality ;)
64
def if_label_eq := dk_string.if_eq.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
65
66
67
68
69


Domain : Type.
nil : Domain.
cons : Label -> Domain -> Domain.
70
71
72
73
74

(; Membership as predicate. ;)

position : Label -> Domain -> uT.
Position : Label -> Domain -> Type.
75
[l,D] pts.eT (position l D) --> Position l D.
76
77
78
79
80
81
82
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).

83
84
def Subset : Domain -> Domain -> Type.
[A,B]
85
    Subset A B
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
86
      -->
87
88
89
    l : Label ->
    Position l A ->
    Position l B.
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
90

91
(; Position and membership ;)
92
93
94
def mem : l : Label -> d : Domain -> Bool.
[ ] mem _ nil --> false
[l1,l2,d]
95
96
97
98
    mem l1 (cons l2 d)
      -->
    or (label_eq l1 l2)
       (mem l1 d).
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
99

100
101
102
103
104
105
106
def mem_diff : l1 : Label ->
               l2 : Label ->
               D : Domain ->
               Istrue (not (label_eq l1 l2)) ->
               Istrue (mem l1 (cons l2 D)) ->
               Istrue (mem l1 D).
[l1,l2,D,H1,H12]
107
108
109
110
    mem_diff l1 l2 D H1 H12
      -->
    dk_logic.bool_or_elim1 (label_eq l1 l2) (mem l1 D) H1 H12.

111
112
def mem_pos : l : Label -> d : Domain -> Istrue (mem l d) -> Position l d.
[l1,l2,d,H]
113
    mem_pos l1 (cons l2 d) H
Raphaël Cauderlier's avatar
Raphaël Cauderlier committed
114
      -->
115
116
117
118
119
120
121
    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
122
                          (mem_pos l1 d (mem_diff l1 l2 d (dk_string.diff_sym l2 l1 Hdiff) H))).