- html - 出于某种原因,IE8 对我的 Sass 文件中继承的 html5 CSS 不友好?
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景?
我正在研究 Coq 并试图证明 Martin-Lof 的等式和路径归纳的等式之间的同构。
我将这两个等式定义如下。
Module MartinLof.
Axiom eq : forall A, A -> A -> Prop.
Axiom refl : forall A, forall x : A, eq A x x.
Axiom el : forall (A : Type) (C : forall x y : A, eq A x y -> Prop),
(forall x : A, C x x (refl A x)) ->
forall a b : A, forall p : eq A a b, C a b p.
End MartinLof.
Module PathInduction.
Axiom eq : forall A, A -> A -> Prop.
Axiom refl : forall A, forall x : A, eq A x x.
Axiom el : forall (A : Type) (x : A) (P : forall a : A, eq A x a -> Prop),
P x (refl A x) -> forall y : A, forall p : eq A x y, P y p.
End PathInduction.
Definition f {A} : forall x y: A, forall m: MartinLof.eq A x y, PathInduction.eq A x y.
Proof.
apply: (MartinLof.el A (fun a b p => PathInduction.eq A a b) _ x y m).
move=> x0.
exact: PathInduction.refl A x0.
Defined.
Definition g {A} : forall x y: A, forall p: PathInduction.eq A x y, MartinLof.eq A x y.
Proof.
apply: (PathInduction.el A x (fun a p => MartinLof.eq A x a) _ y p).
exact: MartinLof.refl A x.
Defined.
Definition pf1 {A}: forall x y: A, forall m: MartinLof.eq A x y,
eq m (g x y (f x y m)).
Definition pf2 {A} : forall x y: A, forall p: PathInduction.eq A x y,
eq p (f x y (g x y p)).
(g x y (f x y m))
最佳答案
问题是你对身份类型的定义不完整,因为它没有指定如何el
与 refl
互动.这是一个完整的解决方案。
From mathcomp Require Import ssreflect.
Module MartinLof.
Axiom eq : forall A, A -> A -> Prop.
Axiom refl : forall A, forall x : A, eq A x x.
Axiom el : forall (A : Type) (C : forall x y : A, eq A x y -> Prop),
(forall x : A, C x x (refl A x)) ->
forall a b : A, forall p : eq A a b, C a b p.
Axiom el_refl : forall (A : Type) (C : forall x y : A, eq A x y -> Prop)
(CR : forall x : A, C x x (refl A x)),
forall x : A, el A C CR x x (refl A x) = CR x.
End MartinLof.
Module PathInduction.
Axiom eq : forall A, A -> A -> Prop.
Axiom refl : forall A, forall x : A, eq A x x.
Axiom el : forall (A : Type) (x : A) (P : forall a : A, eq A x a -> Prop),
P x (refl A x) -> forall y : A, forall p : eq A x y, P y p.
Axiom el_refl : forall (A : Type) (x : A) (P : forall y : A, eq A x y -> Prop)
(PR : P x (refl A x)),
el A x P PR x (refl A x) = PR.
End PathInduction.
Definition f {A} (x y: A) (m: MartinLof.eq A x y) : PathInduction.eq A x y.
Proof.
apply: (MartinLof.el A (fun a b p => PathInduction.eq A a b) _ x y m).
move=> x0.
exact: PathInduction.refl A x0.
Defined.
Definition g {A} (x y: A) (p: PathInduction.eq A x y) : MartinLof.eq A x y.
Proof.
apply: (PathInduction.el A x (fun a p => MartinLof.eq A x a) _ y p).
exact: MartinLof.refl A x.
Defined.
Definition pf1 {A} (x y: A) (m: MartinLof.eq A x y) : eq m (g x y (f x y m)).
Proof.
apply: (MartinLof.el A (fun x y p => p = g x y (f x y p))) => x0.
by rewrite /f MartinLof.el_refl /g PathInduction.el_refl.
Qed.
Definition pf2 {A} (x y: A) (m: PathInduction.eq A x y) : eq m (f x y (g x y m)).
Proof.
apply: (PathInduction.el A x (fun y p => p = f x y (g x y p))).
by rewrite /f /g PathInduction.el_refl MartinLof.el_refl.
Qed.
eq1_rect
也可以实现类似的定义。和
eq2_rect
.
Inductive eq1 (A : Type) (x : A) : A -> Type :=
| eq1_refl : eq1 A x x.
Inductive eq2 (A : Type) : A -> A -> Type :=
| eq2_refl x : eq2 A x x.
Definition f {A} {x y : A} (p : eq1 A x y) : eq2 A x y :=
match p with eq1_refl _ _ => eq2_refl A x end.
Definition g {A} {x y : A} (p : eq2 A x y) : eq1 A x y :=
match p with eq2_refl _ z => eq1_refl A z end.
Definition fg {A} (x y : A) (p : eq2 A x y) : f (g p) = p :=
match p with eq2_refl _ _ => eq_refl end.
Definition gf {A} (x y : A) (p : eq1 A x y) : g (f p) = p :=
match p with eq1_refl _ _ => eq_refl end.
eq1
对应于您的
PathInduction.eq
, 和
eq2
对应于您的
MartinLof.eq
.您可以通过让 Coq 打印其递归原则的类型来检查这一点:
Check eq1_rect.
Check eq2_rect.
Type
中定义了这两个而不是
Prop
.我这样做只是为了让 Coq 生成的递归原则更接近你所拥有的;默认情况下,Coq 对
Prop
中定义的事物使用更简单的递归原则。 (尽管可以通过一些命令更改该行为)。
关于equality - 证明 Coq 中 Martin-Lof 等式和路径归纳之间的同构,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/45488325/
我正在尝试理解 Coq 定理: Theorem thm0 : UseCl Pos (PredVP (UsePN john_PN) walk_V) -> UseCl Pos
编辑 Require Import Bool List ZArith. Variable A: Type. Inductive error := | Todo. Induc
我试图在 Coq 中证明以下引理: Lemma not_eq_S2: forall m n, S m <> S n -> m <> n. 这似乎很容易,但我不知道如何完成证明。有人可以帮帮我吗? 谢谢
我想查看我的证明中使用的所有公理。 获取此类信息的最简单方法是什么? 我将使用哪些命令、脚本或工具? 我对所有公理或所有使用过的公理感兴趣。 最佳答案 你应该使用 Print Assumptions
我想以某种方式限制在归纳定义中允许什么样的输入构造函数。说我想说定义二进制数如下: Inductive bin : Type := | O : bin | D : bin -> bin |
Coq 标准库中是否有对自然数进行欧几里德除法的函数?我一直无法找到一个。如果没有,那么从数学上讲,是否有理由不应该有一个? 我想要这个的原因是因为我试图将一个列表分成两个较小的列表。我希望一个列表的
我在将参数传递给 coq 中的产品类型时遇到问题。我有一个看起来像这样的定义, Definition bar (a:Type) := a->Type. 我需要定义一个函数,它接收“a”和“ba
这是本在线类(class)中出现的证明https://softwarefoundations.cis.upenn.edu/plf-current/StlcProp.html#lab222 . Proo
在命题和谓词演算中证明了数十个引理后(有些比其他的更具挑战性,但通常仍然可以在 intro-apply-destruct 自动驾驶仪上证明)我从 ~forall 开始打了一个并立即被捕获。显然,我缺乏
我正在学习命题逻辑和推理规则。析取三段论规则指出,如果我们的前提中有(P 或 Q),并且也有(非 P);然后我们可以到达Q。 我一生都无法弄清楚如何在 Coq 中做到这一点。假设我有: H : A \
从 Coq 引用手册 (8.5p1) 来看,我的印象是 revert是 intro 的倒数,但 generalize 也是如此在某种程度上。例如,revert和 generalize dependen
假设我知道某些自然数是好的。我知道 1 很好,如果 n 很好,那么 3n 就是,如果 n 很好,那么 n+5 就是,这些只是构造好数字的方法。在我看来,这在 Coq 中的充分形式化是 Inductiv
通常在 Coq 中,我发现自己在做以下事情:我有证明目标,例如: some_constructor a c d = some_constructor b c d 而我真的只需要证明a = b因为无论如
我希望能够为不同的归纳定义定义相同的 Coq 符号,并根据参数的类型区分这些符号。 这是一个最小的例子: Inductive type : Type := | TBool : type. Induct
有没有办法对 Coq 的类型类使用递归?例如,在为列表定义显示时,如果您想调用 show递归列表函数,那么你将不得不使用这样的固定点: Require Import Strings.String. R
假设我有一个解决某种引理的奇特策略: Ltac solveFancy := some_preparation; repeat (first [important_step1 | importa
我是 Coq 的新手。我注意到可以使用在 Coq 中定义空集 Inductive Empty_set : Set :=. 是否也可以将函数从空集定义为另一个通用集/类型? 如果是这样怎么办? 最佳答案
有人能给我一个 Coq 中存在实例化和存在泛化的简单例子吗?当我想证明exists x, P ,其中 P是一些 Prop使用 x ,我经常想命名x (如 x0 或类似的),并操纵 P。这可以是 Coq
我见过很多在功能上相互重叠的 Coq 策略。 例如,当您在假设中有确切的结论时,您可以使用 assumption , apply , exact , trivial ,也许还有其他人。其他示例包括 d
我需要使用标准库中称为 Coq.Arith.PeanoNat ( https://coq.inria.fr/library/Coq.Arith.PeanoNat.html ) 的部分。 我尝试过导入整
我是一名优秀的程序员,十分优秀!