Логика: упражнение In_app_iff

#coq #logical-foundations

#coq #логические основы

Вопрос:

Пытаясь решить In_app_iff excersize из главы Logic, я пришел к этому чудовищу:

 (* Lemma used later *)
Lemma list_nil_app : forall (A : Type) (l : list A),
    l    [] = l.
Proof.
  intros A l. induction l as [| n l' IHl'].
  - simpl. reflexivity.
  - simpl. rewrite -> IHl'. reflexivity.
Qed.

(** **** Exercise: 2 stars, standard (In_app_iff)  *)
Lemma In_app_iff : forall A l l' (a:A),
  In a (l  l') <-> In a l / In a l'.
Proof.
  intros A l l' a. split.
    induction l as [| h t IHl].
       (* l = [] *) destruct l' as [| h' t'].
           (* l' = [] *) simpl. intros H. exfalso. apply H.
           (* l' = h'::t' *) simpl. intros [H1 | H2].
          * right. left. apply H1.
          * right. right. apply H2.
       (* l = h::t *) destruct l' as [| h' t'].
          (* l' = [] *) simpl. intros [H1 | H2].
          * left. left. apply H1.
          * left. right. rewrite list_nil_app in H2. apply H2.
          (* l' = h'::t' *) intros H. simpl in H. simpl. destruct H as [H1 | H2].
          * left. left. apply H1.
          * apply IHl in H2. destruct H2 as [H21 | H22].
            ** left. right. apply H21.
            ** simpl in H22. destruct H22 as [H221 | H222].
               *** right. left. apply H221.
               *** right. right. apply H222.
    induction l as [| h t IHl].
       (* l = [] *) simpl. intros [H1 | H2].
          exfalso. apply H1.
          apply H2.
       (* l = h::t *) destruct l' as [| h' t'].
          simpl. intros [H1 | H2].
               rewrite list_nil_app. apply H1.
               exfalso. apply H2.
          simpl. intros [H1 | H2].
               destruct H1 as [H11 | H12].
                    left. apply H11.

Вот что я получил в конце:

 A : Type
h : A
t : list A
h' : A
t' : list A
a : A
IHl : In a t / In a (h' :: t') -> In a (t    h' :: t')
H12 : In a t
============================
h = a / In a (t    h' :: t')

Как я могу извлечь из H12 и IHl того факта, что In a (t h' :: t') ?

Потому что H12 находится в дизъюнкции. И этого достаточно, чтобы сделать вывод.

apply H12 in IHl. не работает.

Пожалуйста, помогите.

1. Побочные замечания: для завершения этого доказательства не требуется анализ прецедентов на l' (вы можете придумать гораздо более простое доказательство), а - также является допустимым элементом для структурирования ваших доказательств (обычно они используются в следующем порядке: - , , * -- , ** и т.д.)

2. @eponier «Побочные замечания: анализ случая на l ‘ не требуется для завершения этого доказательства (вы можете придумать гораздо более простое доказательство)» — можете ли вы дать подсказку, как это сделать в ответе?

3. Например, вы можете заменить первое destruct l' на только simpl .

Ответ №1:

Для этого есть разные способы.

Здесь вывод IHl является одним из пунктов цели, поэтому обратное рассуждение будет работать довольно хорошо.

 right. (* We will prove the right hand side of the disjunct. *)
apply IHl.
left.
apply H12.

Также возможны прямые рассуждения, хотя и немного более подробные. Используйте assert , чтобы доказать предположение, действительно необходимое IHl :

 assert (preIHl : In a t / In a (h' :: t')).
- ...
- apply IHl in preIHl.
  apply preIHl.

1. При использовании assert тактики я предпочитаю использовать фигурные скобки, например, assert (...). { some_proof. } вместо маркеров (поскольку это не анализ конкретного случая). Просто вопрос стиля.