1
$\begingroup$

I am also unfamiliar and trying to solve proofs relative to the topic Relations and Divisibility but I would like to solve such COQ proof theorems. I am not quite sure how to solve proofs like this for example :

Require Import Arith.

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).

Definition congruence (a b c : Z) := (a | (b - c)).
Lemma relations_ex : forall a : Z, equivalence (congruence a).

Proof.

EDIT :

1 goal
a, x, y, H1 : Z
H2 : x - y = H1 * a
______________________________________(1/1)
y - x = -1 * (a * H1)
unfold symmetric, congruence.
    intros x y H.
    unfold congruence in *.
    destruct H as [H1 H2].
    exists (-H1).
    rewrite Z.opp_eq_mul_m1.
    rewrite Z.mul_comm.
    rewrite Z.mul_assoc.
    rewrite Z.mul_comm.
    rewrite <- Z.opp_mul_distr_l.
    reflexivity.
$\endgroup$
1
  • 1
    $\begingroup$ If you want to mark a question as resolved, please click on the little checkmark on the left of an answer. This way it is much more visible and convenient. $\endgroup$
    – Trebor
    May 17, 2023 at 3:01

1 Answer 1

0
$\begingroup$

Here's a framework for getting started.

Lemma relations_ex : forall a : Z, equivalence (congruence a).
Proof.
  intros a.
  repeat split.
  - unfold reflexive, congruence.
    intros x.
    admit.
  - unfold symmetric, congruence.
    intros x y.
    admit.
  - unfold transitive, congruence.
    intros x y z.
    admit.
Admitted.

You'll have to finish the admit. sections.

$\endgroup$
0

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.