Use a consistent documentation format for ALF quantifiers signature (c…

…vc5#10856)

Towards a standard documentation format for the ALF signature.

Also adds a missing check for alpha-equiv.

---------

Co-authored-by: Hans-Jörg <[email protected]>

proofs/alf/cvc5/programs/Quantifiers.smt3

@@ -1,21 +1,64 @@
 (include "../theories/Builtin.smt3")
 (include "../theories/Quantifiers.smt3")
 
-(program substitute
+; program: $substitute
+; args:
+; - arg1 S: The domain of the substitution.
+; - arg2 S: The range of the substitution.
+; - arg3 U: The term to process.
+; return: the result of replacing all occurrences of arg1 with arg2 in arg3.
+(program $substitute
   ((T Type) (U Type) (S Type) (x S) (y S) (f (-> T U)) (a T) (z U) (w T))
   (S S U) U
   (
-  ((substitute x y x)             y)
-  ((substitute x y (f a))         (_ (substitute x y f) (substitute x y a)))
-  ((substitute x y z)             z)
+  (($substitute x y x)             y)
+  (($substitute x y (f a))         (_ ($substitute x y f) ($substitute x y a)))
+  (($substitute x y z)             z)
   )
 )
 
-(program substitute_list ((T Type) (U Type) (F U) (x T) (xs @List :list) (t T) (ts @List :list))
+; program: $substitute_list
+; args:
+; - arg1 @List: The list of domains of the substitution.
+; - arg2 @List: The list of ranges of the substitution.
+; - arg3 U: The term to process.
+; return: >
+;   The result of applying the substitutions specified by arg1
+;   and arg2 in order to arg3. In particular, the first element in the lists arg1
+;   and arg2 are processed first.
+(program $substitute_list ((T Type) (U Type) (F U) (x T) (xs @List :list) (t T) (ts @List :list))
   (@List @List U) U
   (
-    ((substitute_list (@list x xs) (@list t ts) F) (substitute_list xs ts (substitute x t F)))
-    ((substitute_list @list.nil @list.nil F)       F)
+    (($substitute_list (@list x xs) (@list t ts) F) ($substitute_list xs ts ($substitute x t F)))
+    (($substitute_list @list.nil @list.nil F)       F)
+  )
+)
+
+; program: $contains_subterm
+; args:
+; - arg1 S: The term to process.
+; - arg2 U: The term to find.
+; return: The result is true if arg2 is a subterm of arg1.
+(program $contains_subterm
+  ((T Type) (U Type) (S Type) (x U) (y S) (f (-> T S)) (a T))
+  (S U) Bool
+  (
+  (($contains_subterm x x)      true)
+  (($contains_subterm (f a) x)  (alf.ite ($contains_subterm f x) true ($contains_subterm a x)))
+  (($contains_subterm x y)      false)
+  )
+)
+
+; program: $contains_subterm_list
+; args:
+; - arg1 T: The term to process.
+; - arg2 @List: The list of terms to find.
+; return: true if any term in arg2 is a subterm of arg1.
+(program $contains_subterm_list ((T Type) (U Type) (t T) (x U) (xs @List :list))
+  (T @List) Bool
+  (
+    (($contains_subterm_list t (@list x xs)) (alf.ite ($contains_subterm t x) true ($contains_subterm_list t xs)))
+    (($contains_subterm_list t @list.nil)    false)
   )
 )
 

proofs/alf/cvc5/rules/Quantifiers.smt3

@@ -2,42 +2,77 @@
 (include "../theories/Quantifiers.smt3")
 
 
+; rule: instantiate
+; implements: ProofRule::INSTANTIATE.
+; premises:
+; - Q Bool: The quantified formula to instantiate.
+; args:
+; - ts @List: The list of terms to instantiate with.
+; conclusion: The result of substituting free occurrences of xs in F with ts.
 (declare-rule instantiate ((F Bool) (xs @List) (ts @List))
   :premises ((forall xs F))
   :args (ts)
-  :conclusion (substitute_list xs ts F))
+  :conclusion ($substitute_list xs ts F))
 
-; returns the list of skolems for F
-(program mk_skolems ((x @List) (xs @List :list) (F Bool))
+; program: $mk_skolems
+; args:
+; - arg1 @List: The bound variable list to process.
+; - arg2 Bool: The body of the quantified formula. This impacts the definition of the introduced skolems.
+; return: >
+;   The list of skolem variables for the quantified formula whose bound variable list
+;   is arg1 and whose body is arg2.
+(program $mk_skolems ((x @List) (xs @List :list) (F Bool))
   (@List Bool) @List
   (
-    ((mk_skolems (@list x xs) F) (alf.cons @list (@quantifiers_skolemize F x) (mk_skolems xs F)))
-    ((mk_skolems @list.nil F)    @list.nil)
+    (($mk_skolems (@list x xs) F) (alf.cons @list (@quantifiers_skolemize F x) ($mk_skolems xs F)))
+    (($mk_skolems @list.nil F)    @list.nil)
   )
 )
 
+; rule: skolemize
+; implements: ProofRule::SKOLEMIZE.
+; premises:
+; - Q Bool: The quantified formula to skolemize. This is either an existential or a negated universal.
+; conclusion: >
+;   The skolemized body of Q, where its variables are replaced by skolems
+;   introduced via $mk_skolems,
 (declare-rule skolemize ((F Bool))
   :premises (F)
   :conclusion
     (alf.match ((T Type) (x @List) (G Bool))
         F
         (
-          ((exists x G)       (substitute_list x (mk_skolems x F) G))
-          ((not (forall x G)) (substitute_list x (mk_skolems x (exists x (not G))) (not G)))
+          ((exists x G)       ($substitute_list x ($mk_skolems x F) G))
+          ((not (forall x G)) ($substitute_list x ($mk_skolems x (exists x (not G))) (not G)))
         ))
 )
 
+; rule: skolem_intro
+; implements: ProofRule::SKOLEM_INTRO.
+; args:
+; - t T: The purification skolem.
+; conclusion: >
+;   An equality equating t to its original form. This indicates that
+;   the purification skolem for any term x can be assumed to be equal to x.
 (declare-rule skolem_intro ((T Type) (x T))
   :args ((@purify x))
   :conclusion (= (@purify x) x)
 )
 
-; B is the formula to apply to
-; vs is a list of variables to substitution for the variable list ts
-; Note we don't currently check whether this is valid renaming.
+; rule: alpha_equiv
+; implements: ProofRule::ALPHA_EQUIV.
+; args:
+; - B Bool: The formula to apply to alpha equivalence to.
+; - vs @List: The list of variables to substitute from.
+; - ts @List: The list of (renamed) variables to substitute into.
+; requires: B does not contain any occurence of the range variables ts.
+; conclusion: >
+;   The result of applying the substitution specified by vs and ts to
+;   B. The substitution is valid renaming due to the requirement check.
 (declare-rule alpha_equiv ((B Bool) (vs @List) (ts @List))
   :args (B vs ts)
-  :conclusion (= B (substitute_list vs ts B))
+  :requires ((($contains_subterm_list B ts) false))
+  :conclusion (= B ($substitute_list vs ts B))
 )
 
 ; rule: beta_reduce implements ProofRewriteRule::BETA_REDUCE