关于互归纳命题的证明

Question

考虑以下代码：

Require Import List.

Set Implicit Arguments.

Inductive even_length {A : Type} : list A -> Prop:=
| e_nil : even_length nil
| e_cons : forall e l, odd_length l -> even_length (e::l)
with
  odd_length {A : Type} : list A -> Prop :=
  | o_cons : forall e l, even_length l -> odd_length (e::l). 

Lemma map_even : forall A B (f : A -> B) (l : list A),
    even_length l -> even_length (map f l).
Proof.
  induction l.
  (** nil *)
  - intros. simpl. econstructor.
  (** cons *)
  - intros. simpl.
    inversion_clear H.
    econstructor.
    Abort. (** odd_length l -> odd_length (map f l) would help *)

请注意，我希望通过列表l 的归纳来证明它。

正如here 中所解释的，默认情况下，Coq 只生成非互感原则，并且要获得互感原则，Scheme 命令是必要的。 所以这就是我所做的：

Scheme even_length_mut := Induction for even_length Sort Prop
with odd_length_mut := Induction for odd_length Sort Prop.

Check even_length_mut.
(**   
even_length_mut
     : forall (A : Type) (P : forall l : list A, even_length l -> Prop) (P0 : forall l : list A, odd_length l -> Prop),
       P nil e_nil ->
       (forall (e : A) (l : list A) (o : odd_length l), P0 l o -> P (e :: l) (e_cons e o)) ->
       (forall (e : A) (l : list A) (e0 : even_length l), P l e0 -> P0 (e :: l) (o_cons e e0)) -> forall (l : list A) (e : even_length l), P l e 
*)

从上面的这个类型和我看到的例子中，我设法完成了这个证明：

Lemma map_even : forall A B (f : A -> B) (l : list A),
    even_length l -> even_length (map f l).
Proof.
  intros.
  apply (even_length_mut (fun l (h : even_length l) => even_length (map f l) )
                         (fun l (h : odd_length l) => odd_length (map f l) )
        ); 
    try econstructor; auto.
Qed.

但是，这种归纳并没有结束l，而是所谓的“证据之上的归纳”。

我的问题是even_length_mut 中的谓词应该是什么，所以 感应结束l？

编辑：另外，是否有可能得到odd_length l -> odd_length (map f l) 假设？

Answer 1

为了通过归纳证明这一点，我们需要对引理进行概括以获得更强的归纳假设，或者使用自定义归纳方案一次将两个元素添加到列表中，而不是只添加一个（这也需要这样的概括） .

由于默认的归纳方案（induction l）一次只添加一个元素，我们需要一个中间谓词来记录列表的“状态”在它的长度为偶数的状态之间，即我们还需要记住l 长度为奇数的情况。

Lemma map_odd_even {A B} (f : A -> B) : forall l : list A,
  (even_length l -> even_length (map f l)) /\
  (odd_length l -> odd_length (map f l)).
Proof.
  induction l.

您可以应用相同的想法来证明偶数长度列表的更一般的归纳方案，您的map_even 定理将通过apply even_list_ind 很容易地遵循。 （编辑：另一位候选人，induction l using even_list_ind 失败，我不知道为什么。）

Theorem even_list_ind {A} (P : list A -> Prop) :
  P [] ->
  (forall x y l, even_length l -> P l -> P (x :: y :: l)) ->
  forall l, even_length l -> P l.