Доказательство теоремы Кока: простой дробный закон в арифметике Пеано - PullRequest
Новая
       73

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

1 голос
/ 30 ноября 2019

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

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

Мы знаем, что (n + m) / 2 = n/ 2 + м / 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), поэтому я не могу найти способ применить гипотезу индукции.

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

Ответы [ 2 ]

3 голосов
/ 01 декабря 2019

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

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.
2 голосов
/ 01 декабря 2019

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

Если вы используете 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 ... ... 1020 *

...