I've been doing some exercises on Coq, and have stuck for the next problem:
Let
T: Set
with 2 operationsf
,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!
g x x = x
then you can provef x x = x
, but now you have to figure out how to “catch your tail”. $\endgroup$