Почему вложение тактики индукции также вкладывает индуктивные гипотезы в лямбду?

Question

Theorem mult_comm : forall m n : nat,
  m * n = n * m.
Proof.
intros.
induction n.
- simpl. rewrite (mult_0_r m). reflexivity.
- simpl.
  rewrite <- IHn.
  induction m.
    simpl. reflexivity.
    simpl.

Выше приведено во второй главе Фонда программного обеспечения.

1 subgoal
m, n : nat
IHn : S m * n = n * S m
IHm : m * n = n * m -> m * S n = m + m * n
______________________________________(1/1)
S (n + m * S n) = S (m + (n + m * n))

Я действительно смущен тем, что IHm должно быть здесь.Насколько я понимаю, тактика Coq скомпилирована под капотом какой-то функциональной программы, но я действительно не уверен, что здесь происходит.Я почти уверен, что это не то, что я намеревался сделать.

Я хотел сделать что-то вроде следующей программы Idris.

add_comm : {a,b : Nat} -> a + b = b + a
add_assoc : {a,b,c : Nat} -> (a + b) + c = a + (b + c)

total
mult_comm : {m,n : Nat} -> (m * n) = n * m
mult_comm {m = Z} {n = Z} = Refl
mult_comm {m = Z} {n = (S k)} = mult_comm {m=Z} {n=k}
mult_comm {m = (S k)} {n = Z} = mult_comm {m=k} {n=Z}
mult_comm {m = (S k)} {n = (S j)} = 
    let prf1 = mult_comm {m=k} {n=S j}
        prf2 = mult_comm {m=S k} {n=j}
        prf3 = mult_comm {m=k} {n=j}
        prf_add_comm = add_comm {a=k} {b=j}
        prf_add_assoc = add_assoc {a=k} {b=j} {c=j*k}
        prf_add_assoc' = add_assoc {a=j} {b=k} {c=j*k} 
    in
        rewrite prf1 in
        rewrite sym prf2 in
        rewrite prf3 in
        rewrite sym prf_add_assoc in
        rewrite sym prf_add_assoc' in
        rewrite (add_comm {a=k} {b=j}) in
        Refl

В частности, мне нужно prf1prf2 и prf3, которые я получаю с помощью рекурсивных вызовов mult_comm.В Coq два доказательства застряли в лямбде, и я не уверен, как это произошло.Я вижу, что тактика Coq induction не делает то, что, я думаю, она должна делать.

В дополнение к объяснению вышеизложенного, позвольте мне также спросить, есть ли в Coq больше вводного материала, чем в Фондах программного обеспечения только весли я снова застряну на какой-то тактике?Обратите внимание, что я знаю, как решить эту проблему в Coq, поскольку нашел решение в Интернете.

Я пытался безуспешно заняться книгой SF еще в 2016 году как введение в программирование с зависимой типизацией, а теперь с преимуществом:Оглядываясь назад, я вижу, что Маленький Тайпер и книга Идрис намного лучше в этом отношении.

Answer 1

Когда вы вызываете тактику induction, Coq использует эвристику для определения предиката P : nat -> Prop, который вы хотите доказать по индукции. Перед повторным вызовом induction состояние проверки выглядит следующим образом:

  m, n : nat
  IHn : m * n = n * m
  ============================
  m * S n = m + m * n

Случилось так, что Кок решил включить предпосылку IHn в предикат индукции, который был выведен как

P m := m * n = n * m -> m * S n = m + m * n

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

Lemma double_inj : forall n m, n + n = m + m -> n = m.
Proof.
  intros n m H.
  induction n as [|n IH].
  (* ... *)

Если H был сброшен после вызова induction, вам пришлось бы доказать forall n m, n = m, что явно не выполняется.

Этот пример является одной из причин, почему часто бывает плохой идеей вызывать induction несколько раз в одном доказательстве Coq. Как мы предлагаем в этом упражнении в Основах программного обеспечения, лучше доказать вспомогательную лемму, поскольку вы можете четко указать предикат индукции. Для этого примера есть и другие варианты. Например, вы можете вызвать clear IHn, чтобы отбросить предпосылку IHn, что приведет Coq к правильному предикату. Язык доказательства ssreflect, который теперь поставляется с Coq, имеет другую тактику для выполнения индукции, которая называется elim, что позволяет вам более четко выбирать предикат.

Я согласен с вашим последним комментарием, но должен добавить, что целью программных фондов не является введение в программирование с зависимой типизацией. Несмотря на то, что Coq поддерживает эту парадигму, писать такие программы обычно непросто, и гораздо проще использовать тактику для доказательства лемм о просто типизированных программах. Например, Idris принимает ваше доказательство mult_comm, потому что его средство проверки завершения достаточно умен, чтобы распознавать все рекурсивные вызовы как убывающие, даже если они не уменьшаются относительно фиксированного аргумента (во втором предложении n уменьшается тогда как в третьем m делает). Это невозможно в Coq, и вы должны разделить определение на несколько рекурсивных функций, по одной для каждого аргумента, или использовать обоснованную индукцию для пар натуральных чисел, что в данном примере было бы излишним.

У Адама Члипалы есть еще один учебник Coq под названием CPDT , который вы, возможно, захотите проверить. Тем не менее, я не думаю, что вы найдете там исчерпывающее описание тактики Coq. Как и induction, многие тактики основаны на эвристике и их сложно объяснить подробно.

В заключение отметим, что Матье Созо разработал пакет под названием Equations , который делает программирование с зависимой типизацией в Coq намного ближе к Idris или Agda. Если вы находите этот стиль доказательства более интуитивным, вы можете попробовать использовать его.