Why does this verify?

[Shelby Doolittle]

I'm working on a verifier for Metamath proofs, and I've reached the point of implementing disjoint requirements. I tried to make a minimal example of invalid use of disjoint variables, but the primary C metamath implementation seems to accept it. I'm likely doing something wrong, but I can't figure out what.

AFAIU, this file should not verify, but it does:

```

$c true num 0 1 != $.
$v x y $.

num_x $f num x $.
num_y $f num y $.

num_0 $a num 0 $.
num_1 $a num 1 $.

num_zero $a num 0 $.
num_one  $a num 1 $.

${
    $d x y $.
    x_ne_y $a true x != y $.
$}

the1 $p true 0 != 0 $=
    num_zero num_zero x_ne_y $.

```

[Mario Carneiro]

The metamath C implementation is correct in this case, that is a correct theorem. A $d constraint on two variables asserts that the substitutions to those variables have no *variables* in common. A constant expression like "0" has no variables in it, so it is disjoint with itself.

The use of != here is misleading, because a $d on two variables is not asserting that the variables have distinct values, but rather distinct *names*. So for example we need something like that to know that y is free in "A. x x e. y", because if x and y had the same name then the theorem would be asserting "A. x x e. x" which has no free variables in it.

One consequence of this is that for sorts which have binding syntax in them, like the "setvar x" used in "A.  x ph",  it is disastrous to allow constants in, in the sense of $a setvar 0 $., because then you could form the expression "A. 0 x = 0" which in addition to being nonsensical can be used to prove false by circumventing the $d check on a theorem that requires it - e.g. dtru says "-. A. x x = y" but if you substitute 0 for both x and y you get "-. A. 0 0 = 0", and you can similarly substitute 0 for x in a proof of "A. x x = x" to get "A. 0 0 = 0" and hence a contradiction.

[Mario Carneiro]

A variation on your example which should be rejected would be to use `x` twice, like so:

$c true num != $.

$v x y $.

num_x $f num x $.
num_y $f num y $.

${
    $d x y $.
    x_ne_y $a true x != y $.
$}

the1 $p true x != x $=
    num_x num_x x_ne_y $.

--
You received this message because you are subscribed to a topic in the Google Groups "Metamath" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/metamath/Ww0shheWk_U/unsubscribe.
To unsubscribe from this group and all its topics, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/80cb855b-cc66-4d67-9060-98913da6bd56n%40googlegroups.com.

[Shelby Doolittle]

Thanks for the quick and thorough response.

How might I extend this example so it is impossible to prove `0 != 0`? I don't know of anything other than distinct variables that would prevent something like this.

[Glauco]

I'm afraid that your x_ne_y axiom is already too "powerful" and "extending" the example is not gonna help (if you mean "adding" statements)

You might replace x_ne_y with something like 

  0_ne_1 $a true 0 != 1 $.

  1_ne_0 $a true 1 != 0 $.

but, of course, this does not scale at all

Glauco

[Thierry Arnoux]

Hi Shelby,

David has gathered a set of test MM files for verifiers, which you can find here: https://github.com/david-a-wheeler/metamath-test

Glauco added there a set-dist.mm file with a disjoint requirement removed to have a test for that case, but that is in no way minimal like your example, so it might be interesting to add your example to this repository.

BR,
_
Thierry