Coq: Доказательство связи между ‹и ≤

Я изучаю Coq прямо сейчас, и в более крупном доказательстве меня озадачило следующее подкрепление:

  Theorem sub : ∀ n m : nat, n ≤ m → n ≠ m → n < m.

Или в разложенном виде:

  Theorem sub : ∀ n m : nat, n ≤ m → n ≠ m → S n ≤ m.

Здесь «n ≤ m» индуктивно определяется следующим образом:

  Inductive le : nat → nat → Prop :=
  | le_n : ∀ n : nat, le n n
  | le_S : ∀ n m : nat, (le n m) → (le n (S m)).

Я не ушел очень далеко, но моя попытка выглядит так:

  Theorem sub : ∀ n m : nat, n ≤ m → n ≠ m → n < m.
  Proof.
    unfold lt.
    intro n.
    induction n.
    - induction m.
      + intros. exfalso. contradiction.
      + admit.
    - admit.
  Admitted.

На первом индуктивном шаге (отмеченном первым допуском) индуктивная гипотеза показывает следующее:

1 subgoal
m : nat
IHm : 0 ≤ m → 0 ≠ m → 1 ≤ m
______________________________________(1/1)
0 ≤ S m → 0 ≠ S m → 1 ≤ S m

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


coq proof coq-tactic
person Rakeeb Hossain    schedule 30.08.2019    source источник
comment
Обратите внимание, помимо ответа @SCappella, это тоже решит intros; lia..   -  person lelf    schedule 07.09.2019

Ответы (1)


arrow_upward
3
arrow_downward

Поскольку le определен как индуктивный предикат, имеет смысл провести индукцию по нему, а не по n. le не ссылается ни на 0, ни даже на S n (там есть S m), поэтому индукция по n, вероятно, не лучший вариант. Индукция на m может сработать, но, вероятно, сложнее, чем необходимо.

Перед тем, как приступить к формальному доказательству, часто бывает полезно подумать о том, как вы могли бы доказать это неформально (хотя все еще используя те же определения). Если вы предполагаете, что n ≤ m, то по индуктивному определению lt это означает, что либо n и m одинаковы, либо m является преемником некоторого числа m' и n меньше или равно m' (вы можете понять, почему определение из lt подразумевает это?). В первом случае нам придется использовать дополнительную гипотезу n ≠ m, чтобы вывести противоречие. Во втором случае это нам даже не понадобится. n ≤ m' означает, что S n ≤ S m', поэтому, поскольку m = S m', S n ≤ m, т.е. n < m.

Для формализации нам нужно доказать это предположение в последней строке, которое n ≤ m подразумевает S n ≤ S m. Вы должны попробовать аналогичный неформальный анализ, чтобы доказать это. В остальном неофициальное доказательство должно быть простым для формализации. Анализ дела на H: n ≤ m составляет всего destruct H..

Еще кое-что. Это не обязательно, но часто может помочь в долгосрочной перспективе. Если при определении индуктивного типа (или предиката) вы можете выделить параметр, который используется одинаково в каждом конструкторе, это может сделать принцип индукции более действенным. То, как вы это делаете с le, n универсально количественно и используется одинаково для обоих конструкторов. Каждый экземпляр le начинается с le n.

  Inductive le : nat → nat → Prop :=
  | le_n : ∀ n : nat, le n n
  | le_S : ∀ n m : nat, (le n m) → (le n (S m)).

Это означает, что мы можем вынести этот индекс в параметр.

  Inductive le' (n: nat) : nat → Prop :=
  | le_n' : le' n n
  | le_S' : ∀ m : nat, (le' n m) → (le' n (S m)).

Это дает вам немного более простой / лучший принцип индукции.

le'_ind
     : forall (n : nat) (P : nat -> Prop),
       P n ->
       (forall m : nat, le' n m -> P m -> P (S m)) ->
       forall n0 : nat, le' n n0 -> P n0

Сравните это с le_ind.

le_ind
     : forall P : nat -> nat -> Prop,
       (forall n : nat, P n n) ->
       (forall n m : nat, le n m -> P n m -> P n (S m)) ->
       forall n n0 : nat, le n n0 -> P n n0

По сути, здесь происходит то, что с le_ind вы должны доказывать все для каждого n. С le'_ind вам нужно только доказать это для конкретного n, который вы используете. Иногда это может упростить доказательства, но не обязательно для доказательства вашей теоремы. Это хорошее упражнение, чтобы доказать, что эти два предиката эквивалентны.

person SCappella    schedule 30.08.2019