可以找到一种方法＆＃x27; Reverse＆＃x27;构造函数

发布于 2025-02-01 16:53:57 字数 524 浏览 3 评论 0原文

我试图证明以下简单的引理：

Lemma wayBack :
  forall (a b n:nat) (input:list nat), a <> n -> implist n (a::b::input) -> implist n input.

暗示是如下：

Inductive implist : nat -> list nat -> Prop :=
 | GSSingle    : forall (n:nat), implist n [n]
 | GSPairLeft  : forall (a b n:nat) (l:list nat), implist n l -> implist n ([a]++[b]++l)
 | GSPairRight : forall (a b n:nat) (l:list nat), implist n l -> implist n (l++[a]++[b]).

有什么想法如何做到这一点？

谢谢！！

原文

I try to prove the following simple Lemma :

Lemma wayBack :
  forall (a b n:nat) (input:list nat), a <> n -> implist n (a::b::input) -> implist n input.

were implist is as follows :

Inductive implist : nat -> list nat -> Prop :=
 | GSSingle    : forall (n:nat), implist n [n]
 | GSPairLeft  : forall (a b n:nat) (l:list nat), implist n l -> implist n ([a]++[b]++l)
 | GSPairRight : forall (a b n:nat) (l:list nat), implist n l -> implist n (l++[a]++[b]).

Any idea how to do this ?

Thank you !!

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

婴鹅 2025-02-08 16:53:57

这里是：

Require Import Program.Equality.

Lemma wayBack :
  forall (a b n:nat) (input:list nat), a <> n -> implist n (a::b::input) -> implist n input.
Proof.
  intros.
  dependent induction H0.
  1: eassumption.
  assert (exists l', l = a :: b :: l' /\ input = l' ++ [a0 ; b0]) as [l' [-> ->]].
  {
    clear - x H0 H.
    change (l ++ [a0] ++ [b0]) with (l ++ [a0; b0]) in x.
    remember [a0; b0] as t in *.
    clear Heqt.
    induction H0 in input, t, x, H |- *.
    + cbn in *.
      inversion x ; subst.
      now destruct H.
    + cbn in *.
      inversion x ; subst ; clear x.
      eexists ; split.
      1: reflexivity.
      reflexivity.
    + cbn in x.
      rewrite <- app_assoc in x.
      edestruct IHimplist as [? []] ; try eassumption.
      subst.
      eexists ; split.
      cbn.
      2: rewrite app_assoc.
      all: reflexivity.
  }
  econstructor.
  eapply IHimplist ; try eassumption.
  reflexivity.
Qed.

这里有两个主要困难：第一个是您要对您的假设进行归纳inmandist n（a :: b :: input）>，但是由于a：：b :: input不仅是一个变量，还需要一些摆弄，该标准归纳无法做到，而是依赖归纳 程序可以。

第二个困难实际上占据了我的大部分证明，它是能够分解您在最后一个情况下获得的平等，即您在开始时而不是在列表结束时添加值。

Here it is:

Require Import Program.Equality.

Lemma wayBack :
  forall (a b n:nat) (input:list nat), a <> n -> implist n (a::b::input) -> implist n input.
Proof.
  intros.
  dependent induction H0.
  1: eassumption.
  assert (exists l', l = a :: b :: l' /\ input = l' ++ [a0 ; b0]) as [l' [-> ->]].
  {
    clear - x H0 H.
    change (l ++ [a0] ++ [b0]) with (l ++ [a0; b0]) in x.
    remember [a0; b0] as t in *.
    clear Heqt.
    induction H0 in input, t, x, H |- *.
    + cbn in *.
      inversion x ; subst.
      now destruct H.
    + cbn in *.
      inversion x ; subst ; clear x.
      eexists ; split.
      1: reflexivity.
      reflexivity.
    + cbn in x.
      rewrite <- app_assoc in x.
      edestruct IHimplist as [? []] ; try eassumption.
      subst.
      eexists ; split.
      cbn.
      2: rewrite app_assoc.
      all: reflexivity.
  }
  econstructor.
  eapply IHimplist ; try eassumption.
  reflexivity.
Qed.

There are two main difficulties here: the first is that you want to do an induction on you hypothesis implist n (a::b::input), but since a::b::input is not just a variable, there is a need for some fiddling, that standard induction cannot do, but dependent induction from Program can.

The second difficulty, which actually takes up most of my proof, is to be able to decompose the equality you get in the last case, that where you add values at the beginning rather than at the end of the list.

回复收藏 0 原文

~没有更多了~