Почему Coq переименовывает переменные в индукции?

Question

Я пытаюсь доказать следующую теорему.

Theorem subseq_trans : forall (l1 l2 l3 : list nat),
  subseq l1 l2 -> subseq l2 l3 -> subseq l1 l3.
Proof.
  intros l1 l2 l3 H12 H23. generalize dependent l1. (* here l2 l3 *) induction H23.
  - intros. inversion H12. apply empty.
  - (* here l1 l2 *) rename l2 into l3. rename l1 into l2. ...

В строке 3 после generalize dependent l1. у меня есть следующий контекст:

l2, l3 : list nat
H23 : subseq l2 l3

Но в строке 5 перед переименованиемУ меня есть

l1, l2 : list nat
H23 : subseq l1 l2
IHsubseq : ...

Итак l2 и l3 стали l1 и l2.Почему так случилось?Как я могу предотвратить это?

Я не думаю, что это важно, но subseq определяется так:

Inductive subseq : list nat -> list nat -> Prop :=
  | empty l : subseq [] l
  | first x l1 l2 (H : subseq l1 l2) : subseq (x :: l1) (x :: l2)
  | skip x l1 l2 (H : subseq l1 l2) : subseq l1 (x :: l2).

Моя версия Coq:

The Coq Proof Assistant, version 8.8.2 (January 2019)

Answer 1

Он переименован в l1 и l2, потому что это имя дано в определении subseq.Чтобы исправить это, вы можете явно назвать переменные при выполнении индукции:

induction H23 as [ | ? l2 l3 | ].

Здесь есть 3 случая для subseq, поэтому вам нужно 3 ветви.Я назвал списки только для случая first, поэтому я оставил имена пустыми для других случаев и использовал ? один раз, оба из которых говорят Coq использовать именование по умолчанию.