Что делать, если индукция удаляет слишком много информации, чтобы сделать цель разрешимой?

Question

Inductive subseq : list nat -> list nat -> Prop :=
  | subseq_base : subseq [] []
  | subseq_there : forall seq l x, subseq seq l -> subseq seq (x :: l)
  | subseq_here : forall seq l x, subseq seq l -> subseq (x :: seq) (x :: l).

Theorem subseq_snd :
  forall l1 l2 l,
  subseq (l1 ++ l2) l -> subseq l1 l.
Proof.
intros.
induction H.
-

1 subgoal
l1, l2 : list nat
______________________________________(1/1)
subseq l1 [ ]

По сути, Coq не может распознать, что l1 ++ l2 = [] в этом случае также означает, что l1 = [], но, поскольку нет никаких предпосылок, я также не могу доказать это.Что здесь нужно сделать?

Answer 1

Я не мог оставить этот вопрос без ответа, используя remember.Доказательство очень похоже на приведенное @HTNW, но не использует dependent induction и не выполняет вложенную индукцию.

Theorem subseq_snd :
  forall l1 l2 l,
  subseq (l1 ++ l2) l -> subseq l1 l.
Proof.
  intros. remember (l1++l2) as L.
  revert l1 l2 HeqL.
  induction H; intros.
  - destruct l1.
    + apply subseq_base.
    + discriminate.
  - apply subseq_there. eapply IHsubseq, HeqL.
  - destruct l1.
    + apply subseq_nil.
    + inversion HeqL; subst. apply subseq_here.
      eapply IHsubseq; reflexivity.
Qed.

Answer 2

Вам нужно выполнить индукцию как для l1, так и l, и использовать H для устранения невозможных случаев. По сути, я не думаю, что вы можете напрямую выполнить индукцию на H; Вы должны индуцировать значения, с которыми оно связано, и разрушать H, пока вы их просматриваете.

Эта лемма здесь должна быть определена первой, хотя. Вы могли бы включить его в доказательство, но его тип достаточно интересен, чтобы стоять в одиночестве:

Theorem subseq_nil (l : list nat): subseq nil l.
Proof.
  induction l; constructor; assumption.
Qed.

А потом главное доказательство:

Theorem subseq_snd (l1 l2 l : list nat): subseq (l1 ++ l2) l -> subseq l1 l.
Proof.
  (* I like to give parameters on the left side of the :, so I use revert to get the
     correct goal for the induction:
     forall l, subseq (l1 ++ l2) l -> subseq l1 l *)
  revert l; induction l1 as [ | x l1 Hl1]; intro l. (* It's best to give names *)
  - intros ?.
    apply subseq_nil.
  (* Below we get H : subseq (x :: foo) bar. The inversion tactic is like destruct
     but it spews out equalities about the type indices instead of leaving you stranded
     like induction would. In the l=nil case, inversion produces a contradiction,
     because subseq_nil has been ruled out, and, in the l=cons case, it case splits
     between subseq_there and subseq_here. *)
  - induction l as [ | x' l Hl]; simpl; intro H; inversion H.
    + apply subseq_there.
      apply Hl.
      assumption.
    + apply subseq_here.
      apply Hl1.
      assumption.
Qed.

Answer 3

Вы можете использовать экспериментальную тактику dependent induction.Это, наверное, ближе всего к тому, что вы хотите.Вам понадобится эта лемма:

Theorem subseq_nil (l : list nat): subseq nil l.
Proof.
  induction l; constructor; assumption.
Qed.

По сравнению с двойной induction + inversion, ее намного легче читать, даже если она длиннее.Он имеет 3 - пуль, по одной на конструктор, только с одной рекурсивной точкой входа.На самом деле, я даже не осознавал, что subseq представлял собой прерывистые подпоследовательности, пока не использовал dependent induction, что сделало структуру программы достаточно ясной, чтобы я мог понять, что происходит.Кроме того, срок действия создаваемой программы намного меньше.

Theorem subseq_app (l1 l2 l : list nat): subseq (l1 ++ l2) l -> subseq l1 l.
Proof.
  intro H.
  dependent induction H.
  - destruct l1.
    + constructor.
    + discriminate.
  - apply subseq_there.
    exact (IHsubseq _ _ eq_refl).
  - destruct l1.
    + apply subseq_nil.
    + injection x as [] prf_seq.
      apply subseq_here.
      exact (IHsubseq _ _ prf_seq).
Qed.

Answer 4

Основываясь на идее уничтожения списков, вот версия доказательства, сделанного в Идрисе для полноты. Оказывается, Идрису становится слишком тесно, если я не разрушу неявные аргументы.

data Subseq : List a -> List a -> Type where
    Base : Subseq [] []
    There : Subseq seq l -> Subseq seq (x :: l)
    Here : Subseq seq l -> Subseq (x :: seq) (x :: l)

subseq_empty : Subseq [] l
subseq_empty {l = []} = Base
subseq_empty {l = (x :: xs)} = There subseq_empty

subseq_snd : Subseq (l1 ++ l2) l -> Subseq l1 l
subseq_snd {l1 = []} {l} _ = subseq_empty
subseq_snd {l1 = (x :: xs)} {l = (y :: ys)} (There z) = There (subseq_snd z)
subseq_snd {l1 = (x :: xs)} {l = (x :: ys)} (Here z) = Here (subseq_snd z)

Помимо деструктурированных неявных аргументов, именно так и предполагалось доказательство.

Несмотря на то, что «Маленький Typer» высоко оценил тактику стиля Coq до конца, как видно из вышесказанного, есть определенные аргументы для того, чтобы сделать это, как Идрис.