Isabelle 中的可变参数函数

Question

是否可以使用 Isabelle 证明助手定义一个涉及可变参数函数的理论？

例如，我想定义所有元数 n 的谓词的理论，这些谓词通过循环置换是不变的。 给定一个类型 T 和一个整数 n， 我想定义所有 n 的谓词的理论，例如：P A_1,... A_n P A_n A_2, ..., A_n-1。

在 Coq 中可以使用依赖类型，我想知道是否有办法使用 Isabelle 来表达这一点？

Answer 1

n-ary 函数的类似方法是：首先，我们定义正自然数的类型：

theory foo
imports Main "~~/src/HOL/Library/Cardinality" "~~/src/Tools/Adhoc_Overloading"
begin

typedef num1 = "UNIV :: unit set"
  by (rule UNIV_witness)

typedef 'n suc = "UNIV :: ('n::finite) option set"
  by (rule UNIV_witness)

instance num1 :: finite
proof
  show "finite (UNIV :: num1 set)"
    unfolding type_definition.univ[OF type_definition_num1]
    using finite by (rule finite_imageI)
qed

instance suc :: (finite) finite
proof
  show "finite (UNIV :: ('n::finite) suc set)"
    unfolding type_definition.univ[OF type_definition_suc]
    using finite by (rule finite_imageI)
qed

setup_lifting type_definition_num1

现在我们定义 n 的类型，它接受 n 类型的值 'a 并返回 'b 作为从 'n ⇒ 'a 获取函数并返回 'b 的函数类型，以及这些函数的抽象和应用：

typedef ('a,'n,'b) nary_fun = "UNIV :: (('n::finite ⇒ 'a) ⇒ 'b) set"
  by (rule UNIV_witness)

setup_lifting type_definition_suc
setup_lifting type_definition_nary_fun

lift_definition nary_fun_apply_1 :: "('a,num1,'b) nary_fun ⇒ 'a ⇒ 'b" 
  is "λf x. f (λ_. x)" .  

lift_definition nary_fun_apply_suc :: "('a,('n::finite) suc,'b) nary_fun ⇒ 'a ⇒ ('a,'n,'b) nary_fun" 
  is "λ(f::('n option ⇒ 'a) ⇒ 'b) (x::'a) (y::'n ⇒ 'a). f (case_option x y)" .  

lift_definition nary_fun_abs_1 :: "('a ⇒ 'b) ⇒ ('a,num1,'b) nary_fun" 
  is "λf x. f (x ())" .

lift_definition nary_fun_abs_suc :: "('a ⇒ ('a,'n::finite,'b) nary_fun) ⇒ ('a,'n suc,'b) nary_fun" 
  is "λf x. f (x None) (λn. x (Some n))" .

lemma nary_fun_1_beta [simp]: "nary_fun_apply_1 (nary_fun_abs_1 f) x = f x"
  by (simp add: nary_fun_abs_1_def nary_fun_apply_1_def Abs_nary_fun_inverse)

lemma nary_fun_suc_beta [simp]: "nary_fun_apply_suc (nary_fun_abs_suc f) x = f x"
  by (simp add: nary_fun_abs_suc_def nary_fun_apply_suc_def Abs_nary_fun_inverse 
                Abs_suc_inverse Rep_nary_fun_inverse)

添加一些语法糖：

consts nary_fun_apply :: "('a,('n::finite),'b) nary_fun ⇒ 'a ⇒ 'c" (infixl "$" 90)

adhoc_overloading nary_fun_apply nary_fun_apply_1 nary_fun_apply_suc

syntax
  "_nary_fun_abs" :: "pttrns ⇒ 'b ⇒ ('a,'n,'b) nary_fun"    ("χ (_). _" 10)

translations
  "χ x y. e" == "CONST nary_fun_abs_suc (λx. (χ y. e))"
  "χ x. e" == "CONST nary_fun_abs_1 (λx. e)"

syntax
  "_NumeralType" :: "num_token => type"  ("_")
  "_NumeralType1" :: type ("1")

translations
  (type) "1" == (type) "num1"

parse_translation {*
  let
    fun mk_numtype n =
      if n = 1 then Syntax.const @{type_syntax num1}
      else if n < 0 then raise TERM ("negative type numeral", [])
      else Syntax.const @{type_syntax suc} $ mk_numtype (n - 1)

    fun numeral_tr [Free (str, _)] = mk_numtype (the (Int.fromString str))
      | numeral_tr ts = raise TERM ("numeral_tr", ts);

  in [(@{syntax_const "_NumeralType"}, K numeral_tr)] end;
*}

print_translation {*
  let
    fun int_of (Const (@{type_syntax num1}, _)) = 1
      | int_of (Const (@{type_syntax suc}, _) $ t) = 1 + int_of t
      | int_of t = raise TERM ("int_of", [t]);

    fun suc_tr' [t] =
          let
            val num = string_of_int (int_of t + 1) handle TERM _ => raise Match;
          in
            Syntax.const @{syntax_const "_NumeralType"} $ Syntax.free num
          end
      | suc_tr' _ = raise Match;
  in
   [(@{type_syntax suc}, K suc_tr')]
  end;
*}

syntax 
  "_nary_fun_type" :: "type ⇒ type ⇒ type ⇒ type" ("(_ ^/ _ ⇒/ _)" [15, 16, 15] 15)

translations
  (type) "'a ^ 'n ⇒ 'b" == (type) "('a,'n,'b) nary_fun"

现在您可以编写'n-ary 类型的函数，该函数采用'a 类型的'n 值并将'b 作为'a ^ 'n ⇒ 'b 返回，并且您可以使用χ，如Lambda 抽象和@ 987654337@点赞功能申请：

lemma "(χ x y. (x, y)) $ 1 $ 2 = (1,2)" by simp

term "(χ x y z. (x, y + z))"
(* "χ x y z. (x, y + z)" :: "'a ^ 3 ⇒ 'a × 'a" *)

我想，我对 Andreas 的表述是否对你更方便取决于你想对你的函数做什么。

Answer 2

Isabelle/HOL 在一定程度上支持任意但固定数量的函数。标准技巧是将函数的类型编码为类型的基数。因此，您实际上只有一个包含固定数量值的参数。当然，函数的所有可变参数都必须取自同一类型。在您的示例中，循环性要求已经强制执行此操作。

例如，您可以如下定义元数 n 的不变谓词的类型。

  typedef ('n :: "{one, plus}", 'a) inv_pred 
    = "{P :: ('n ⇒ 'a) ⇒ bool. ∀f. P f ⟷ P (λn. f (n + 1))}"
    morphisms apply_ip Abs_inv_pred
    by blast

在这里，我们将可变数量谓词建模为从索引集'n 到元素类型'a 的函数的谓词。 'n 的排序约束确保类型定义了操作 + 和 1，我们使用它们来指定移位。我们可以假设+ 在发生溢出时回绕，但这也可以稍后通过引理中的类型类约束来完成。

理论Numeral_Type（在~~/src/HOL/Library 的分布中）定义了写为文字数字的有限基数类型。在溢出的情况下，它们的添加确实会环绕。因此，可以写

typ "(5, int) inv_pred"

表示具有 5 个参数的谓词类型，整数在循环排列下是不变的。同样，(100, nat) inv_pred 类型包含所有此类元数为 100 的谓词。

如果您使用普通函数来编码可变的arity 参数，则没有很好的语法将函数应用于给定的参数列表。理论~~/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product 定义了一个向量类型('n, 'a) vec，也可以在这里使用。不过，您必须为此定义自己的语法，例如 apply_ip P [: x1, x2, x3, x4 :] 并编写适当的解析器和漂亮的打印机。

但是，Isabelle 在类型检查期间无法在类型级别上进行计算。因此，您将很难输入诸如

之类的术语

apply_ip P ([: x1, x2 :] ++ [: x3, x4 :])

因为 2 + 2 与 Isabelle/HOL 中的 4 类型不同。