我想证明莱玛·RnP_eq。 From mathcomp Require Import ssreflect.
Require Import Coq.Program.Equality.
Definition func {n m l o:nat}
(I:t R 0 -> t R m -> t R l)(J:t R n -> t R l -> t R o):=
(fun (x:t R n)(a:t R m) => J (snd (splitat 0 x)) (I (fst (splitat 0 x)) a)).
Lemma deriveP_eq (n
我可以定义以下归纳类型:
Inductive T : Type -> Type :=
| c1 : forall (A : Type), A -> T A
| c2 : T unit.
但是,命令Check (c1 (T nat))在消息中失败:术语T nat的类型是Type@{max(Set, Top.3+1)},而它的类型是Type@{Top.3} (宇宙不一致)。
我如何调整上述归纳定义,使c1 (T nat)不会造成宇宙不一致,并且不设置宇宙多态性?
以下方法可以工作,但我更希望在不添加相等项的情况下找到解决方案:
Inductive T (A : Type) : Type
当我证明一些定理时,我的目标随着我应用越来越多的策略而变化。一般来说,目标倾向于分成多个子目标,子目标更简单。在最后一点,Coq决定目标是被证明的。这个“经过验证”的目标是什么样子的?这些目标看起来很好:
a = a. (* Any object is identical to itself (?) *)
myFunc x y = myFunc x y. (* Result of the same function with the same params
is always t
我注意到Coq对支持和类型的平等性综合了不同的归纳原则。有人对此有什么解释吗?
平等被定义为
Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x
相关的归纳原则有以下几种类型:
eq_ind
: forall (A : Type) (x : A) (P : A -> Prop),
P x -> forall y : A, x = y -> P y
现在,让我们定义一个eq的Type吊坠:
Inductive eqT {A:Type}(x:A):A->Type:= eqT_refl:
我能证明关于共进型的“共进原理”吗?例如,流类型的协归纳原理的伪代码如下所示:
Π P : Stream A -> Type.
Π destruct_head : Π x : Stream A. P x -> Σ y : A. Path A (head x) y.
Π destruct_tail : Π x : Stream A. P x -> P (tail x).
(Σ y : Stream A. P y)
我的感觉是,这是正确的,但我想不出一个方法来证明它在Coq或Agda。
在Isabelle中,我试图对相互递归的归纳定义进行规则归纳。下面是我能够创建的最简单的示例:
theory complex_exprs
imports Main
begin
datatype A = NumA int
| AB B
and B = NumB int
| BA A
inductive eval_a :: "A ⇒ int ⇒ bool" and eval_b :: "B ⇒ int ⇒ bool" where
eval_num_a: "eval_a (NumA i) i" |
eval_a_b
我很难理解什么是构造函数以及它是如何工作的。
例如,在Coq中,我们被教导这样定义自然数:
Inductive nat : Type :=
| O : nat
| S : nat -> nat.
并被告知S是一个构造函数,但这到底是什么意思呢?
如果我这样做了:
Check (S (S (S (S O)))).
我知道它是nat类型的4。
这是如何工作的,Coq如何知道(S (S (S (S O))))代表4
我猜这个问题的答案是Coq中一些非常聪明的背景魔法。
我有以下类型的家庭:
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
data Nat = Z | S Nat
type family WrapMaybes (n :: Nat) (a :: *) :: *
type instance WrapMaybes Z a = a
type instance WrapMaybes (S n) a = Maybe (WrapMaybes n a)
这在很大程度上如预期的那样工作,例如WrapMaybes (S (S Z)) Int ~ Maybe (Maybe Int)。
现在,很明显(
我今天早些时候看到了,虽然我清楚地知道,任何可能的drusba :: a -> Void实现都不会终止(毕竟,不可能构建Void),但我不明白为什么absurd :: Void -> a也是如此。审议GHC的执行情况:
newtype Void = Void Void
absurd :: Void -> a
absurd a = a `seq` spin a where
spin (Void b) = spin b
在我看来,spin无止境地解开了无限系列Void新类型包装器,即使您能够找到一个Void来传递它,也永远不会返回。无法区分的实现如下所示:
absurd
如何让Coq识别出两种类型,每种类型都是从使用相同参数从模块函子创建的模块中导入的,但出现在不同的模块中,它们实际上是相同的类型?
极小例子
Module Type S.
End S.
Module F (s : S).
Inductive foo : Type := a.
End F.
Module G (s : S).
Include F s.
End G.
Module H (s : S).
Include F.
End H.
Module I (s : S).
Module G := G s.
Module H := H s.
(* This is a type error
假设我们有一个'Client‘对象:
(我只是提到下面'Client‘对象的属性和相等方法!)
public class Client {
private Long clientId;
private String clientName;
private Integer status;
//getters and setters for above attributes
.....
...
//hashCode method
....
..
public boolean equals(Obje
我正致力于在Coq中正式化,但是对于具有非均匀类型参数的归纳数据类型,我很难通过归纳法来证明。
让我简单介绍一下我正在处理的数据类型。在Haskell中,我们将自由选择函子编码为GADT:
data Select f a where
Pure :: a -> Select f a
Select :: Select f (Either a b) -> f (a -> b) -> Select f b
这里的关键是第二个数据构造函数中的存在类型变量b。
我们可以将这个定义转换为Coq:
Inductive Select (F : Type -> T
我正在从软件基金会提供的资源中学习coq。在证明鸽子洞原理的过程中,我试图定义一个函数,从列表中提取子序列,这样里面就没有重复的元素。以下是我的定义:
Fixpoint norepeat_subseq {X : Type} (l : list X) : list X :=
match l with
| [] => []
| n :: t => match (In n t) with
| False => n :: norepeat_subseq t
| _ => norepeat_subseq t
这里是自然数均匀度的归纳和计算定义。
Inductive ev : nat -> Prop :=
| ev_0 : ev O
| ev_SS : forall n:nat, ev n -> ev (S (S n)).
Definition even (n:nat) : Prop :=
evenb n = true.
其中一个暗示了另一个。
Theorem ev__even : forall n,
ev n -> even n.
intros n E.
induction E as [ | n' E' ].
reflexivity. app
关于逻辑基础的章节。我得到了我想要理解的节选的解决方案:
Definition antisymmetric {X: Type} (R: relation X) :=
forall a b : X, (R a b) -> (R b a) -> a = b.
Theorem le_antisymmetric :
antisymmetric le.
Proof.
unfold antisymmetric. intros a b [| b' H1] H2.
- reflexivity.
- absurd (S b' <= b').
看起来,就像w/ Inductive和Fixpoint一样,你可以相互定义Function的w/ with。你能给出这个的语法和/或一个例子吗?我在任何地方都找不到任何东西。我想这和Fixpoint是一样的(在这上面也找不到)。一个不能工作(但半编译--最后两行用红色突出显示)的例子:
Variable ARG:Type.
Variable phy inf phyinf: ARG.
Function Phy (x:ARG): ARG := match x with Inf x => phyinf | _ => phy end
with Inf (x:ARG): ARG := mat
我正在尝试计算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
编辑
Require Import Bool List ZArith.
Variable A: Type.
Inductive error :=
| Todo.
Inductive result (A : Type) : Type :=
Ok : A -> result A | Ko : error -> result A.
Variable bool_of_result : result A -> bool.
Variable rules : Type.
Variable boolean : Type.
你如何解释归纳谓词?它们是用来干什么的?他们背后的理论是什么?它们只存在于依赖型系统中,还是在其他系统中?它们在某种程度上与GADT有关吗?在Coq中,为什么默认情况下它们是真的?
这是Coq的一个例子:
Inductive even : nat -> Prop :=
| even0 : even 0
| evens : forall p:nat, even p -> even (S (S P))
你将如何使用这个定义?这是一种数据类型还是一个命题?
我一直在写类似于流的东西。我能证明每个函子定律,但我想不出一种方法来证明它是全部的:
module Stream
import Classes.Verified
%default total
codata MyStream a = MkStream a (MyStream a)
mapStream : (a -> b) -> MyStream a -> MyStream b
mapStream f (MkStream a s) = MkStream (f a) (mapStream f s)
streamFunctorComposition : (s : MyStr
对于归纳类型nat,生成的归纳原则在其语句中使用构造函数O和S:
Inductive nat : Set := O : nat | S : nat -> nat
nat_ind
: forall P : nat -> Prop,
P 0 ->
(forall n : nat, P n -> P (S n)) -> forall n : nat, P n
但是对于le,生成的语句不使用构造函数le_n和le_S。
Inductive le (n : nat) : nat -> Prop :=
le_n : n <= n | le_S :