Isabelle 中的可变参数函数

Question

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

比如我想定义所有元数为n的谓词循环置换不变的理论。给定一个类型 T 和一个整数 n，我想定义所有 arity n 谓词的理论，例如验证：P A_1,... A_n <-> P A_n A_2, .. ., A_n-1.

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

Answer 1

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。我们可以假设 + 在发生溢出时回绕，但这也可以稍后在引理中使用类型 class 约束来完成。

理论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不是同一类型。

Answer 2

做n元函数的类似方法是这样的：首先，我们定义正自然数的类型：

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 ary函数的类型，它以n类型的值'a和return a 'b作为函数的类型从 'n ⇒ 'a 和 return 中获取一个函数 '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 元类型的函数，将 'n 类型的值 'a 和 return 和 'b 作为 'a ^ 'n ⇒ 'b，你可以像 Lambda 抽象一样使用 χ，像函数应用一样使用 $：

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 的表述是否对您更方便取决于您究竟想用您的函数做什么。

Isabelle 中的可变参数函数

Variable arity function in Isabelle

isabelle