# Equational reasoning in Coq

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!

• 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”. Jun 12 at 15:59
• 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. Jun 12 at 16:04
• @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? Jun 12 at 16:13

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

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



f x x = x

Both are of the form f x ? = x.
You also have another axiom stating an equality with x.
• 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". Jun 12 at 16:14