找不到 'reverse' 构造函数的方法

Question

我尝试证明以下简单引理：

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]).

知道怎么做吗？

谢谢！！

Answer 1

这里是：

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.

这里主要有两个难点：第一个是你想对你的假设implist n (a::b::input)进行归纳，但是由于a::b::input不仅仅是一个变量，所以需要一些摆弄，那个标准 induction 做不到，但是 Program 中的 dependent induction 可以。

第二个困难，实际上占据了我的大部分证明，是能够分解你在最后一种情况下得到的相等性，即你在列表的开头而不是末尾添加值。

找不到 'reverse' 构造函数的方法

Can't find a way to 'reverse' a constructor

coq