0
$\begingroup$

I've been doing some exercises on Coq, and have stuck for the next problem:

Let T: Set with 2 operations f, g on it. Suppose that these operations satisfy the following relations:

  1. f x (g x y) = x
  2. g x (f x y) = x

Verify that forall (x: T), f x x = x.

So I've declared things:

Parameter T : Set.
Parameter f g: T -> T -> T.

Axiom ax_f: forall (x y: T), f x (g x y) = x.
Axiom ax_g: forall (x y: T), g x (f x y) = x.

Lemma l: forall (x: T), f x x = x.
Proof. intros. assert (Hf := ax_f x x). assert (Hg := ax_g x x).

But then I don't know what to do. I've tried rewriting the statement f x x = x via the axioms above, but that hadn't helped me. The only way to solve it that I found was the asserting g x x = x. With this in context, the problem solves quickly:

assert (g x x = x) as G.
2:{rewrite <- G at 2. assumption. }

But as one might notice, a new goal g x x = x was created, and thus nothing really changed so far. At this point, I don't really get how one solves this.

Can anyone give a hint on this? Thanks in advance!

Improve this question
$\endgroup$
3
  • 1
    $\begingroup$ As for a hint, have you thought about how to solve it informally with pen and paper? You have figured out that if you can prove g x x = x then you can prove f x x = x, but now you have to figure out how to “catch your tail”. $\endgroup$
    – Jason Rute
    Jun 12, 2022 at 15:59
  • 2
    $\begingroup$ I hesitate to give you more of a hint than that, but I and many others find that you can miss the forest for the trees when formalizing, and it is better to take a step back first and solve the problem informally before diving in to formalize it. $\endgroup$
    – Jason Rute
    Jun 12, 2022 at 16:04
  • $\begingroup$ @JasonRute thanks for the hint! I was sitting with pen and paper before and this didn't help me, I was just burying myself into the symbolic things. After a bit of time, I've sat back and got the solution. Now I find this question pretty silly, should I consider removing it? $\endgroup$
    – Paul Snopov
    Jun 12, 2022 at 16:13

1 Answer 1

Reset to default
2
$\begingroup$

This is a hint. Note that you have the following axiom:

Axiom ax_f: forall (x y: T), f x (g x y) = x.

and your goal is

f x x = x

Both are of the form f x ? = x.

You also have another axiom stating an equality with x.

Like Jason said, this is really a math question and you should try to figure it out on paper before moving to Coq.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Thanks! Yeah, indeed, this not is pretty obvious, but for some reason I haven't came up with a thought that " y := f x x is the thing I need". $\endgroup$
    – Paul Snopov
    Jun 12, 2022 at 16:14

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.