partialidx: prove implication for comparisons with two variables

[mgartner]

This commit adds support for proving partial index predicates are
implied by query filters when they contain comparison expressions with
two variables and they are not identical expressions.

Below are some examples where the left expression implies (=>) the right
expression. The right is guaranteed to contain the left despite both
expressions having no constant values.

a > b  =>  a >= b
a = b  =>  a >= b
b < a  =>  a >= b
a > b  =>  a != b

Release note: None

[cockroach-teamcity]

This change is 

[RaduBerinde]

Reviewable status: complete! 0 of 0 LGTMs obtained (waiting on @mgartner)

---

pkg/sql/opt/partialidx/implicator.go, line 541 at r1 (raw file):

	predLeft := pred.Child(0).(*memo.VariableExpr)
	predRight := pred.Child(1).(*memo.VariableExpr)

This would be a lot easier to process if we had a function like:

implies := func(left, right opt.ColumnID, op opt.Operator, pred opt.ScalarExpr)

and call it twice: implies(a,b,op,pred) and implies(b, a, inverseOp, pred)

[mgartner]

Reviewable status: complete! 0 of 0 LGTMs obtained (waiting on @RaduBerinde)

---

pkg/sql/opt/partialidx/implicator.go, line 541 at r1 (raw file):

Previously, RaduBerinde wrote…

This would be a lot easier to process if we had a function like:

implies := func(left, right opt.ColumnID, op opt.Operator, pred opt.ScalarExpr)

and call it twice: implies(a,b,op,pred) and implies(b, a, inverseOp, pred)

Great idea. I think it's cleaner now 👍

[RaduBerinde]

Reviewable status: complete! 0 of 0 LGTMs obtained (waiting on @mgartner and @RaduBerinde)

---

pkg/sql/opt/partialidx/implicator.go, line 533 at r2 (raw file):

	}

	inverseOp := func(op opt.Operator) opt.Operator {

[nit] the "inverse" of EQ feels like it would be NE :) Maybe name it commutedOp

---

pkg/sql/opt/partialidx/implicator.go, line 584 at r2 (raw file):

	eRightCol := e.Child(1).(*memo.VariableExpr).Col
	if impliesPred(eLeftCol, eRightCol, e.Op()) || impliesPred(eRightCol, eLeftCol, inverseOp(e.Op())) {
		// If the operators are inverses of each other, then they are equivalent

A little confused by this. What are we trying to do here? Determine when pred is exactly equivalent to e? I'm not sure why we're looking at the inverseOp?
I'd expect to use a second flag returned by impliesPred that indicates if we were in one of the "loose" cases (under switch op)

---

pkg/sql/opt/partialidx/testdata/implicator/atom, line 227 at r2 (raw file):

----
true
└── remaining filters: @1 > @2

Add some trivial tests with @1 >= @2 => @1 >= @2 and @2 <= @1 => @1 >= @2 to make sure we don't have remaining filters.

[mgartner]

Reviewable status: complete! 0 of 0 LGTMs obtained (waiting on @RaduBerinde)

---

pkg/sql/opt/partialidx/implicator.go, line 533 at r2 (raw file):

Previously, RaduBerinde wrote…

[nit] the "inverse" of EQ feels like it would be NE :) Maybe name it commutedOp

Good point. Done.

---

pkg/sql/opt/partialidx/implicator.go, line 584 at r2 (raw file):

Previously, RaduBerinde wrote…

A little confused by this. What are we trying to do here? Determine when pred is exactly equivalent to e? I'm not sure why we're looking at the inverseOp?
I'd expect to use a second flag returned by impliesPred that indicates if we were in one of the "loose" cases (under switch op)

The only cases it's not "loose" is when the operators are equal or commuted-equal (>= and <=). I didn't need to cover the e.Op() == pred.Op()case because that's handled outside this function by checking pointer equality, but I think that made this confusing. I tried to put this intoimpliesPredbut it complicated things more. I've made the comment more clear and added thee.Op() == pred.Op()` case for clarity. Let me know what you think.

---

pkg/sql/opt/partialidx/testdata/implicator/atom, line 227 at r2 (raw file):

Previously, RaduBerinde wrote…

Add some trivial tests with @1 >= @2 => @1 >= @2 and @2 <= @1 => @1 >= @2 to make sure we don't have remaining filters.

Good catch! I reorganized the tests and made them more exhaustive.

[RaduBerinde]

Reviewable status: complete! 1 of 0 LGTMs obtained (waiting on @mgartner)

---

pkg/sql/opt/partialidx/implicator.go, line 584 at r2 (raw file):

Previously, mgartner (Marcus Gartner) wrote…

The only cases it's not "loose" is when the operators are equal or commuted-equal (>= and <=). I didn't need to cover the e.Op() == pred.Op()case because that's handled outside this function by checking pointer equality, but I think that made this confusing. I tried to put this intoimpliesPredbut it complicated things more. I've made the comment more clear and added thee.Op() == pred.Op()` case for clarity. Let me know what you think.

Looks good, thanks!

[mgartner]

bors r=RaduBerinde

[craig]

Build succeeded:

• GitHub CI (Cockroach)