Доказательство теорем Кок: простой закон дробей в арифметике Пеано

Question

Я изучаю coq и пытаюсь доказать равенства в арифметике пеано.

Я застрял на простом законе дробей.

Мы знаем, что (n + m) / 2 = n / 2 + m / 2 из начальной школы. В арифметике пеано это справедливо, только если n и m четны (потому что тогда деление дает правильные результаты).

Compute (3 / 2) + (5 / 2). (*3*)
Compute (3 + 5) / 2. (*4*)

Итак, мы определяем:

Theorem fraction_addition: forall n m: nat , 
    even n -> even m ->  Nat.div2 n + Nat.div2 m = Nat.div2 (n + m).

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

intros n m en em.
induction n.
- reflexivity.
- ???

Это приводит меня в ситуацию, когда

en = even (S n) а также IHn : even n -> Nat.div2 n + Nat.div2 m = Nat.div2 (n + m), поэтому я не нахожу способа применить гипотезу индукции.

После долгих поисков стандартной библиотеки и документации я не нашел ответа.

Answer 1

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

From Coq Require Import Arith Even.
Lemma nat_ind2 (P : nat -> Prop) :
  P 0 ->
  P 1 ->
  (forall n, P n -> P (S n) -> P (S (S n))) ->
  forall n, P n.
Proof.
now intros P0 P1 IH n; enough (H : P n /\ P (S n)); [|induction n]; intuition.
Qed.

nat_ind2 можно использовать следующим образом:

Theorem fraction_addition n m :
  even n -> even m ->
  Nat.div2 n + Nat.div2 m = Nat.div2 (n + m).
Proof.
  induction n using nat_ind2.
  (* here goes the rest of the proof *)
Qed.

Answer 2

Вы также можете доказать свою теорему без индукции, если вы не против использовать стандартную библиотеку.

Если вы используете Even m в вашей гипотезе (которая говорит exists n, m = 2*m), то вы можете использовать простые алгебраические переписывания с леммами из стандартной библиотеки.

Require Import PeanoNat.
Import Nat.

Goal forall n m, Even n -> Even m -> n / 2 + m / 2 = (n+m)/2.
  inversion 1; inversion 1.
  subst.
  rewrite <- mul_add_distr_l.
  rewrite ?(mul_comm 2).
  rewrite ?div_mul; auto.
Qed.

Знак вопроса просто означает "перезаписывайте как можно больше (ноль или больше) раз".

inversion 1 выполняет инверсию первой индуктивной гипотезы в цели, в данном случае сначала Even n а потом Even m. Это дает намn = 2 * x а также m = 2 * x0 в контексте, который мы затем подставляем.

Также обратите внимание even_spec: forall n : nat, even n = true <-> Even n, так что вы можете использовать even если вы предпочитаете это, просто перепишите с even_spec первый...