Equational reasoning in Coq

Question

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!

Answer 1

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.

Answer 2

In order to prove this by hand, let's use the method of analytic tableaux for first-order logic without unification.

This is a method for classical first-order logic, so it won't necessarily give us a proof that will go through in intuitionistic first-order logic, but the theorem we're asked to show is simple enough that we can examine the proof and see if we used any reasoning that's not constructively valid.

In addition to the rules shown on the Wikipedia page, I permit substitution of equal ground terms, so if $s$ and $t$ are both closed terms (i.e. no free variables) and $s = t$, then I can replace $s$ with $t$ textually in any of my formulas. (I will only need the ability to replace equals with equals in closed formulas, but the tableau calculus will still work if you allow substitution of ground terms in open formulas too).

• Premise 1: $ [\forall x y](f(x, g(x, y)) = x) $
• Premise 2: $ [\forall x y](g(x, f(x, y)) = y) $
• Negated Goal: $f(c, c) \neq c$ where $c$ is a constant symbol.
• From premise 1, $f(c, g(c, c)) = c$. From here we can see the trick, we need to simplify the second argument of $f$ eventually.
• From premise 1, $f(c, g(c, f(c, c)) = c$.
• From premise 2, $g(c, f(c, c)) = c$.
• By substitution of equal ground terms, $f(c, c) = c$, which contradicts our negated goal.

This proof ended up going through just by instantiating axioms and rewriting ground terms, which is intuitionistically valid, so let's translate it into Coq.

You can emulate forward reasoning in Coq with assertions and liberal use of tactics like easy, auto, and intuition. It's not great but it does work.

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.
  assert (L1 : forall z, f z (g z (f z z)) = z) by (intro z; pose proof ax_f as H; easy).
  assert (L2 : forall z, g z (f z z) = z) by (intro z; pose proof ax_g as H; easy).
  intro x.
  pose proof L1 x as L1x.
  pose proof L2 x as L2x.
  rewrite L2x in L1x.
  easy.
Qed.
```