Доказательство о взаимно индуктивном предложении - PullRequest
Новая
       28

Доказательство о взаимно индуктивном предложении

0 голосов
/ 11 мая 2019

Рассмотрим следующий код: 

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.

Как объяснено в здесь ,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)?

1 Ответ

1 голос
/ 12 мая 2019

Чтобы доказать это по индукции, нам нужно либо обобщить лемму, чтобы получить более сильную гипотезу индукции, либо использовать собственную схему индукции, которая добавляет в список сразу два элемента вместо одного (который также потребует такого обобщения).

Поскольку схема индукции по умолчанию (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.

Вы можете применить ту же идею, чтобы доказать более общую схему индукции для списков четной длины, из которой ваша окончательная теорема будетследовать легко через induction l using even_list_ind, вариант тактики induction. 

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