1
$\begingroup$

I currently have the following subgoal in Coq:

1 subgoal
(2 unfocused at this level)

x : list char
m, n : nat
H2 : 2 * m = 3 * n

========================= (1 / 1)

exists n' : nat, n = 2 * n'

Is there any lemma inside the standard library or Mathcomp, which could be helpful to solve it?

Improve this question
$\endgroup$
2
  • $\begingroup$ Do you know how to prove this with pencil and paper? Coq is not primarily an automated theorem prover, although some people do use it for that purpose. Generally speaking, you need to know how to do a proof yourself before you can do it in Coq. $\endgroup$
    – djao
    Commented Nov 12 at 11:02
  • $\begingroup$ This is Presburger arithmetic; is there not a d.p. that can get it immediately? $\endgroup$
    – Michael Norrish
    Commented 1 hour ago

5 Answers 5

Reset to default
4
$\begingroup$ 
Require Import Lia.
  
Goal forall m n, 2*m = 3*n -> exists k, n = 2*k.
Proof.
  intros m n H. exists (m-n). lia.
Qed.
Improve this answer
$\endgroup$
2
  • $\begingroup$ Thanks. Seems like I didn't spend enough time to actual think about the proof itself... $\endgroup$
    – motrellin
    Commented Nov 15 at 13:45
  • $\begingroup$ This method does not work with 3*m = 11*n to show that 3 divides n ;-) $\endgroup$
    – Dominique Larchey-Wendling
    Commented Nov 17 at 22:19
1
$\begingroup$

You can use the dvdn predicate. Search (_ %| _ * _) should show things like dvdn_mulr, dvdn_mull, Gauss_dvdr and Gauss_dvdl and Search (_ %| _) ex should show dvdnP.

Improve this answer
$\endgroup$
2
0
$\begingroup$

For this you need Bezout. Since 2 and 3 are co-prime, there is a,b st 2a+3b = 1 + 2*3. For instance 2.2+3.1 works. Then 2an+3bn = n + 6n thus n = 2(an + 2bm - 3n) because 2m = 3n.

Improve this answer
$\endgroup$
0
$\begingroup$ 
From Coq Require Import Lia Wf_nat.

Lemma n_is_divisible_by_2_if_2_m_eq_3_n n m
  (EQ : 2 * m = 3 * n)
  : exists n', n = 2 * n'.
Proof with lia || eauto.
  rename m into l. revert n EQ. induction l as [l IH] using lt_wf_ind. intros [ | n] ?.
  - assert (claim1 : l = 0)...
  - assert (claim2 : l >= 3)... destruct l as [ | [ | [ | l]]]...
    assert (claim3 : 2 * l + 3 = 3 * n)...
    assert (claim4 : n > 0)...
    assert (claim5 : exists n', n - 1 = 2 * n').
    { eapply IH with (m := l)... }
    destruct claim5 as [n' claim5]. exists (S n')...
Qed.
Improve this answer
$\endgroup$
0
$\begingroup$

I have a proof for this that doesn't use mathcomp, but it is not even remotely idiomatic Coq.

It uses even induction.

It also uses opose proof from JoJoModding's answer to one of my earlier questions to wire up the even induction. This tactic is not in the Coq standard library, but rather stdpp from this library.

Also, I use even z to mean $\exists w \mathop. w + w = z$ not $\exists w \mathop. 2w = z$ for convenience. I use even' with the latter definition.

From stdpp Require Import tactics.
From Coq Require Import Lia.

Ltac finisher := intuition ; firstorder ; (lia || idtac) ; eauto ; simpl.

Definition even x := exists z, z + z = x.

Lemma bool_lem : forall b, b = true \/ b = false.
Proof.
  intro b.
  induction b.
  - finisher.
  - finisher.
Qed.

Fixpoint even_func x :=
  match x with
  | O => true
  | S O => false
  | S (S x) => even_func x
  end
.


Fixpoint even_induction (f : nat -> Type) (case0 : f 0) (case1 : f 1) (i : forall x, f x -> f (S (S x))) y :=
  match y with
  | O => case0
  | S O => case1
  | S (S w) => (i w) (even_induction f case0 case1 i w)
  end
.


Lemma even_iff_even_func : forall x, even x <-> even_func x = true.
Proof.
  opose proof (even_induction (fun x => even x <-> even_func x = true) _ _ _).
  - simpl. assert (0 + 0 = 0) by finisher. unfold even. now finisher.
  - simpl.
    assert ((even 1 <-> false = true) <-> not (even 1)) by finisher.
    apply H.
    unfold even.
    finisher.
  - intro x.
    intro H.
    assert (even_func (S (S x)) = even_func x) by finisher.
    rewrite H0.
    assert (even_func x = true \/ even_func x = false) by now pose proof bool_lem (even_func x).
    destruct H1.
    + assert (even x) by finisher.
      intuition.
      unfold even in H.
      firstorder.
      unfold even.
      assert (S x0 + S x0 = S (S x)) by finisher.
      finisher.
    + intuition.
      * unfold even in H.
        destruct H.
        induction x0.
        -- finisher.
        -- assert (exists w, w + w = x).
           ++ assert (x0 + x0 = x) by finisher. finisher.
           ++ now pose proof H2 H4.
      * unfold even in H4.
        destruct H4.
        assert (S x0 + S x0 = S (S x)) by finisher.
        unfold even.
        now finisher.
  - finisher.
Qed.

Lemma even_iff_even_double_successor : forall x, even x <-> even (S (S x)).
Proof.
  intro x.
  enough (even_func x = even_func (S (S x))).
  - pose proof even_iff_even_func x.
    pose proof even_iff_even_func (S (S x)).
    now finisher.
  - now finisher.
Qed.

Lemma evenness_lemma_1 : forall x, even (3 * S (S x)) <-> even (3 * x).
Proof.
  intro x.
  pose proof even_iff_even_func (3 * S (S x)).
  pose proof even_iff_even_func (3 * x).
  enough (even_func (3 * (S (S x))) = even_func (3 * x)).
  - now finisher.
  - opose proof (even_induction (fun x => even_func (3 * (S (S x))) = even_func (3 * x)) _ _ _).
    + finisher.
    + finisher.
    + intro w.
      intro I.
      assert (3 * w = w + w + w) by finisher.
      assert (3 * S( S( w)) = S( S( S( S( S( S( w + w + w ))))))) by finisher.
      rewrite H1 in I.
      rewrite H2 in I.
      rewrite H2.
      clear H1 H2.
      assert (3 * S( S( S( S( w )))) = S(S(S(S( S(S(S(S( S(S(S(S(w + w + w))))))))))))) by finisher.
      rewrite H1.
      clear H1.
      now finisher.
    + now finisher.
Qed.

Lemma evenness_lemma_2 : forall x, even (3 * x) <-> even x.
Proof.
  intro x.
  pose proof even_iff_even_func (3 * x).
  pose proof even_iff_even_func x.
  enough (even_func (3 * x) = even_func x).
  - finisher.
  - opose proof (even_induction (fun x => even_func (3 * x) = even_func x) _ _ _).
    + now finisher.
    + now finisher.
    + intro w.
      intro I.
      assert (3 * w = w + w + w) by finisher.
      rewrite H1 in I.
      clear H1.
      assert (3 * S(S(w)) = S(S(S(S(S(S(w + w + w))))))) by finisher.
      rewrite H1.
      now clear H1.
    + now finisher.
Qed.

Theorem two_m_eq_3_n : forall m n, 2 * m = 3 * n -> even n.
Proof.
  intro m.
  intro n.
  opose proof (even_induction (fun x => 2 * m = 3 * x -> even x) _ _ _).
  - unfold even. now finisher.
  - now finisher.
  - finisher.
    pose proof even_iff_even_double_successor x.
    apply H1. clear H1.
    assert (2 * m = m + m) by finisher.
    assert (m + m = 3 * S (S x)) by finisher.
    assert (even (3 * S (S x))) by finisher.
    clear H0 H1 H2.
    pose proof evenness_lemma_1 x.
    assert (even (3 * x)) by finisher.
    pose proof evenness_lemma_2 x.
    now finisher.
  - finisher.
Qed.

So yeah, it can be done with basically brute force.

Improve this answer
$\endgroup$
0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.