Доказательство леммы, основанное на определениях Fixpoint

Пытаемся доказать следующую лемму:

Я пробовал развернуть nth_error и nth в цели, но я не могу придумать способ сказать Coq, чтобы он нарушил определение Fixpoint этих двух функций. Я также попытался провести индукцию по n и спискам, но ни один из них не смог решить проблему, поскольку элементы в списке не имеют отношения друг к другу. Но это, очевидно, верная лемма, сейчас я чувствую, что это недоказуемо, кто-нибудь может помочь мне решить эту проблему? Очень признателен!

Lemma nth_error_nth :
  forall nodes1 (node : node) n,
    n < length nodes1 ->
    nth_error nodes1 n = Some (nth n nodes1 node).

coq coq-tactic proof-general
person Boooooo    schedule 18.08.2019    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Ваш вопрос действительно должен быть отредактирован, чтобы включить минимальный воспроизводимый пример, чтобы нам не нужно было угадывать, какие определения вы Пользуюсь. Я предполагаю, что вы используете модуль List стандартной библиотеки, а node - это просто какой-то тип. Без дополнительной информации я просто предполагаю, что это что-то вроде Variable node: Type.

Чтобы доказать эту лемму, должна работать индукция по самому списку. Вероятно, вам также потребуется провести анализ случая для n (попробуйте destruct n), поскольку n_th и некоторые другие вещи зависят от того, является ли n 0 или нет. Если что-то кажется невозможным доказать, попробуйте усилить индуктивную гипотезу. Это предполагает наличие большего количества гипотез в цели, когда вы используете induction. Вы можете добиться этого с помощью revert или просто никогда intro рассматриваемой гипотезы.

Вы, вероятно, получите несколько абсурдных гипотез, например n ‹0. Вы можете использовать некоторые леммы из PeanoNat.Nat, чтобы вывести из этого противоречие. Было бы полезно использовать Search просторечие. Например, Search (?n < 0). находит лемму, о которой я говорил. Также есть один шаг, на котором вам нужно будет завершить m < n из S m < S n, что можно сделать с помощью Lt.lt_S_n.

Для начала вот начало доказательства.

Lemma nth_error_nth :
  forall nodes1 (node : node) n,
    n < (length nodes1) ->
    nth_error nodes1 n = Some (nth n nodes1 node).
Proof.
  (* we don't intro n since we'll need to apply
     the inductive hypothesis to two different values of n *)
  intros nodes1 node.
  induction nodes1 as [ | a nodes1 IH].
person SCappella    schedule 18.08.2019
comment
Большое спасибо и извините за опубликованный мной фрагмент кода, который вас запутал. Я провел доказательство с помощью вашего метода и, думаю, во многом опирался на вашу идею. - person Boooooo; 18.08.2019
comment
Обратите внимание, что SearchAbout устарел, поскольку 8.5 в пользу Search. - person eponier; 19.08.2019
comment
@eponier хммм, мог бы поклясться, что разница все же есть. Думаю, нет! - person SCappella; 19.08.2019