Индукция Coq по модулю

Question

Я новичок в coq, и у меня действительно есть трудности с применением индукции. пока я могу использовать теоремы из библиотеки, или тактики, такие как омега, все это «не проблема». Но как только они не работают, я всегда застрял.

Чтобы быть точным, то теперь я пытаюсь доказать

Lemma mod_diff : forall n m : nat, n>=m /\ m <> 0 -> (n - m) mod m = n mod m. 

случай п = 0 у меня уже есть.

Proof. 
    intros. destruct H as [H1 H2 ]. induction n. 
     rewrite Nat.mod_0_l by omega. rewrite Nat.mod_0_l; omega. 

Но как сделать шаг индукции?

1 subgoal 
n : nat 
m : nat 
H1 : S n >= m 
H2 : m <> 0 
IHn : n >= m -> (n - m) mod m = n mod m 
______________________________________(1/1) 
(S n - m) mod m = S n mod m 

Answer 1

Индукционные не является необходимым для доказательства, имеются достаточные Леммы в библиотеке Coq, которые могут быть использованы. Чтобы найти эти леммы, я использовал SeachAbout modulo и SearchAbout plus.

Тогда я сделал:

Lemma mod_add_back: forall n m : nat, m <> 0 -> ((n + m) mod m) = (n mod m). 
intros. 
rewrite Nat.add_mod. 
rewrite Nat.mod_same. 
rewrite plus_0_r. 
rewrite Nat.mod_mod. 
reflexivity. 
assumption. 
assumption. 
assumption. 
Qed. 

Lemma mod_diff: forall n m : nat, n >= m /\ m <> 0 -> (n - m) mod m = n mod m. 
intros. 
intuition. 
rewrite <- mod_add_back. 
assert ((n - m + m) = n) by omega. 
rewrite H. 
reflexivity. 
intuition. 
Qed. 

Обратите внимание на использование assert ... by omega доказать экземпляр переписывания, который, кажется, не будет доступен в качестве встроенной леммы. Это немного сложно, потому что с натами это вообще не работает, но только если n >= m. (EDIT: фактически встроенная лемма Nat.sub_add работала бы).

Итак, идея в доказательстве состоит в том, чтобы сначала доказать лемму, которая позволяет вам «добавить назад» m, так как кажется хорошей идеей иметь отдельную лемму. Однако, я полагаю, это могло быть сделано как одно доказательство.

Действительно, индукция по n не продвигает доказательства вообще, потому что нет никакого способа, чтобы показать предпосылки индуктивной гипотезы (не может получить n >= m от S n >= m). Хотя индукция является важным строительным блоком, это не всегда правильный инструмент.

Answer 2

Как сказал @Atsby, уже полезные Леммы в библиотеке, так что вы можете, например, сделать

Require Import NPeano. 
Require Import Omega. 

Lemma mod_diff : forall n m : nat, n>=m /\ m <> 0 -> (n - m) mod m = n mod m. 
    intros n m [H1 H2]. 
    rewrite <- (Nat.mod_add _ 1); try rewrite mult_1_l, Nat.sub_add; auto. 
Qed. 

Что касается вашего вопроса о том, как сделать это с индукцией, мой общий совет, чтобы получить индукцию гипотеза, которая является настолько общей, насколько это возможно, т. е. не вводить количественные переменные до того, как вы сделаете induction. А также попытайтесь получить гипотезу индукции, которая также полезна для «следующего» значения. Поэтому я попытался бы доказать еще одну формулу (n + k * m) mod m = n mod m и сделать индукцию по адресу k, потому что для доказательства дела необходимо только алгебраическое переписывание от k. Однако в этом случае эта «другая формула» уже была в библиотеке, называемой Nat.sub_add.

Answer 3

Вы должны использовать другой принцип индукции.

mod функция подчиняется следующим отношениям.

Inductive mod_rel : nat -> nat -> nat -> Prop := 
    | mod_rel_1 : forall n1 n2, n2 = 0 -> mod_rel n1 n2 0 
    | mod_rel_2 : forall n1 n2, n2 > 0 -> n1 < n2 -> mod_rel n1 n2 n1 
    | mod_rel_3 : forall n1 n2 n3, n2 > 0 -> n1 >= n2 -> mod_rel (n1 - n2) n2 n3 -> mod_rel n1 n2 n3. 

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

Ниже приведена область функции mod.

Inductive mod_dom : nat -> nat -> Prop := 
    | mod_dom_1 : forall n1 n2, n2 = 0 -> mod_dom n1 n2 
    | mod_dom_2 : forall n1 n2, n2 > 0 -> n1 < n2 -> mod_dom n1 n2 
    | mod_dom_3 : forall n1 n2, n2 > 0 -> n1 >= n2 -> mod_dom (n1 - n2) n2 -> mod_dom n1 n2. 

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

Conjecture wf_ind : forall P1, (forall n1, (forall n2, n2 < n1 -> P1 n2) -> P1 n1) -> forall n1, P1 n1. 
Conjecture O_gt : forall n1, n1 = 0 \/ n1 > 0. 
Conjecture lt_ge : forall n1 n2, n1 < n2 \/ n1 >= n2. 

Conjecture mod_total : forall n1 n2, mod_dom n1 n2. 

Принцип индукции связан с областью mod «s является

Check mod_dom_ind : forall P1 : nat -> nat -> Prop, 
    (forall n1 n2, n2 = 0 -> P1 n1 n2) -> 
    (forall n1 n2, n2 > 0 -> n1 < n2 -> P1 n1 n2) -> 
    (forall n1 n2, n2 > 0 -> n1 >= n2 -> mod_dom (n1 - n2) n2 -> P1 (n1 - n2) n2 -> P1 n1 n2) -> 
    forall n1 n2, mod_dom n1 n2 -> P1 n1 n2. 

Но поскольку mod тотально, можно упростить это

Conjecture mod_ind : forall P1 : nat -> nat -> Prop, 
    (forall n1 n2, n2 = 0 -> P1 n1 n2) -> 
    (forall n1 n2, n2 > 0 -> n1 < n2 -> P1 n1 n2) -> 
    (forall n1 n2, n2 > 0 -> n1 >= n2 -> P1 (n1 - n2) n2 -> P1 n1 n2) -> 
    forall n1 n2, P1 n1 n2. 

Этот принцип индукции применяется к любой паре натуральных чисел. Это лучше подходит для доказательства фактов о mod, так как соответствует структуре определения mod. mod не может быть определен напрямую с использованием структурной рекурсии, поэтому структурная индукция только доведёт вас до того, пока вы докажете что-нибудь о mod.

Не каждое доказательство должно быть разрешено с индукцией. Вам нужно спросить себя, почему вы считаете, что что-то истинно, и перевести это на строгое доказательство. Если вы не знаете, почему это правда, вам нужно узнать или узнать, почему это так или нет.

Но деление и модуляция могут быть определены косвенно структурной рекурсией. В следующей функции n3 и n4 служат промежуточным фактором и остатком. Вы определяете его, уменьшая размер дивиденда и увеличивая остаток до тех пор, пока остаток не достигнет делителя, после чего вы увеличите коэффициент и перезагрузите остаток и продолжите. Когда дивиденд достигает нуля, у вас есть истинный коэффициент и остаток (при условии, что вы не разделили на ноль).

Conjecture ltb : nat -> nat -> bool. 

Fixpoint div_mod (n1 n2 n3 n4 : nat) : nat * nat := 
    match n1 with 
    | 0 => (n3, n4) 
    | S n1 => if ltb (S n4) n2 
    then div_mod n1 n2 n3 (S n4) 
    else div_mod n1 n2 (S n3) 0 
    end. 

Definition div (n1 n2 : nat) : nat := fst (div_mod n1 n2 0 0). 

Definition mod (n1 n2 : nat) : nat := snd (div_mod n1 n2 0 0). 

Вы до сих пор не используют структурную индукцию, чтобы доказать, что о div и mod. Вы используете его, чтобы доказать что-то около div_mod. Эти функции соответствуют следующей (структурно-индуктивной) теореме.

Theorem augmented_division_algorithm : forall n1 n2 n3 n4, n4 < n2 -> 
    exists n5 n6, n1 + n3 * n2 + n4 = n5 * n2 + n6 /\ n6 < n2. 
Proof. 
induction n1. 
firstorder. 
exists n3. 
exists n4. 
firstorder. 
firstorder. 
destruct (lt_ge (S n4) n2). 
specialize (IHn1 n2 n3 (S n4) H0). 
firstorder. 
exists x. 
exists x0. 
firstorder. 
admit. (* H1 implies the conclusion. *) 
Conjecture C2 : forall n1 n2, n1 < n2 -> 0 < n2. 
pose proof (C2 _ _ H). 
specialize (IHn1 n2 (S n3) 0). 
firstorder. 
exists x. 
exists x0. 
firstorder. 
Conjecture C3 : forall n1 n2, n1 < n2 -> S n1 >= n2 -> S n1 = n2. 
pose proof (C3 _ _ H H0). 
subst. 
cbn in *. 
admit. (* H2 implies the conclusion. *) 
Qed. 

Алгоритм обычного деления может быть получен путем установки n3 и n4 к нулю.

Conjecture division_algorithm : forall n1 n2, 0 < n2 -> exists n5 n6, 
    n1 = n5 * n2 + n6 /\ n6 < n2. 

Отказ от ответственности: гипотезы и просто типизированные функции.