如何使用修复策略证明 coq 中列表的两步归纳

Question

我想通过使用fix策略来证明列表的两步归纳

在接下来的证明过程中，我在调用 self 之前在结构上缩小了目标（通过将 pxy 应用到目标），所以我希望在同一定理中调用 self 不会导致无限递归。

From Coq Require Import Lists.List.
Import ListNotations.

Lemma list_back_inversion : forall {X : Type} (l : list X), 
  l = [] \/ exists y l', l = l' ++ [y].
  induction l.
  - auto.
  - right. destruct IHl; subst.
    + exists a. exists []. reflexivity.
    + destruct H. destruct H. subst. exists x. exists (a::x0). reflexivity.
Qed. 

Theorem list_2_step_ind: forall (X : Type) (P : list X -> Prop),
  P [] -> (forall x, P [x]) -> (forall x y (l : list X), P l -> P (x :: l ++ [y])) -> forall l' : list X, P l'.
Proof.
  fix self 6.
  intros X P p0 px pxy l.
  destruct l.
  - apply p0.
  - destruct (list_back_inversion l).
    + subst. apply px.
    + destruct H. destruct H. subst. apply pxy. apply (self _ _ p0 px pxy).
Qed.

但是我收到了这个错误

Recursive definition of self is ill-formed.
In environment
...

Recursive call to self has principal argument equal to 
"x3" instead of one of the following variables: "l0"

我知道如何使用其他策略来证明这个定理，但现在我想通过使用 fix 来证明该定理以了解更多信息

Answer 1

正如评论中提到的，coq 会抛出该错误，因为终止检查器无法证明

l

在结构上小于

l ++ [y]

。可以添加等于列表长度的新参数并对其使用

fix

策略。

From Coq Require Import Lists.List.
Import ListNotations.
Require Import Lia.

Lemma list_back_inversion : forall {X : Type} (l : list X), 
  l = [] \/ exists y l', l = l' ++ [y].
  induction l.
  - auto.
  - right. destruct IHl; subst.
    + exists a. exists []. reflexivity.
    + destruct H. destruct H. subst. exists x. exists (a::x0). reflexivity.
Qed. 


Theorem list_2_step_with_length_arg: forall (X : Type) (P : list X -> Prop),
  P [] -> (forall x, P [x]) -> (forall x y (l : list X), P l -> P (x :: l ++ [y])) -> forall (l : list X) (len : nat) {L: len = length l}, P l.
Proof.
  fix self 7.
  intros X P p0 px pxy l len leq.
  destruct len; destruct l; simpl in *. (* to pass requirements of termination checker we need to destruct len first to end this function when len reach to 0 *)
  - apply p0.
  - inversion leq.
  - inversion leq.
  - destruct (list_back_inversion l).
      * subst. apply px.
      * destruct H. destruct H. subst. apply pxy. 
      apply (self _ _ p0 px pxy x1 (len - 1)).
      simpl in *. inversion leq. rewrite app_length. simpl. lia. 
Qed.

Theorem list_2_step: forall (X : Type) (P : list X -> Prop),
  P [] -> (forall x, P [x]) -> (forall x y (l : list X), P l -> P (x :: l ++ [y])) -> forall (l : list X), P l.
Proof.
  intros X P p0 px pxy l.
  apply (@list_2_step_with_length_arg X P p0 px pxy l (length l) eq_refl).
Qed.