逻辑：In App Off 练习答案

【问题标题】：Logic: In_app_iff exercize逻辑：In App Off 练习
【发布时间】：2019-04-24 21:08:04
【问题描述】：

试图解决逻辑章节中的 In_app_iff excersize 我遇到了这个怪物：

(* 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. 不起作用。

请帮忙。

【问题讨论】：

旁注：不需要对l' 的案例分析来完成这个证明（你可以想出一个更简单的证明），- 也是构建你的证明的有效子弹（通常，它们的使用顺序如下：-、+、*、--、++、**等）
@eponier “旁注：完成这个证明不需要对 l' 进行案例分析（你可以想出一个更简单的证明）” - 你能在回答？
例如，您可以仅将第一个 destruct l' 替换为 simpl。

标签： coq logical-foundations

【解决方案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.

【讨论】：

当使用assert 策略时，我更喜欢使用花括号，例如assert (...). { some_proof. } 而不是子弹（因为它不是案例分析）。只是风格问题。