chaudhuri / maetning Goto Github PK

@tausbn notes:

A second problem [...] comes from my attempt at creating a goal that would create unboundedly many variables during proof search:

%positive p.
%positive q.

%assume r : (\A y,a,b,w. q(y,a) * q(a,b) * p(b,w)) => (\A z. q(y,z) * p(z,w)).

%refute \E x,y,z. p(x,y) * q(y,z) * p(z,x).

@tausbn notes:

[I]n some cases, saturation doesn't happen (through what appears to be a problem with the implementation).

An example of this is the following:

%negative nat.
%assume nz : nat(z).

% assume ns : \A x. nat(x) => nat(s(x)).
%assume nns : \A x. nat(x) & nat(x) => nat(s(x)).

%pseudo p : \A x. nat(s(s(s(x)))).

%refute \A x. nat(x) + (nat(x) => 0).

Here, the goal is refutable with the axiom ns, but not with the axiom nns. Since the only difference between these is the fact that the latter requires two instances of the same nat(x), this is somewhat worrisome. I imagine this might be some failure of fairness.

• SYN057+1.p
• SYN060+1.p
• SYN065+1.p
• SYN066+1.p
• SYN081+1.p (shows clear looping behavior)

Given

%negative p.

the following two queries succeed:

%refute ~((~(\A x. ~p)) & (\A x. ~p)).

%prove  ~((~(p       )) & (p       )).

Since the former is an instance of the latter, this indicates a bug.
Note that

%prove  ~((~(\A x.  p)) & (\A x.  p)).

succeeds, as does

%prove  ~((~(      ~p)) & (      ~p)).

Thus, both quantification and negation are needed to trigger this bug.

This is currently proved but should not be (checked in as tests/excollapse.mg):

%negative p.
%negative q.

%assume a0 : \E x. p(x).
%assume a1 : \E x. q(x).

%prove \E x. p(x) & q(x).

The oc test needs to be done after the joined term has been instantiated, not before.

This order is of course slower, but it is also correct.

Regression test in tests/bug/occurs_check.mg, courtesy of @tausbn.