Coq无法推断`match`中的类型参数
Coq是一个交互式定理证明助理，它基于构造性类型理论。在Coq中，match语句用于模式匹配，可以根据给定的模式匹配输入的表达式，并执行相应的操作。然而，Coq无法自动推断match语句中的类型参数，需要手动指定。
在Coq中，match语句的一般形式如下：
match <expression> with
| <pattern1> => <result1>
| <pattern2> => <result2>
...
| <patternN> => <resultN>
end其中，<expression>是要匹配的表达式，<pattern>是模式，<result>是与模式匹配时要执行的操作。
对于无法推断类型参数的情况，我们可以使用@符号来显式地指定类型参数。例如，如果我们有一个类型为list nat的列表，并希望使用match语句对其进行模式匹配，可以这样写：
match myList with
| nil => ...
| cons x xs => ...
end在这个例子中，myList是一个类型为list nat的列表，nil和cons x xs是模式，...是与模式匹配时要执行的操作。注意，这里没有涉及到类型参数的推断。
如果我们需要在match语句中使用类型参数，可以使用@符号显式地指定类型参数。例如，如果我们有一个类型为list (option nat)的列表，并希望使用match语句对其进行模式匹配，可以这样写：
match myList with
| nil => ...
| cons (@Some nat x) xs => ...
| cons None xs => ...
end在这个例子中，@Some nat x和None是模式，...是与模式匹配时要执行的操作。通过在@Some前面加上nat，我们显式地指定了@Some的类型参数为nat。
总结一下，Coq无法自动推断match语句中的类型参数，需要手动指定。我们可以使用@符号来显式地指定类型参数。
相关·内容
2回答
我正在尝试计算Coq中的v元素在natlist/bag中出现的#。我试过：
Fixpoint count (v:nat) (s:bag) : nat :=
match s with
| nil => 0
| h :: tl => match h with
| v => 1 + (count v tl)
end
end.
然而，我的证据行不通：
Example test_count1: count 1 [1;2;3;1;4;1] = 3.
Proof. simpl. refle
浏览 0提问于2019-01-21得票数 0
回答已采纳
2回答
如何用coq写一个“安全”的头？
coq、proof、dependent-type
我试图在Coq中做一些类似于的事情，它定义了一个部分函数，但证明了它实际上是完全的：
{-@ head :: {xs:[a] | len xs > 0} -> a @-}
head (x:xs) = x
这是我的第一次尝试，但Coq不喜欢它(“此模式不支持强制转换”)：
Definition safeHead {A : Type} (xs : list A) (nonempty : xs <> nil) : A.
Proof.
refine (fun {A : type} (xs : list A) (pf : xs <> nil) =>
浏览 1提问于2021-06-20得票数 2
回答已采纳
1回答
Coq看不出两种类型是相同的
types、functional-programming、coq
我试图在向量上定义rev函数，它的大小被嵌入其中，我不知道如何在它上定义rev函数。
以下是我的类型定义：
Inductive vect {X : Type} : nat -> Type -> Type
:= Nil : vect 0 X
| Cons : forall n, X -> vect n X -> vect (S n) X
.
我在它上定义了一些有用的功能：
Fixpoint app {X : Type} {n m : nat} (v1 : vect n X) (v2 : vect m X)
: vect (n + m) X :=
matc
浏览 2提问于2015-09-09得票数 7
回答已采纳
1回答
Coq:将信息保存在match语句中
recursion、coq
我正在构建一个递归函数，它在list l上执行一个l。在cons分支中，我需要使用l = cons a l'的信息来证明递归函数终止。但是，当我使用match l时，信息会丢失。
如何使用match保存信息？
下面是函数(最后给出了drop和drop_lemma_le，以提高可读性)：
Fixpoint picksome (l:list nat) (H : Acc lt (length l)) {struct H}: list nat.
refine (
match l with
nil => nil
| con
浏览 4提问于2014-12-05得票数 7
回答已采纳
1回答
我试图理解Coq中的依赖类型和依赖匹配，我有下面的代码，在下面我有一个add_pair函数，其思想是我想要接收一个(依赖)列表，其中正好有两个元素，并返回列表中两个元素的和。由于列表的大小是在类型中编码的，所以我应该能够将它定义为一个总函数，但是我发现了一个错误，即match不是exaustive。
这是代码
Module IList.
Section Lists.
(* o tipo generico dos elementos da lista *)
Variable A : Set.
(* data type da lista, recebe um nat
浏览 2提问于2022-04-19得票数 1
回答已采纳
1回答
考虑以下大小列表的类型定义：
Inductive listn: nat -> Type -> Type :=
| nil: forall {A: Set}, listn 0 A
| cons: forall {n: nat} {A: Set}, A -> listn n A -> listn (S n) A.
这本质上是Idris中的类型。
我试图为init定义listn函数，它删除了最后一个元素。
我尝试的实现实际上与Idris中init的定义完全相同。这是在伊德里斯：
init : Vect (S len) elem -> Vect len elem
init
浏览 6提问于2022-03-19得票数 1
回答已采纳
4回答
如何利用Coq中有关此函数类型的信息
variadic-functions、coq、idris、dependent-type
假设我有以下类型的typ，表示bool或nat：
Inductive typ : Type := TB | TN.
我还有一个函数从typ的列表中提取一个实际的函数类型，还有一个结果类型：
Fixpoint get_types (s: seq typ) (result_type: Type) : Type :=
match s with
| nil => result_type
| x :: xs => match x with
| TN => nat -> get_types xs result_type
| TB => bool -> get_t
浏览 0提问于2018-02-24得票数 3
回答已采纳
1回答
兰伯-微积分列表中的元素数？
coq、lambda-calculus
我正在coq中编码polymorphe列表，并且我已经将类型定义为
Definition listA A :Set :=
forall T :Set, T -> (A -> T -> T) -> T.
(* empty list*)
Definition pnil (A :Set) : listA A :=
fun T: Set => fun (x : T ) => fun (c : A -> T -> T) => x.
Definition pcons (A :Set): A -> (listA A
浏览 1提问于2022-03-14得票数 1
回答已采纳
2回答
在下面的Agda程序中，我得到了关于one定义中缺少大小写的警告，尽管myList只适合cons大小写。 open import Data.Nat
data List (A : Set) : Set where
nil : List A
cons : A → List A → List A
myList : List ℕ
myList = cons 1 (cons 2 (cons 3 nil))
one : ℕ
one with myList
... | (cons x xs) = x Incomplete pattern matching for .test.with-16
浏览 40提问于2019-05-28得票数 2
回答已采纳
2回答
在Coq中通过索引实现安全的元素检索
coq、agda
我试图在Agda中演示Coq提取机制和MAlonzo编译器在代码生成方面的区别。我在Agda中提出了一个简单的例子：
data Nat : Set where
zero : Nat
succ : Nat → Nat
data List (A : Set) : Set where
nil : List A
cons : A → List A → List A
length : ∀ {A} → List A → Nat
length nil = zero
length (cons _ xs) = succ (length xs)
data Fin : Nat → Set wh
浏览 2提问于2014-05-20得票数 1
回答已采纳
2回答
Haskell初学者-定义和使用类型
haskell
我正在尝试执行与这个正确工作的代码相当的代码：
len :: [a] -> Int
len [] = 0
len (x:xs) = 1 + len xs
但是对于我定义为MyList的类型：
data MyList a = Nil | Cons a (MyList a)
以下是我的尝试：
mylen :: (MyList a) -> Int
mylen Nil = 0
mylen (Cons a (MyList a)) = 1 + mylen (MyList a)
但我知道这些错误：
范围中的‘a’不存在冲突的定义:数据构造函数‘MyList’
我想不出怎么才能让
浏览 4提问于2016-04-09得票数 0
回答已采纳
3回答
使用DataKind的类型签名中的绑定名称
haskell、syntax、type-systems
所以，我终于找到了一个可以使用新的DataKinds扩展(使用GHC7.4.1)的任务。下面是我使用的Vec：
data Nat = Z | S Nat deriving (Eq, Show)
data Vec :: Nat -> * -> * where
Nil :: Vec Z a
Cons :: a -> Vec n a -> Vec (S n) a
现在，为了方便起见，我想实现fromList。简单的递归/折叠基本上没有问题--但是我想不出如何给它正确的类型。作为参考，这是Agda版本：
fromList : ∀ {a} {A : Set a}
浏览 0提问于2012-06-28得票数 9
回答已采纳
1回答
如何在Scala中的同伴对象(带有特性)中“应用”？
scala、traits
资料来源: Scala v10中的函数编程。
在以下粘贴代码中
sealed trait List[+A]
case object Nil extends List[Nothing]
case class Cons[+A](head: A, tail: List[A]) extends List[A]
object List {
def sum(ints: List[Int]): Int = ints match {
case Nil => 0
case Cons(x,xs) => x + sum(xs)
}
def product(ds: List[D
浏览 3提问于2014-09-26得票数 2
1回答
我想创建一个依赖函数，但是我在False_rec项上遇到了一个类型不匹配错误。我试图做以下类似的事情：
Definition env A := list A.
Fixpoint zip (xs ys : env nat) (H : length xs = length ys) : env (nat * nat).
Proof.
refine
(match xs, ys with
| [], [] => []
| x :: xs, y :: ys =>
(x, y) :: zip xs ys _
| _, _ => False_rec _ _
浏览 1提问于2018-08-24得票数 0
回答已采纳
1回答
Coq中的异构列表
coq、convoy-pattern
我正在考虑编写一个Coq程序来验证的某些属性。我已经使用了一些基本的数据类型，但是连接元组会给我带来一些麻烦。
下面是代码的相关部分：
Require Import List.
Require Import String.
(* An enum representing SQL types *)
Inductive sqlType : Set := Nat | Bool.
(* Defines a map from SQL types (which are just enum values) to Coq types. *)
Fixpoint toType (t : sqlType) :
浏览 2提问于2015-04-02得票数 2
回答已采纳
1回答
无法匹配Haskell类型
haskell
我知道有很多关于这个话题的问题，但是我觉得我正在使用的库中有一些特定的东西，给了我错误。
module Test where
import Clash.Prelude
init' :: Vec (n + 1) a -> Vec n a
init' (_ :> Nil) = Nil
init' (x :> (xs:>ys)) = x :> (init' (xs:>ys))
我所犯的错误是，
Test.hs:28:14: error:
• Couldn't match type ‘n’ with ‘n0 + 1
浏览 0提问于2018-07-21得票数 1
回答已采纳
2回答
在coq中证明两表队列
recursion、queue、coq、dependent-type、fixpoint-combinators
我正在尝试证明所描述的here队列实现的正确性 Inductive queue_type (A : Type) : Type := Queue : list A -> list A -> queue_type A.
Context {A : Type}.
Definition empty_queue : queue_type A := Queue nil nil.
Definition enqueue (queue : queue_type A) (elt : A) : queue_type A :=
match queue with Queue front back =&
浏览 40提问于2021-06-23得票数 1
回答已采纳
2回答
像OCaml这样的语言如何实现模式匹配？
pattern-matching
假设我有这样的代码片段：
type 'a mylist = | Nil | Cons of 'a * 'a mylist
let rec last l =
match l with
| Nil -> None
| Cons(x, Nil) -> Some(x)
| Cons(x, xs) -> last xs
显然，此模式与mylist - Nil和Cons的构造函数匹配。我的问题是如何实现这样的东西。在找到与Cons匹配的值之前，不能只是将值输入到l，所以我假设OCaml编译器实现了类似于“反向构造函数”的东西，该构
浏览 5提问于2022-12-01得票数 2
2回答
异构列表长度中的歧义类型变量
haskell
在计算异构列表的长度时，我遇到了不明确类型变量的问题。问题似乎是长度函数在HList的元素中不是多态的。
我的密码
首先，我使用的所有语言扩展：
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
浏览 1提问于2016-05-07得票数 4
回答已采纳
1回答
Coq:分离逻辑基础中的Int与Nat的比较
coq、proof、theorem-proving
通过Separation Logic Foundations，我被Repr.v中的exercise triple_mlength卡住了。我认为我目前的问题是我不知道如何在Coq中处理int和nats。 Lemma triple_mlength: forall (L: list val) (p:loc),
triple (mlength p)
(MList L p)
(fun r => \[r = val_int (length L)] \* (MList L p)) Check (fun L => val_int (length L))不会抛出错误，所
浏览 35提问于2021-07-04得票数 1
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
活动推荐
腾讯云开发者
