-5
$\begingroup$

I am confused. Coq gives the following error:

No subterm matching Hab * a.

What is causing the problem, and how can I solve it?

Definition relation (X Y : Type) := X -> Y -> Prop.
Definition reflexive {X: Type} (R: relation X X) := forall a : X, R a a.
Definition transitive {X: Type} (R: relation X X) := forall a b c : X, (R a b) -> (R b c) -> (R a c).
Definition symmetric {X: Type} (R: relation X X) := forall a b : X, (R a b) -> (R b a).
Definition antisymmetric {X: Type} (R: relation X X) := forall a b : X, (R a b) -> (R b a) -> a = b.
Definition equivalence {X:Type} (R: relation X X) := (reflexive R) /\ (symmetric R) /\ (transitive R).

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

Lemma modelus : forall a b c d : Z, (a | b * c) -> Zis_gcd a b d -> (a | c * d).
Proof.
  intros a b c d [Hab Hac] [H1 H2].
  unfold Z.divide in *.
  destruct H1 as [H3 H1].
  destruct H2 as [H4 H2].
  exists (c * H3 + b * H4).
  rewrite Z.mul_add_distr_r.
  rewrite <- Hac.
  rewrite Z.mul_assoc.
  rewrite <- H1.
  rewrite <- H2.
  reflexivity.
Improve this question
$\endgroup$
4
  • $\begingroup$ Isn't the error message self-explanatory? In doing rewrite<- Hac., you're asking to replace all occurrences of Hab * a in the goal by b * c. But there are no occurrences of Hab * a in the goal. $\endgroup$
    – mudri
    May 15 at 21:33
  • $\begingroup$ what is the mathematical argument you want to follow to do this proof in Coq? $\endgroup$
    – Lolo
    May 16 at 0:01
  • $\begingroup$ Please understand that the edit history is always available for everyone to see. You may leave a question as is even if it is resolved for you, in case it receives future answers and/or helps other visitors. If you have specific reasons that you want to remove some information from the question, please let me know. $\endgroup$
    – Trebor ♦
    May 17 at 17:04
  • $\begingroup$ This is just a problem with the left-associativity of the operator * in Coq. The term c * x * a is read (c * x) * a and not c * (x * a). You may use the associativity of multiplication before your rewrite. P.S. Why calling Haban integer ? $\endgroup$
    – Pierre Castéran
    May 18 at 14:20

0

Reset to default

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.

Browse other questions tagged or ask your own question.