功能和归纳定义之间的平等 [英] Equality between functional and inductive definitions

问题描述

我对 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.

这篇关于功能和归纳定义之间的平等的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！