关于互归纳命题的证明

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，而是所谓的"induction over evidence"。

我的问题是 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.

您可以应用相同的想法来证明 even-length 列表的更一般的归纳方案，从中您的 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.

关于互归纳命题的证明

A proof about a mutually inductive proposition

coq

induction