0
$\begingroup$ 
Require Import ZArith.

Open Scope Z_scope.


Lemma mod_mult_or : forall a b c, (a | b) \/ (a | c) -> (a | b * c).
Proof.
intros.
destruct H as [H1|H2].
apply Zdivide_mult_l; assumption.
apply Zdivide_mult_r; assumption.
Qed.


Lemma mod_mult : forall a b c, (a | b) /\ (a | c) -> (a | b * c).
Proof.
intros a b c [Hab Hac].
apply Z_divide_mul.
apply Hab.
apply Hac.
Qed.

Close Scope Z_scope.

I keep getting all sorts of errors on both proofs. I am not quite sure how to solve each proof the correct way. If someone can help me thanks!

Improve this question
$\endgroup$
2
  • $\begingroup$ Have you tried importing Coq.ZArith.Znumtheory.? $\endgroup$
    – Couchy
    Commented Apr 25, 2023 at 3:45
  • $\begingroup$ I am trying to approach it strictly with the ZArith library and using Z_scope. $\endgroup$
    – itsFrank
    Commented Apr 25, 2023 at 16:32

2 Answers 2

Reset to default
1
$\begingroup$

You have to make the quotient explicit in a relation a | b (defined through an existential quantifier).

Lemma mod_mult_or : forall a b c, (a | b) \/ (a | c) -> (a | b * c).
Proof.
  intros.
  destruct H as [[q1 H1] | [q2 H2]].
  - exists (q1 * c).
    subst.  repeat rewrite <- Z.mul_assoc.  
    f_equal; now rewrite (Z.mul_comm  a c). 
  - 
 
Qed.
Improve this answer
$\endgroup$
4
  • $\begingroup$ Lemma mod_mult_or : forall a b c, (a | b) \/ (a | c) -> (a | b * c). Proof. intros a b c H. destruct H as [Hb | Hc]. - apply Z.divide_mul_r. exact Hb. - apply Z.divide_mul_l. exact Hc. Qed. I tried this way but it seems to have not worked. :( $\endgroup$
    – itsFrank
    Commented Apr 25, 2023 at 16:30
  • $\begingroup$ I edited the first sub-goal of the proof. What was the issue with it? $\endgroup$
    – Pierre Castéran
    Commented Apr 25, 2023 at 20:10
  • $\begingroup$ I figured it out. $\endgroup$
    – itsFrank
    Commented Apr 25, 2023 at 21:15
  • $\begingroup$ Just used unfold rewrite exists -> tactic, thanks! $\endgroup$
    – itsFrank
    Commented Apr 25, 2023 at 21:17
0
$\begingroup$

Which version of Coq are you using? This should work:

Require Import ZArith.

Open Scope Z_scope.


Lemma mod_mult_or : forall a b c, (a | b) \/ (a | c) -> (a | b * c).
Proof.
intros.
destruct H as [H1|H2].
Search (_ | _ * _).
apply Z.divide_mul_l; assumption.
apply Z.divide_mul_r; assumption.
Qed.

Lemma mod_mult : forall a b c, (a | b) /\ (a | c) -> (a | b * c).
Proof.
intros a b c [Hab Hac].
apply mod_mult_or.
left.
apply Hab.
Qed.

Close Scope Z_scope.
Improve this answer
$\endgroup$

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.