1
$\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!

$\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
    Commented 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
    Commented 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$ Commented Jun 12, 2022 at 16:13

2 Answers 2

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.

$\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$ Commented Jun 12, 2022 at 16:14
1
$\begingroup$

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.
```
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.