Coq: Зачем переписывать лемму в теореме создания двух подцелей? - PullRequest
Новая
       53

Coq: Зачем переписывать лемму в теореме создания двух подцелей?

0 голосов
/ 11 декабря 2019

Я пытаюсь доказать, что мои ненулевые функции 'распространяются по списку списков.

Я написал ненулевые' с фильтром следующим образом: 

Definition nonzeros' (l : list nat) : list nat := filter (fun x => match x with | O => false | _ => true end) l.

Я ужеДоказал это 2 леммы: 

Lemma nonzeros'_remove_0 :
  forall (a b: list nat),
  nonzeros' (0 :: b) = nonzeros' b.
Proof.
  intros a b.
  unfold nonzeros'.
  simpl. 
  reflexivity.
Qed.

Lemma nonzeros'_not_remove_Sn :
  forall (a b: list nat) (n : nat),
  nonzeros' (S n :: b) = S n :: nonzeros' b.
Proof.
  intros a b n.
  unfold nonzeros'.
  simpl. 
  reflexivity.
Qed.

Теперь я должен подтвердить распределение по concat: 

Lemma nonzero'_distribution_over_concat :
  forall (a b : list nat),
  nonzeros' (concat a b) = concat (nonzeros' a) (nonzeros' b).

Чтобы это доказать, я делаю следующее: 

Proof.
  intros a b.
  induction a as [| h t IHa].
  - 
    simpl. 
    reflexivity.
  - 
    simpl.
    destruct h.
    + rewrite nonzeros'_remove_0. rewrite nonzeros'_remove_0. rewrite IHa. reflexivity.

Проблема в том, что после тактики 

rewrite nonzeros'_remove_0.

Coq создать 2 подзадачи: 

______________________________________(1/2)
nonzeros' (concat t b) = concat (nonzeros' (0 :: t)) (nonzeros' b)
______________________________________(2/2)
list nat

Второй подзадача является неожиданной. Почему это появляется?

...