Merge branch 'master' into fix1649fix1649

1 files changed, 179 insertions, 0 deletions

diff --git a/proofs/lfsc/signatures/nary_programs.plf b/proofs/lfsc/signatures/nary_programs.plf
new file mode 100644
index 000000000..f04e6ba40
--- /dev/null
+++ b/proofs/lfsc/signatures/nary_programs.plf
@@ -0,0 +1,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)
+)