Используя индукцию, начиная с 1 в Coq - PullRequest
Новая
       76

Используя индукцию, начиная с 1 в Coq

0 голосов
/ 18 февраля 2019

Я пытаюсь использовать индукцию, начиная с 1 в доказательстве Coq.Из этого вопроса я получил доказательство нужного мне принципа индукции: 

Section induction_at_1.
  Variable P : nat -> Prop.
  Hypothesis p1 : P 1.
  Hypothesis pS : forall n, P n -> P (S n).

  Theorem induction_at_1:
    forall n, n > 0 -> P n.

    induction n; intro.
    - exfalso; omega.
    - destruct n.
      + apply p1.
      + assert (S n >= 1) by omega.
        intuition.
  Qed.
End induction_at_1.

То, что я получаю, выглядит структурно очень похожим на стандартную индукцию.Фактически, Check nat_ind дает 

nat_ind:
  forall P : nat -> Prop,
  P 0 ->
  (forall n : nat, P n -> P (S n)) ->
  forall n : nat, P n

, а Check induction_at_1 дает 

induction_at_1:
  forall P : nat -> Prop,
  P 1 ->
  (forall n : nat, P n -> P (S n)) ->
  forall n : nat, n > 0 -> P n

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

Lemma cancellation:
  forall a b c: nat, a > 0 -> a * b = a * c -> b = c.

Это, кажется, в точности соответствует той индукции, которую я имею выше, но когда я начинаю свое доказательство, как это 

  intros a b c H0 H1.
  induction a using induction_at_1.

Iполучите следующую ошибку, которую я не могу интерпретировать: 

Not the right number of induction arguments (expected 2 arguments).

Поскольку два принципа индукции выглядят практически одинаково для меня, я не уверен, почему это не работает.Есть идеи?

1 Ответ

0 голосов
/ 19 февраля 2019

Я также нахожу это поведение странным, но есть несколько способов обойти это.Одна из них заключается в использовании тактики индукции ssreflect, которая называется elim: 

From Coq Require Import ssreflect.

Lemma cancellation:
  forall a b c: nat, a > 0 -> a * b = a * c -> b = c.
Proof.
intros a b c H.
elim/induction_at_1: a / H.
(* ... *)
Abort.

. Во второй строке указывается Coq выполнить индукцию на H (не a), обобщая a и используяпринцип индукции induction_at_1.Я не мог получить что-то похожее на работу, используя обычную Coq induction.

Альтернативой является использование простой натуральной индукции чисел.В этом случае я полагаю, что лемма следует за индукцией по b при обобщении c (я не уверен, что индукция по a работает).Если вам нужно показать что-то в форме m <= n -> P n для всех n, вы можете заменить n на n - m + m (что должно быть возможно с гипотезой m <= n), а затем доказать P (n - m + m) по индукциина n - m.

...