1
2
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
37
38
39
40
41
42
43
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
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
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
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
|
; depends: core_defs.plf util_defs.plf
; This file defines a library of methods for reasoning about n-ary functions.
; Notice that since LFSC does not have support for n-ary function symbols, we
; represent n-ary function applications in a null-terminated, Curried form.
; In particular, the term `(or A B C)` is represented in LFSC as:
; `(apply (apply f_or A) (apply (apply f_or B) (apply (apply f_or C) false)))`
; i.e. using the macro definitions in core_defs:
; `(or A (or B (or C false)))`
; where notice that `false` is the null-terminator for `or`. Many operators
; are treated in this way, including Boolean connectives `and` and `or`,
; arithmetic plus and multiplication, string concatenation, and so on.
; We call the term like the one above "an f_or-application in n-ary form".
; When applicable, we simply write "f-application" to refer to a term that is
; in n-ary form. We call A, B, C the "elements" of the f-application above.
; We say that an f-application is a "singleton" if it consists of a single
; element, e.g. `(or A false)`.
;
; This file defines a set of side conditions that are useful in defining
; theory-specific proof rules involving n-ary functions and are agnostic to the
; function in question. When applicable, the side conditions take the n-ary
; function `f` as an argument, or its null terminator `null`.
; Head and tail for n-ary operators with null terminators. These methods
; fail if t is not an f-application.
(program nary_head ((f term) (t term)) term
(match t ((apply t1 t2) (getarg f t1))))
(program nary_tail ((f term) (t term)) term
(match t ((apply t1 t2) (let t12 (getarg f t1) t2))))
; Remove the first occurrence of term l from t. This side condition fails if t
; is not an f-application, or if t does not contain l.
(program nary_rm_first ((f term) (t term) (l term)) term
(match t
((apply t1 t2) ; otherwise at end, l not found
(let t12 (getarg f t1)
(ifequal t12 l t2 (apply t1 (nary_rm_first f t2 l))))))
; otherwise not an f-app in n-ary form
)
; Same as `nary_rm_first`, but also checks whether t is l itself and returns null if so,
; where null is a null terminator.
(program nary_rm_first_or_self ((f term) (t term) (l term) (null term)) term
(ifequal t l null (nary_rm_first f t l))
)
; Does t contain l? This side condition may fail if t is not an f-application.
(program nary_ctn ((f term) (t term) (l term)) flag
(match t
((apply t1 t2)
(let t12 (getarg f t1)
(ifequal t12 l tt (nary_ctn f t2 l))))
; otherwise not an f-app in n-ary form
(default ff))
)
; Same as `nary_ctn`, but also checks if t is l, returning true if so.
(program nary_ctn_or_self ((f term) (t term) (l term)) flag
(ifequal t l tt (nary_ctn f t l))
)
; Returns true if t is a subset of s, when these terms were interpreted as sets.
; This side condition may fail if t or s is not an f-application.
(program nary_is_subset ((f term) (t term) (s term)) flag
(match t
((apply t1 t2)
(let t12 (getarg f t1)
(ifequal (nary_ctn_or_self f s t12) tt (nary_is_subset f t2 s) ff)))
; otherwise not in n-ary form
(default tt))
)
; Concatenates terms t1 and t2 that are f-applications in n-ary form.
(program nary_concat ((f term) (t1 term) (t2 term) (null term)) term
(match t1
((apply t11 t12)
(let t112 (getarg f t11)
(apply t11 (nary_concat f t12 t2 null))))
(default t2)) ; any non-application term is interpreted as null
)
; Insert element elem at the beginning of the f-application t.
(program nary_insert ((f term) (elem term) (t term) (null term)) term
(ifequal elem null t (apply (apply f elem) t)))
; Dual to `nary_insert`. Returns a term pair ( elem, t' ) where elem is the
; head of t, and t' is the tail of t.
(program nary_decompose ((f term) (t term) (null term)) termPair
(match t
((apply t1 t2)
(match t1
((apply t11 t12) (ifequal t11 f (pair t12 t2) (pair null t)))
(default (pair null t))))
(default (pair null t)))
)
; N-ary elimination. This replaces a singleton f-application with its element.
; For example, this replaces e.g. (or t false) with t.
(program nary_elim ((f term) (t term) (null term)) term
(match t
((apply t1 t2)
; if null terminated, then we return the head, otherwise not in n-ary form
(ifequal t2 null (getarg f t1) t))
(default (ifequal t null t (fail term))))
)
; N-ary introduction, which is the inverse of nary_elim. This turns a term t into
; a (singleton) f-application if it is not already in n-ary form. For example,
; this replaces t with (or t false) if t is not already in n-ary form.
(program nary_intro ((f term) (t term) (null term)) term
(match t
((apply t1 t2)
(match t1
((apply t11 t12) (ifequal t11 f t (apply (apply f t) null)))
(default (apply (apply f t) null))))
(default (ifequal t null t (apply (apply f t) null))))
)
; Extract the n^th element of f-application t. This side condition fails if
; t is not an f-application, or contains fewer than n elements.
(program nary_extract ((f term) (t term) (n mpz)) term
(match t
((apply t1 t2)
(mp_ifzero n
(getarg f t1)
(nary_extract f t2 (mp_add n (mp_neg 1))))))
)
; Helper for dropping duplicates from an f-application t. Elements occur in
; the returned f-application in the order they first appear in t.
; This side condition takes an accumulator tacc which tracks which terms it is
; adding to the return value. We require an explicit accumulator to ensure
; propering ordering for cases like (or A B B A), where (or A B) should be
; returned instead of (or B A).
; This method fails if t is not an f-application.
(program nary_drop_dups_rec ((f term) (t term) (tacc term)) term
(match t
((apply t1 t2)
(let t12 (getarg f t1)
(let c (nary_ctn f tacc t12)
(let t2d (nary_drop_dups_rec f t2 (ifequal c tt tacc (apply t1 tacc)))
(ifequal c tt t2d (apply t1 t2d))))))
(default t))
)
; Drop all duplicates in an f-application t using the helper method
; `nary_drop_dups_rec`.
(program nary_drop_dups ((f term) (t term) (null term)) term
(nary_elim f (nary_drop_dups_rec f t null) null)
)
; Truncate, which returns the f-application in which the subterm c has been
; replaced by the null terminator, where c is an f-application that is a
; suffix of t. For example, (or t1 ... tn c) ---> (or t1 ... tn false).
; This side condition fails if c is not a suffix of f-application t.
(program nary_truncate ((f term) (t term) (c term) (null term)) term
(ifequal t c null
(match t
((apply t1 t2)
(let t12 (getarg f t1)
(apply t1 (nary_truncate f t2 c null))))))
)
; Helper for reverse, which takes an accumulator of terms we have added in
; reverse order to the value we will return. This side condition fails if
; t is not an f-application.
(program nary_reverse_rec ((f term) (t term) (acc term) (null term)) term
(match t
((apply t1 t2)
(let t12 (getarg f t1)
(nary_reverse_rec f t2 (apply t1 acc) null)))
(default (ifequal t null acc (fail term))))
)
; Reverse the elements in f-application t using the helper method
; `nary_reverse_rec`.
(program nary_reverse ((f term) (t term) (null term)) term
(nary_reverse_rec f t null null)
)
|
