这是我想要证明的:
A : Type
i : nat
index_f : nat ? nat
n : nat
ip : n < i
partial_index_f : nat ? option nat
L : partial_index_f (index_f n) ? Some n
V : ? i0 : nat, i0 < i ? option A
l : ? z : nat, partial_index_f (index_f n) ? Some z ? z < i
============================
V n ip
? match
partial_index_f (index_f n) as fn
return (partial_index_f (index_f n) ? fn ? …我正在使用Menhir解析DSL.我的解析器使用精心设计的嵌套类型集合构建AST.在以后的类型检查和为用户生成的错误报告中的其他传递期间,我想参考它发生的源文件位置.这些不是解析错误,它们在解析完成后生成.
一个天真的解决方案是为所有AST类型配备额外的位置信息,但这将使得与它们一起工作(例如构建或匹配)不必要的笨拙.这样做的既定做法是什么？
当我将以下Coq数据类型提取到OCaml时:
Inductive Foo := | A | B.
Inductive Bar (f:Foo) := | C | D.
Extraction Language Ocaml.
Extraction "test.ml" Foo Bar.
我得到以下ML代码:
type foo =
| A
| B
type bar =
| C
| D
'bar'类型与Coq不同,因为它'f'作为其类型签名的一部分.
定义这些类型的最佳方法是什么,以便将它们很好地提取到OCaml？
我的代码中有几个地方看起来像这样:
let (a,b,c) = (f "a", f "b", f "c")
如果我能写下这样的话会很好:
let (a,b,c) = map f ("a", "b", "c")
如果有办法在OCaml中做这样的事情？
我正在尝试构建一个彼此依赖的模块类型的层次结构.在Coq我可以这样写:
Module Type Foo.
Parameter t:Type.
End Foo.
Module Type Bar1 (T:Foo).
Parameter f1: T.t -> T.t.
End Bar1.
Module Type Bar2 (T:Foo).
Parameter f2: T.t -> T.t.
End Bar2.
Module Ex (F:Foo) (B1: Bar1 F) (B2:Bar2 F).
End Ex.
我如何在OCaml中表达它？
是否有一种方法可以定义“本地”Ltac 表达式，我可以用它来证明引理但在外部不可见？
Lemma Foo ...
Proof.
Ltac ll := ...
destrict t.
- reflexivity.
- ll.
- ll.
Qed.
(* ll should not be visible here *)
我是Coq的新手,需要一些帮助才能让我开始.特别是我有兴趣使用依赖类型定义向量(固定大小列表)的一些操作.我从Vector包开始,尝试实现一些额外的功能.例如,我很难实现琐碎的'take'和'drop'函数,这些函数从列表中取出或删除第一个'p'元素.
Require Import Vector.
Fixpoint take {A} {n} (p:nat) (a: t A n) : p<=n -> t A p :=
match a return ( p<=n -> t A p) with
| cons A v (S m) => cons (hd v) (take m (tl v)) m
| nil => fun pf => a
end.
错误(如果是nil)是:
The term "a" has type "t A n" while it is expected to have type "t A p".
有人能帮助我一些起点吗？谢谢!
是否有一种策略可以使用而不是replace在下面的示例中来简化此表达式？
Require Import Vector.
Goal forall (n b:nat) (x:t nat n), (map (fun a => plus b a) x) = x.
Proof.
intros n b x.
replace (fun a => plus b a) with (plus b) by auto.
...