功能和定义:间的平等
问题说明
我对 a列表包含的命题 P
(或重复l
)有一个归纳定义重复元素,以及对其取反的函数定义 Q
(或 no_repeats l
)。
I have an inductive definition of the proposition P
(or repeats l
) that a lists contains repeating elements, and a functional definition of it's negation Q
(or no_repeats l
).
我想证明 P<-> 〜Q
和〜P<->问
。我已经能够显示这四个含义中的三个,但是〜Q-> P
似乎有所不同,因为我无法从〜Q
中提取数据。
I want to show that P <-> ~ Q
and ~ P <-> Q
. I have been able to show three of the four implications, but ~ Q -> P
seems to be different, because I'm unable to extract data from ~Q
.
Require Import List.
Variable A : Type.
Inductive repeats : list A -> Prop := (* repeats *)
repeats_hd l x : In x l -> repeats (x::l)
| repeats_tl l x : repeats l -> repeats (x::l).
Fixpoint no_repeats (l: list A): Prop :=
match l with nil => True | a::l' => ~ In a l' /\ no_repeats l' end.
Lemma not_no_repeats_repeats: forall l, (~ no_repeats l) -> repeats l.
induction l; simpl. tauto. intros.
对 l
进行归纳后,第二个情况是
After doing induction on l
, the second case is
IHl : ~ no_repeats l -> repeats l
H : ~ (~ In a l /\ no_repeats l)
============================
repeats (a :: l)
是否有可能推论从这里开始\ /〜no_repeats l
(足够了吗?)
Is it possible to deduce In a l \/ ~ no_repeats l
(which is sufficient) from this?
正确答案
您的陈述暗示 A
上的相等支持双重否定消除:
Your statement implies that equality on A
supports double negation elimination:
Require Import List.
Import ListNotations.
Variable A : Type.
Inductive repeats : list A -> Prop := (* repeats *)
repeats_hd l x : In x l -> repeats (x::l)
| repeats_tl l x : repeats l -> repeats (x::l).
Fixpoint no_repeats (l: list A): Prop :=
match l with nil => True | a::l' => ~ In a l' /\ no_repeats l' end.
Hypothesis not_no_repeats_repeats: forall l, (~ no_repeats l) -> repeats l.
Lemma eq_nn_elim (a b : A) : ~ a <> b -> a = b.
Proof.
intros H.
assert (H' : ~ no_repeats [a; b]).
{ simpl. intuition. }
apply not_no_repeats_repeats in H'.
inversion H'; subst.
{ subst. simpl in *. intuition; tauto. }
inversion H1; simpl in *; subst; intuition.
inversion H2.
Qed.
并非每种类型都支持 eq_nn_elim
只能通过在 A
上放置其他假设来证明 not_no_repeats_repeats
。足以假设 A
具有可判定的相等性;即:
Not every type supports eq_nn_elim
, which means that you can only prove not_no_repeats_repeats
by placing additional hypotheses on A
. It should suffice to assume that A
has decidable equality; that is:
Hypothesis eq_dec a b : a = b \/ a <> b.
这篇好文章是转载于:学新通技术网
- 版权申明: 本站部分内容来自互联网,仅供学习及演示用,请勿用于商业和其他非法用途。如果侵犯了您的权益请与我们联系,请提供相关证据及您的身份证明,我们将在收到邮件后48小时内删除。
- 本站站名: 学新通技术网
- 本文地址: /reply/detail/tangkkaai
-
YouTube API 不能在 iOS (iPhone/iPad) 工作,但在桌面浏览器工作正常?
it1352 07-30 -
保持在后台运行的 iPhone 应用程序完全可操作
it1352 07-25 -
使用 iPhone 进行移动设备管理
it1352 07-23 -
iPhone,一张图像叠加到另一张图像上以创建要保存的新图像?(水印)
it1352 07-17 -
在android同时打开手电筒和前置摄像头
it1352 09-28 -
扫描 NFC 标签时是否可以启动应用程序?
it1352 08-02 -
检查邮件是否发送成功
it1352 07-25 -
Android微调工具-删除当前选择
it1352 06-20 -
希伯来语的空格句子标记化错误
it1352 06-22 -
Android App 和三星 Galaxy S4 不兼容
it1352 07-20