TITLE: Equational reasoning in Coq
QUESTION [0 upvotes]: 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:

f x (g x y) = x
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!

REPLY [2 votes]: 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.
{"set_name": "stack_exchange", "score": 0, "question_id": 1514}