coq - 假设并证明关于不同类型相等性的定理(证明具有依赖类型的两个偶数之和的交换性)
问题描述
简短的问题是:如何从下面的代码证明(或如何以“更好”的方式假设)定理even_sum_right_0
(even_sum_commute
或两者)
Inductive even : nat -> Type :=
| EZ : even 0
| ES : forall n, odd n -> even (S n)
with odd : nat -> Type :=
| OS : forall n, even n -> odd (S n).
Fixpoint even_sum n1 n2 (e1 : even n1) : even n2 -> even (n1 + n2) :=
match e1 with
| EZ => fun e2 => e2
| ES _ o1 => fun e2 => ES (odd_sum o1 e2)
end
with odd_sum n1 n2 (o : odd n1) : even n2 -> odd (n1 + n2) :=
match o with
| OS _ e => fun e2 => OS (even_sum e e2)
end.
Theorem add_comm_right_0 : forall n, n = n + 0.
induction n; crush.
Defined.
Theorem add_comm : forall (n m : nat), n + m = m + n.
induction n; intros.
apply add_comm_right_0.
crush.
Defined.
Theorem even_sum_commut' : forall n1 n2, even (n1 + n2) -> even (n2 + n1).
intros.
rewrite add_comm.
apply H.
Defined.
Theorem odd_sum_commut' : forall n1 n2, odd (n1 + n2) -> odd (n2 + n1).
intros. rewrite add_comm. assumption.
Defined.
Scheme even_mut := Induction for even Sort Prop
with odd_mut := Induction for odd Sort Prop.
Theorem even_sum_right_0 : forall n1 (e1 : even n1),
e1 = even_sum_commut' n1 0 (even_sum e1 EZ).
Proof.
apply (even_mut (fun n en => en = even_sum_commut' n 0 (even_sum en EZ))
(fun n on => on = odd_sum_commut' n 0 (odd_sum on EZ))).
- simpl. reflexivity.
- intros. simpl.
Admitted.
Theorem even_sum_commut : forall n1 n2 (e1 : even n1) (e2 : even n2),
even_sum e1 e2 = even_sum_commut' _ _ (even_sum e2 e1).
Proof.
Admitted.
如我所见,even_sum e1 e2
和even_sum e2 e1
是同一个术语(根据 even_sum 的定义)。所以,在我看来,定理应该是可证明的。但我不确定(类型不同,在我看来这是问题的一部分)。
长篇大论如下。
我正在阅读 Adam Chlipala 的cpdt(非常感谢作者!)。而且我也在尝试解决他提供的练习。前 4 个练习让我很高兴解决它们(因为它是相当快的事情)。但是我遇到了一个练习,如果修改它会变得更有趣。
第0.1 章来自 InductiveTypes,练习 5。
- 定义偶数和奇数自然数的互归纳类型,以便任何自然数同构于这两种类型之一的值。(这个问题不要求你证明对应关系,尽管对任务的一些解释可能是有趣的练习。)编写一个计算两个偶数之和的函数,使得函数类型保证输出也是偶数。证明这个函数是可交换的。
使用下一个定义可以轻松解决此任务:
Inductive nat_even : Type :=
| EZ' : nat_even
| EN' : nat_odd -> nat_even
with nat_odd : Type :=
| ON' : nat_even -> nat_odd.
但我想尝试一下上面给出的另一个定义(受书中给出的定义的启发)。
一个小小的解释。请注意:这不是教科书练习,这是(我自己的)修改,它使任务有点难以解决(至少对我而言)。书中的原始任务相当简单(嗯,你需要考虑一下,但仍然如此)。所以,这里没有任何可能的“违反荣誉守则”......
欢迎任何想法,我很想知道“如何以更好的方式做到这一点”或“如何以另一种方式做到这一点”。我的意思是“如何为不同类型制定和证明定理,这是否可能”。
可能有人可以给我一个指向教科书/论文的链接以供阅读。这也太棒了。
解决方案
解决此类问题的最佳方法是忘记类型依赖性。even n
在这种情况下,和的证明odd n
完全由 表征n
,如以下引理所示。
From Coq Require Import ssreflect ssrfun.
Require Import Coq.Arith.Arith.
Set Implicit Arguments.
Inductive even : nat -> Type :=
| EZ : even 0
| ES : forall n, odd n -> even (S n)
with odd : nat -> Type :=
| OS : forall n, even n -> odd (S n).
Fixpoint even_or_odd (n : nat) : even n + odd n :=
match n with
| 0 => inl EZ
| S m => match even_or_odd m with
| inl p => inr (OS p)
| inr p => inl (ES p)
end
end.
Fixpoint nat_of_evenK n (p : even n) : even_or_odd n = inl p :=
match p with
| EZ => erefl
| @ES m p => congr1 (fun r : even m + odd m =>
match r with
| inl q => inr (OS q)
| inr q => inl (ES q)
end)
(nat_of_oddK p)
end
with nat_of_oddK n (p : odd n) : even_or_odd n = inr p :=
match p with
| @OS m p => congr1 (fun r : even m + odd m =>
match r with
| inl q => inr (OS q)
| inr q => inl (ES q)
end)
(nat_of_evenK p)
end.
Lemma even_irrel n (p q : even n) : p = q.
Proof.
suff [//] : inl p = inl q :> even n + odd n.
by rewrite -2!nat_of_evenK.
Qed.
Lemma odd_irrel n (p q : odd n) : p = q.
Proof.
suff [//] : inr p = inr q :> even n + odd n.
by rewrite -2!nat_of_oddK.
Qed.
尤其,
Definition even_comm_cast n m : even (n + m) -> even (m + n) :=
let: erefl := Nat.add_comm n m in id.
Lemma even_addC n m (p : even (n + m)) (q : even (m + n)) :
p = even_comm_cast m n q.
Proof.
rewrite /even_comm_cast.
case: (n + m) / Nat.add_comm p => //= p; exact: even_irrel.
Qed.
推荐阅读
- javascript - 使 intro.js 工具提示向右强制并使页面滚动
- codeigniter - 如何在where子句codeigniter中使用数组
- jquery - 在控制器中解析二维数组
- python - 根据索引值在python中加入2个csv文件
- python-2.7 - SSL 连接错误:SSL 证书验证失败 (2026) (SQLDriverConnect) pyodbc?
- scala - 如何使用@RunWith(classOf[JUnitRunner]) 升级到 JUnit5 进行 Scala 测试?
- python - ttest_ind 给出 TypeError: unsupported operand type(s) for /: 'str' and 'int'
- javascript - React Consumer Context 无法设置状态 - 前端大师介绍 React 课程 v4 重构
- maven - Swagger CodeGen 依赖问题
- sorting - 如何仅根据第一列对行进行排序?