尝试归纳使用typedef,布尔列表和nat长度的位向量

用户名

我研究了Coq及其相关类型。我对这一切只有最模糊的想法,但是现在我想将一个矢量作为a bool list,其中矢量的长度是该类型的一部分。

(这个问题可能是另一个问题的前身。在下一个问题中,如果我提出这个问题,我将问我在使用typedef以下方法时是否可以弥补损失的钱。)

(对于这个问题,这个问题在底部)

这是我想要的类型的要求:

  • 它必须使用bool list,以便我可以直接或间接在列表上进行模式匹配和递归,并且
  • 向量的长度必须在类型中指定。

这是我所拥有的:

typedef bitvec_4 = "{bl::bool list. length bl = 4}"
  by(auto, metis Ex_list_of_length)

列表的长度必须是类型的一部分,这一点很重要,因为我想将类型与a一起使用definition,其中所有列表的大小都相同,例如以下示例所示:

definition two_bv4_to_bv4 :: "bitvec_4 => bitvec_4 => bitvec_4" where
  "two_bv4_to_bv4 x y = x"

在一个定理中,我不需要指定列表的长度。类型类最终将以某种方式发挥作用,但是正如我所说的,我想在类型定义中指定长度。

定义和类型签名。我在哪里放n = 4!! (具有最小幽默价值的技术笑话)

现在,我尝试用typedef这样的概括,其中长度是一个变量:

typedef bitvec_n = "{(bl::bool list, n::nat). length bl = n}"
  by(auto)

不好 在下一个这样的定义中,我的类型不能保证所有列表的长度都相同:

definition two_bvn_to_bvn :: "bitvec_n => bitvec_n => bitvec_n" where
  "two_bvn_to_bvn x y = x"

有问题吗 (我想是这样)

我已经对bitvec_4上述类型进行了一些试验如果我没有遇到大障碍,我可能会尝试充分利用它们。

我可以为2的幂定义上述类型,最多1024个位,以及反映它们共同属性的类型类。

但是,还有更好的方法吗?我认为,使用一定要简单明了bool list

更新(了解实际的答案)

根据Manuel的回答,我在这里包括一个独立的理论。

它主要是Manuel资料的重复,但是最后,我的功能swap_blswap_2bv以及最终使用value展示了我试图完成的工作的最终结果。我的评论强调了我心中的问题,也许我的最终应用程序表明了为什么我没有将其HOL/Word作为解决方案。

对于typedef类型,要进行间接模式匹配,类似于使用swap_bl2 bitvec,我将AbsRep函数一起用作反函数。正如曼努埃尔指出的那样,一个问题是我可以输入错误长度Abs函数a bool list,并且不会出错。另一个大问题是由于使用该Abs函数而导致抽象冲突

这些问题,想知道我是否可以恢复value对我的typedef类型的使用,这将是我下一个问题的一部分,但此处已回答了所有问题。

theory i141210ac__testing_out_manuels_answer
imports Main "~~/src/HOL/Library/Numeral_Type"
begin
(*Basic type definition.*)
  typedef ('n::finite) bitvec = "{bs :: bool list. length bs = CARD('n)}"
    morphisms bitvec_to_list Abs_bitvec
    by (simp add: Ex_list_of_length)

  setup_lifting type_definition_bitvec

  lift_definition nth :: "('n::finite) bitvec => nat => bool" (infixl "$" 90) 
    is List.nth .

(*Can't use 'value' yet for 'nth', or I get an abstraction violation.*)
  term "(Abs_bitvec [True,False] :: 2 bitvec) $ 1"

(*Truncate or fill the list: needed to set things up for 'value'.*)
  definition set_length :: "nat => bool list => bool list" where
    "set_length n xs = (if length xs < n 
                        then xs @ replicate (n - length xs) False 
                        else take n xs)"              
  lemma length_set_length [simp]: "length (set_length n xs) = n"
    unfolding set_length_def by auto

  definition list_to_bitvec :: "bool list => ('n::finite) bitvec" where
    "list_to_bitvec xs = Abs_bitvec (set_length CARD('n) xs)"
  
(*Finishing the magic needed for 'value'.*)
  lemma list_to_bitvec_code [code abstract]:
    "bitvec_to_list (list_to_bitvec xs :: ('n::finite) bitvec) 
      = set_length CARD('n) xs"
    unfolding list_to_bitvec_def by(simp add: Abs_bitvec_inverse)
  
(*Inverses for lists of length 2: no abstraction violations.*)
  value "list_to_bitvec (bitvec_to_list x) :: 2 bitvec"
  value "bitvec_to_list (list_to_bitvec x :: 2 bitvec)"

(*The magic now kicks in for 'value' and 'nth'. Understanding is optional.*)
  value "(list_to_bitvec [True,False] :: 2 bitvec) $ 1" (*OUTPUT: False.*)

(*For my use, the primary context of all this is pattern matching on lists.
  I can't pattern match on a 'typedef' type directly with 'fun', because 
  it's not a 'datatype'. I do it indirectly.*)
  
fun swap_bl :: "bool list => bool list" where
  "swap_bl [a,b] = [b,a]"
 |"swap_bl _ = undefined"
 
definition swap_2bv :: "2 bitvec => 2 bitvec" where
  "swap_2bv bv = list_to_bitvec (swap_bl (bitvec_to_list bv))"

value "swap_2bv (list_to_bitvec [a,b] :: 2 bitvec)" (*
  OUTPUT: "Abs_bitvec [b, a]" :: "2 bitvec" *)

(*Whether that's all a good idea, that's about the future, but it appears the 
  hard work, recovering the use of 'value', along with generalizing length,
  has been done by Manuel, and the authors of Numeral_Type and its imports.*)
end
曼努埃尔·埃伯

伊莎贝尔也不会支持相关的类型,但有办法还是做你想做的事。例如,已经有用于类型级自然数的类型类和类型语法的堆栈。

theory Scratch
imports Main "~~/src/HOL/Library/Numeral_Type"
begin

lemma "(UNIV :: 4 set) = {0,1,2,3}"
  by (subst UNIV_enum) eval

如您所见,类型4是包含从0数字的类型3顺便说一下,这也可以用于模块化算术中的计算:

lemma "((2 + 3) :: 4) = 1" by simp
lemma "((2 * 3) :: 4) = 2" by simp

您可以使用以下数字类型来参数化长度的位向量:

typedef ('n::finite) bitvec = "{bs :: bool list. length bs = CARD('n)}"
  morphisms bitvec_to_list Abs_bitvec
  by (simp add: Ex_list_of_length)

setup_lifting type_definition_bitvec

您可以通过将nth函数从布尔列表提升为位向量来访问位向量的第n个元素,该功能会自动运行:

lift_definition nth :: "('n::finite) bitvec ⇒ nat ⇒ bool" (infixl "$" 90) is List.nth .

将布尔列表转换为位向量有点棘手,因为您进入的列表长度可能不正确。该表达式list_to_bitvec [True] :: 2 bitvec将进行类型检查,但显然存在问题。您可以通过返回undefined或者在这种情况下更合适的方法来解决此问题,在该列表中填充False或截断列表以获取正确的长度:

definition set_length :: "nat ⇒ bool list ⇒ bool list" where
  "set_length n xs = (if length xs < n then xs @ replicate (n - length xs) False else take n xs)"

lemma length_set_length[simp]: "length (set_length n xs) = n"
  unfolding set_length_def by auto

现在,我们可以定义一个将布尔值列表转换为位向量的函数:

definition list_to_bitvec :: "bool list ⇒ ('n::finite) bitvec" where
  "list_to_bitvec xs = Abs_bitvec (set_length CARD('n) xs)"

但是,我们不允许Abs_bitvec在代码方程式中使用如果您尝试评估,例如list_to_bitvec [True] :: 1 bitvec,您将得到抽象违规。我们必须根据同态性给出一个明确的代码抽象方程list_to_bitvec

lemma list_to_bitvec_code[code abstract]:
  "bitvec_to_list (list_to_bitvec xs :: ('n::finite) bitvec) = set_length CARD('n) xs"
  unfolding list_to_bitvec_def by (simp add: Abs_bitvec_inverse)

现在我们已经基本完成,可以执行以下操作:

definition myvec :: "4 bitvec" where "myvec = list_to_bitvec [True, False, True]"

value myvec
(* Output: "Abs_bitvec [True, False, True, False]" :: "4 bitvec" *)

value "myvec $ 2"
(* Output: "True" :: "bool" *)

注意,您总是必须list_to_bitvec用其长度注释结果Isabelle无法推断长度。

您可能还想看看其中的Word理论~~/src/HOL/Word/它实现固定长度的机器字与各种位操作的像NOTANDOR等:

value "42 AND 23 :: 32 word"
(* Output: "2" :: "32 word" *)

value "293 :: 8 word"
(* Output: "37" :: "8 word" *)

value "test_bit (42 :: 8 word) 1"
(* Output: "True" :: "bool" *)

value "set_bit (42 :: 8 word) 2 True"
(* Output: "46" :: "8 word" *)

value "(BITS i. i < 4) :: 8 word"
(* Output: "15" :: "8 word" *)

另一个相关类型是中的向量src/HOL/Library/Multivariate_Analysis/Finite_Cartesian_Product

本文收集自互联网,转载请注明来源。

如有侵权,请联系[email protected] 删除。

编辑于
0

我来说两句

0条评论
登录后参与评论

相关文章

来自分类Dev

创建链接的向量和列表

来自分类Dev

使用单个fold_left查找列表的长度和总和

来自分类Dev

是否可以将一位的位向量转换为SMTLib2中的布尔变量?

来自分类Dev

关于使用数组和位向量的集合

来自分类Dev

每行的缓存位和总长度

来自分类Dev

计算给定角度和长度的向量

来自分类Dev

在方案中使用位向量

来自分类Dev

列表的总数和长度

来自分类Dev

如何根据列表的长度分割字符向量

来自分类Dev

位向量与布尔值性能列表

来自分类Dev

使用forcats和purrr总结字符向量列表

来自分类Dev

了解和使用Coq中的嵌套归纳定义

来自分类Dev

使用gsub和mapply从另一个长度不同的单词向量中删除单词的向量

来自分类Dev

使用C ++,尝试使用for循环和std :: max查找向量中的最大单词

来自分类Dev

为什么不将向量和列表一起使用?

来自分类Dev

列表中存储的逻辑向量的按位或

来自分类Dev

每行的缓存位和总长度

来自分类Dev

在方案中使用位向量

来自分类Dev

列表的总数和长度

来自分类Dev

Haskell中的结构归纳和归纳假设

来自分类Dev

使用If尝试获取一定长度的向量

来自分类Dev

尝试使用“ len”功能查找列表长度时出现语法错误

来自分类Dev

如果其他语句和向量长度

来自分类Dev

如何根据列表的长度分割字符向量

来自分类Dev

列表中每个向量的长度,然后加到向量(R)中

来自分类Dev

使用 max 和 key 的列表列表中的最大长度列表

来自分类Dev

列表中列表的长度并返回布尔值

来自分类Dev

尝试从数据帧和向量列表中取消列出数据帧时出错

来自分类Dev

尝试使用归纳谓词时出现语法错误

Related 相关文章

热门标签

归档