Add more helpers

althelf/rules.smt3

@@ -150,7 +150,15 @@
   :conclusion CL
 )
 
-; TODO: side condition
+;TODO
+(program check_bind ((ctx @Context) (xs @VarList) (ys @VarList))
+  (@Context @VarList @VarList) Bool
+  (
+   ((check_bind ctx xs ys) true)
+  )
+)
+
+;TRUST
 (declare-rule bind ((ctx @Context) (xs @VarList) (ys @VarList) (T Type) (phi T) (phi' T))
   :assumption ctx
   :premises ((cl (= phi phi')))
@@ -159,7 +167,15 @@
   :conclusion (cl (= (forall xs phi) (forall ys phi')))
 )
 
-; TODO: side condition
+;TODO
+(program check_sko_ex ((ctx @Context) (xs @VarList))
+  (@Context @VarList) Bool
+  (
+   ((check_sko_ex ctx xs) true)
+  )
+)
+
+;TRUST
 (declare-rule sko_ex ((ctx @Context) (xs @VarList) (phi Bool) (psi Bool))
   :assumption ctx
   :premises ((cl (= phi psi)))
@@ -168,7 +184,15 @@
   :conclusion (cl (= (exists xs phi) psi))
 )
 
-; TODO: side condition
+;TODO
+(program check_sko_forall ((ctx @Context) (xs @VarList))
+  (@Context @VarList) Bool
+  (
+   ((check_sko_forall ctx xs) true)
+  )
+)
+
+;TRUST
 (declare-rule sko_forall ((ctx @Context) (xs @VarList) (phi Bool) (psi Bool))
   :assumption ctx
   :premises ((cl (= phi psi)))
@@ -177,23 +201,30 @@
   :conclusion (cl (= (forall xs phi) psi))
 )
 
-; TODO: side condition
-(declare-rule forall_inst ((ctx Bool) (xs @VarList) (phi Bool) (psi Bool))
-  :assumption ctx
-  :premises ((cl (= phi psi)))
-  :args ((cl (= (forall xs phi) psi)))
-  :requires ((check_sko_forall ctx xs) true)
-  :conclusion (cl (= (forall xs phi) psi))
+;TODO
+(program check_forall_inst ((xs @VarList) (P Bool) (P' Bool))
+  (@VarList Bool Bool) Bool
+  (
+   ((check_forall_inst xs P P') true)
+  )
 )
 
-; TODO: side condition
+;TRUST
 (declare-rule forall_inst ((P Bool) (P' Bool) (xs @VarList))
   :args ((cl (or (not (forall xs P) P'))))
   :requires ((check_forall_inst xs P P') true)
   :conclusion (cl (or (not (forall xs P) P')))
 )
 
-; TODO: side condition
+;TODO
+(program check_refl ((ctx @Context) (T Type) (t1 T) (t2 T))
+  (@Context T T) Bool
+  (
+   ((check_refl ctx t1 t2) true)
+  )
+)
+
+;TRUST
 (declare-rule refl ((ctx @Context) (T Type) (t1 T) (t2 T))
   :premises (ctx)
   :args ((cl (= t1 t2)))
@@ -201,19 +232,27 @@
   :conclusion (cl (= t1 t2))
 )
 
-; TODO: implement mkTrans
+;TODO: implement mkTrans
 (declare-rule trans ((Eqs Bool))
   :premise-list Eqs and
   :args (((cl (mkTrans Eqs))))
   :conclusion (cl (mkTrans Eqs))
 )
 
-; TODO: side condition
-(declare-rule cong ((Eqs Bool) (CEq))
+;TODO
+(program check_cong ((Eqs Bool) (CEq Bool))
+  (Bool Bool) Bool
+  (
+   ((check_cong Eqs CEq) true)
+  )
+)
+
+;TRUST
+(declare-rule cong ((Eqs Bool) (CEq Bool))
   :premise-list Eqs and
-  :args ((cl (CEq)))
+  :args ((cl CEq)) ; CEq is an equality
   :requires ((check_cong Eqs CEq) true)
-  :conclusion (cl (CEq))
+  :conclusion (cl CEq)
 )
 
 (declare-rule eq_reflexive ((T Type) (t T))
@@ -221,32 +260,76 @@
   :conclusion (cl (= t t))
 )
 
-; TODO: side conditions
+;TODO
+(program check_eq_transitive ((CL Bool))
+  (Bool) Bool
+  (
+   ((check_eq_transitive CL) true)
+  )
+)
+
+;TRUST
 (declare-rule eq_transitive ((CL Bool))
   :args ((CL))
   :requires ((check_eq_transitive CL) true)
   :conclusion CL
 )
 
-; TODO: side conditions
+;TODO
+(program check_eq_congruent ((CL Bool))
+  (Bool) Bool
+  (
+   ((check_eq_congruent CL) true)
+  )
+)
+
+;TRUST
 (declare-rule eq_congruent ((CL Bool))
   :args ((CL))
   :requires ((check_eq_congruent CL) true)
   :conclusion CL
 )
 
-; TODO: side conditions
+;TODO
+(program check_eq_congruent_pred ((CL Bool))
+  (Bool) Bool
+  (
+   ((check_eq_congruent_pred CL) true)
+  )
+)
+
+;TRUST
 (declare-rule eq_congruent_pred ((CL Bool))
   :args ((CL))
   :requires ((check_eq_congruent_pred CL) true)
   :conclusion CL
 )
 
+;TODO
+(program check_qnt_cnf ((phi Bool) (phi' Bool) (xs @VarList) (xs' @VarList))
+  (@VarList Bool @VarList Bool) Bool
+  (
+   ((check_qnt_cnf xs phi xs' phi') true)
+  )
+)
+
+;TRUST
 (declare-rule qnt_cnf ((phi Bool) (phi' Bool) (xs @VarList) (xs' @VarList))
   :args ((cl (or (not (forall xs phi)) (forall xs' phi'))))
+  :requires ((check_qnt_cnf xs phi xs' phi') true)
   :conclusion (cl (or (not (forall xs phi)) (forall xs' phi')))
 )
 
+;TODO
+(program contains ((inList Bool) (phi Bool))
+  (Bool Bool) Bool
+  (
+   ((contains inList phi) true)
+  )
+)
+
+; TODO: this overloads 'and'
+;TRUST
 (declare-rule and ((C Bool) (CN Bool :list) (phi Bool))
   :premises ((cl (and C CN)))
   :args ((cl phi))
@@ -254,6 +337,7 @@
   :conclusion (cl phi)
 )
 
+;TRUST
 (declare-rule not_or ((C Bool) (CN Bool :list) (phi Bool))
   :premises ((cl (not (or C CN))))
   :args ((cl (not phi)))
@@ -261,6 +345,16 @@
   :conclusion (cl (not phi))
 )
 
+;TODO
+(program check_or ((ors Bool) (clause Bool))
+  (Bool Bool) Bool
+  (
+   ((check_or ors clause) true)
+  )
+)
+
+; TODO: this overloads 'or'
+;TRUST
 (declare-rule or ((C Bool) (CN Bool :list) (C' Bool) (CN' Bool :list))
   :premises ((cl (or C CN)))
   :args ((cl C' CN'))