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$

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