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 $.
On Thu, Dec 29, 2022 at 7:15 PM Mario Carneiro <[email protected]> wrote:
> 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.
>
> On Thursday, December 29, 2022 at 7:03:37 PM UTC-5 [email protected]
> wrote:
>
>> 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 $.
>> ```
>>
> --
> 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
> [email protected].
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/metamath/80cb855b-cc66-4d67-9060-98913da6bd56n%40googlegroups.com
> <https://groups.google.com/d/msgid/metamath/80cb855b-cc66-4d67-9060-98913da6bd56n%40googlegroups.com?utm_medium=email&utm_source=footer>
> .
>
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CAFXXJSt-iFcNmZxud54dKS8XfpAi_S5NNbZLCad6a%3DcAhoo8xw%40mail.gmail.com.
