2
$\begingroup$

What would be a more convenient better way to solve this proof in a less clustered/confusing way?

Lemma trial_ex : forall a b c d : Z, (a | b * c) -> Zis_gcd a b d -> (a | c * d).
Proof.
intros a b c d H1 H2.
destruct H1 as [z H3].
exists (d * z).
apply Zis_gcd_bezout in H2.
destruct H2 as [x y H4].
unfold Z.divide in *.
destruct H3 as [H5 H6].
rewrite <- H4.
rewrite Z.mul_add_distr_r.
rewrite H4.
replace (x * (a * z)) with (x * a * z) by ring.
replace (y * b * z) with (y * (b * z)) by ring.
replace (x * a * z + y * (b * z)) with (x * a * z + y * b * z) by ring.
replace (x * a * z + y * b * z) with ((x * a + y * b) * z) by ring.
replace (x * a + y * b) with d by assumption.
rewrite <- H4. 
rewrite <- Z.mul_add_distr_r.
rewrite Z.mul_comm with (n:=a) (m:=c). 
rewrite Z.mul_assoc. 
reflexivity.
Improve this question
$\endgroup$
4
  • $\begingroup$ Welcome to PA.SE! This is a good question. It is okay to set up multiple accounts, as long as you don't use them to vote oneself, circumvent bans, etc. I'm not an expert of Coq, but I hope someone else can answer your question! $\endgroup$
    – Trebor ♦
    May 17 at 2:56
  • $\begingroup$ Did you try to write a draft proof with pen and paper? Your proof script did not compile on my computer (V 8.16). I don't think its OK to send snippets with errors. About readability: while and after building a proof, using bullets, tacticals, regrouping rewrites may help a lot. $\endgroup$
    – Pierre Castéran
    May 17 at 6:52
  • $\begingroup$ A last comment about your proof. The third line leads to a state where you would have to prove d * c = d * (b * c). I think you will have to take into account the mathematical intuition of this lemma, before translating its proof into Coq. $\endgroup$
    – Pierre Castéran
    May 17 at 8:47
  • $\begingroup$ You should provide a MWE (stackoverflow.com/help/minimal-reproducible-example), so people can help you. Although the terms permit, I encourage you to register an account and build your reputation in the community. Even just asking interesting questions is a good way to build reputation. $\endgroup$
    – Qinshi Wang
    May 17 at 23:10

1 Answer 1

Reset to default
1
$\begingroup$

Indeed, in your tentative proof, you made a classic mistake: using the existential quantifier introduction tactic too early (i.e. without a sufficient context).

In the script below, I use Zis_gcd_bezoutto get uand v, which are used in the argument of the exists tactic.

Require Import ZArith.
Open Scope Z_scope.
Require Import Znumtheory.

Lemma trial_ex : forall a b c d : Z, (a | b * c) -> Zis_gcd a b d -> (a | c * d).
Proof.
  intros a b c d H1 H2; destruct H1 as [z H3].
  apply Zis_gcd_bezout in H2; destruct H2 as [u v Huv].
  exists (c * u + v * z).  
  (* now easy to complete ...  *)
Improve this answer
$\endgroup$
1
  • $\begingroup$ if only eexists would work here... $\endgroup$
    – cody
    Jun 29 at 19:50

Your Answer

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

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