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.
$\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
    Commented May 17, 2023 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$ Commented May 17, 2023 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$ Commented May 17, 2023 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$ Commented May 17, 2023 at 23:10

1 Answer 1

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 ...  *)
$\endgroup$
1
  • $\begingroup$ if only eexists would work here... $\endgroup$
    – cody
    Commented Jun 29, 2023 at 19:50

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.