在比赛中展开类型功能(例如销毁) [英] Unfold a type-function in a match (like destruct)
问题描述
我想编写一个固定点定义,该定义与不带证明模式的从属类型内的值匹配.根本的问题是Coq不会使用 match
来注意类型在依赖类型中是等效的.我可以在证明模式下强制使用它,但是我想知道是否可以在没有它的情况下这样做.
I want to write a fixpoint definition that matches over a value inside a dependent type without proof-mode. The essential issue is that Coq won't use the match
to notice that the types are equivalent in a dependent type; I can force it in proof-mode, but I wonder if it's possible to do so without it.
我正在从事一个涉及大量矩阵运算的项目.矩阵可以是任意多个维度(每个维度都是矩形),所以我写了一个定义来计算矩阵的类型:
I'm working on a project that involves lots of matrix operations. The matrices can be arbitrarily many dimensions (each of which is rectangular), so I wrote a definition to compute the type of the matrix:
Require Import Coq.Unicode.Utf8.
Require Export Vector.
Import VectorNotations.
Require Import List.
Import ListNotations.
Fixpoint matrix (A: Type) (dims: list nat) :=
match dims with
| [] => A
| head::tail => Vector.t (matrix A tail) head
end.
对于原因",我需要线性化元素以选择线性化矩阵的第n个元素.我的第一个尝试是尝试返回一维矩阵,但是我碰到了List的 fold_left
的一堵墙(有关处理的建议,将不胜感激):
For "reasons" I need to linearize the elements in order to select the nth element of a linearized matrix. My first attempt was to try to return a single-dimensional matrix, but I ran into a wall with List's fold_left
(advice on proceeding would be appreciated):
Definition product (dims: list nat) := List.fold_left Nat.mul dims 1.
Definition linearize {A: Type} {dims: list nat} (m: matrix A dims): matrix A [product dims].
Proof.
generalize dependent m.
induction dims.
- intros.
assert (product [] = 1) by reflexivity. rewrite H; clear H.
exact (Vector.cons A m 0 (Vector.nil A)).
- intros.
(* why so hard? *)
assert (product (a::dims) = a * product dims).
{ unfold product.
assert (a::dims = [a] ++ dims) by reflexivity. rewrite H; clear H.
rewrite List.fold_left_app.
assert (List.fold_left Nat.mul [a] 1 = a). admit. }
Abort.
我认为转换为列表可能会更容易,所以:
I decided it might be easier to convert to a list, so:
Fixpoint linearize' {A: Type} {dims: list nat} (m: matrix A dims): list A :=
match dims with
| [] => []
| h::t => Vector.fold_left
(@app A)
[]
(Vector.map linearize' (m: Vector.t (matrix (list A) t) h))
end.
但Coq抱怨:
In environment
linearize' : ∀ (A : Type) (dims : list nat), matrix A dims → list A
A : Type
dims : list nat
m : matrix A dims
h : nat
t : list nat
The term "m" has type "matrix A dims" while it is expected to have type
"Vector.t (matrix (list A) t) h".
我可以使用校对样式"来写定义,但是我感到困惑,因为我无法让Coq接受本质上相同的定点!
I am able to write the definition using a "proof style," but I am flummoxed that I cannot get Coq to accept the fixpoint that is essentially the same!
Definition linearize {A: Type} {dims: list nat} (m: matrix A dims): list A.
Proof.
induction dims.
- (* unfold matrix in m. *) (* exact [m]. *) apply [m].
- simpl in m.
(* exact (Vector.fold_left (@List.app A) [] (Vector.map IHdims m)). *)
apply (Vector.map IHdims) in m.
apply (Vector.fold_left (@List.app A) [] m).
Defined.
好像我可以让Coq破坏 m
的类型以及 dims
,就像归纳法一样,我会很高兴…这里是打印线性化.
It seems like if I could get Coq to destruct the type of m
along with dims
, like what happens in induction, I would be good to go… here's Print linearize.
linearize =
λ (A : Type) (dims : list nat) (m : matrix A dims),
list_rect (λ dims0 : list nat, matrix A dims0 → list A)
(λ m0 : matrix A [], [m0])
(λ (a : nat) (dims0 : list nat) (IHdims : matrix A dims0 → list A)
(m0 : matrix A (a :: dims0)),
let m1 := Vector.map IHdims m0 in Vector.fold_left (app (A:=A)) [] m1)
dims m
: ∀ (A : Type) (dims : list nat), matrix A dims → list A
Arguments linearize {A}%type_scope {dims}%list_scope _
推荐答案
我的第一个反应是" List.fold_left
,他将会度过一段糟糕的时光."
My first reaction was "List.fold_left
, he's going to have a bad time."
这是使用 List.fold_right
的解决方案.
Definition product (dims: list nat) := List.fold_right Nat.mul 1 dims.
Fixpoint concat {A} {n m : nat} (v : Vector.t (Vector.t A m) n) : Vector.t A (n * m) :=
match v with
| []%vector => []%vector
| (x :: xs)%vector => append x (concat xs)
end.
Fixpoint linearize {A: Type} {dims: list nat} : matrix A dims -> matrix A [product dims] :=
match dims with
| [] => fun a => (a :: [])%vector
| head :: tail => fun a => concat (Vector.map (linearize (dims := tail)) a)
end.
fold_left
的问题在于,在非空的情况下,它会展开为立即递归调用,这将为依赖类型的编程隐藏太多信息.一种用例可能是定义尾递归函数,但这不适用于此处.
The problem with fold_left
is that, in the non-empty case, it unfolds to an immediate recursive call, which keeps too much information hidden for dependently typed programming. One use case might be to define tail-recursive functions, but this is not applicable here.
使用 fold_right
,每当您对 dims
进行图案匹配时, cons
案例都会暴露出一个 Nat.mul
其中允许使用 concat:Vector.t(Vector.t A m)n->Vector.t A(n * m)
.
With fold_right
, whenever you pattern-match on dims
, the cons
case exposes one Nat.mul
which permits one use of concat : Vector.t (Vector.t A m) n -> Vector.t A (n * m)
.
这篇关于在比赛中展开类型功能(例如销毁)的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!