Fix test_predtest's idea of what weak refutation means.

I'd initially supposed that predicate_refuted_by(..., true) ought to
say that "A refutes B" means "non-falsity of A implies non-truth of B".
But it seems better to define it as "truth of A implies non-truth of B".
This is more useful in the current system, slightly easier to prove,
and in closer correspondence to the existing code behavior.

With this change, test_predtest no longer claims that any existing
test cases show false proof reports, though there still are cases
where we could prove something and fail to.

Discussion: https://postgr.es/m/5983.1520487191@sss.pgh.pa.us

Author: tglsfdc

src/test/modules/test_predtest/expected/test_predtest.out

@@ -119,7 +119,6 @@ select * from test_predtest($$
 select x is not true, x
 from booleans
 $$);
-WARNING:  weak_refuted_by result is incorrect
 -[ RECORD 1 ]-----+--
 strong_implied_by | f
 weak_implied_by   | f
@@ -128,7 +127,7 @@ weak_refuted_by   | t
 s_i_holds         | f
 w_i_holds         | f
 s_r_holds         | t
-w_r_holds         | f
+w_r_holds         | t
 
 select * from test_predtest($$
 select x, x is not true
@@ -176,7 +175,6 @@ select * from test_predtest($$
 select x is unknown, x
 from booleans
 $$);
-WARNING:  weak_refuted_by result is incorrect
 -[ RECORD 1 ]-----+--
 strong_implied_by | f
 weak_implied_by   | f
@@ -185,7 +183,7 @@ weak_refuted_by   | t
 s_i_holds         | f
 w_i_holds         | f
 s_r_holds         | t
-w_r_holds         | f
+w_r_holds         | t
 
 select * from test_predtest($$
 select x, x is unknown
@@ -214,7 +212,7 @@ weak_refuted_by   | f
 s_i_holds         | f
 w_i_holds         | f
 s_r_holds         | t
-w_r_holds         | f
+w_r_holds         | t
 
 select * from test_predtest($$
 select x, x is null
@@ -650,7 +648,7 @@ weak_refuted_by   | f
 s_i_holds         | f
 w_i_holds         | f
 s_r_holds         | t
-w_r_holds         | f
+w_r_holds         | t
 
 select * from test_predtest($$
 select x is null, int4lt(x,8)
@@ -664,7 +662,7 @@ weak_refuted_by   | f
 s_i_holds         | f
 w_i_holds         | f
 s_r_holds         | t
-w_r_holds         | f
+w_r_holds         | t
 
 select * from test_predtest($$
 select x is not null, x < 'foo'

src/test/modules/test_predtest/test_predtest.c

@@ -104,14 +104,18 @@ test_predtest(PG_FUNCTION_ARGS)
 			c2 = 'f';
 
 		/* Check for violations of various proof conditions */
+
+		/* strong implication: truth of c2 implies truth of c1 */
 		if (c2 == 't' && c1 != 't')
 			s_i_holds = false;
+		/* weak implication: non-falsity of c2 implies non-falsity of c1 */
 		if (c2 != 'f' && c1 == 'f')
 			w_i_holds = false;
+		/* strong refutation: truth of c2 implies falsity of c1 */
 		if (c2 == 't' && c1 != 'f')
 			s_r_holds = false;
-		/* XXX is this the correct definition for weak refutation? */
-		if (c2 != 'f' && c1 == 't')
+		/* weak refutation: truth of c2 implies non-truth of c1 */
+		if (c2 == 't' && c1 == 't')
 			w_r_holds = false;
 	}