Geek Answers Handbook

Coq induction modulo

I am new to coq and I am really having difficulty using induction. as long as I can use theorems from the library, or tactics like omega, all this is "no problem." But as soon as they do not work, I am always stuck.

To be precise, now I'm trying to prove

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

I already have a case n = 0.

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

But how to make an induction step?

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
+4
source share
3 answers

Induction is not required for proof; there are sufficient lemmas in the Coq library that can be used. To find these lemmas, I used SeachAbout moduloand SearchAbout plus.

Then I did:

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). , .
+5

@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+1 k . " " , Nat.sub_add.

+4

.

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.

, undefined. , , , , , , .

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 , mod. .

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,

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 . , , , reset . , ( , ).

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.

Disclaimer: hypotheses and simply typed functions.

+2
source

More articles:


All Articles