Feature suggestion to support duality and similar things

[vporton]

I am a new user of Lean (in fact I have just read the tutorial, but have not yet installed the program). The feature to support duality (such as categorical duality or order duality) is not described in the tutorial, so I assume it is missing in the software.

"rewrite" tactic should be extended to use hints from "hint databases" (an extendable lists of rewrite rules), accessible by a name (such as $db below).

I propose the following syntax:

rewrite $db

where "db" is the name of a hints database.

We could also mix single equalities (like "id") with databases (like "db1", "db2"):

rewrite [$db1, id, $db2]

One example where this may be useful is order-theoretic and category-theoretic duality:

theorem meet_dual: forall order x y, meet order x y = (join (dual order) x y) := sorry

Then to add a new hint to a database, we probably could introduce syntax like this (we should yet think about the exact syntax, I give here only a rough idea):

hint rewrite meet_dual: order_duality

Among the above I suggest an additional feature:

Pass (probably as a string) the name of a hints database to tactic scripts.

This would allow for example sharing the same code for dealing with order theoretic equality and category theoretic duality. (I could show an example that these two dualities should not be mixed in one database, but margins are too small.)

[vporton]

Moreover we may need a variation to repeat rewrite tactic, to apply every hint in the database at most once to every subexpression of the goal (so that it is not repeated infinitely transforming meet into dual join, then join into dual of dual meet, etc.)

I am not expert, but here is my idea for further development.

[avigad]

Thank you for the suggestions. Leonardo de Moura and Daniel Selsam are working on automated procedures for Lean, including a general theorem prover (blast) and a simplifier (simp). It may take a few months before they are fully functional, but when they are in place, we should determine whether they can be used in the way you describe.

[vporton]

In library/algebra/complete_lattice.lean I see theorem knaster_tarski and theorem knaster_tarski_dual repeating essentially the same proof twice. It is where my idea should simplify things.

[vporton]

It looks for me that blast and simp are unrelated with my feature suggestion:

blast and simp are about complex computations, but mine is about a simple idea which however requires to add new variables (probably at C++ level).

Please discuss particular syntax and semantics to use to implement my idea. We should do it right from the first time.

[avigad]

Dear Victor, Thank you for your suggestions. When the simplifier is available, we will be able to simplify expressions with databases of rewrite rules. Please, let us wait until then to see if it provides the functionality you want.

[vporton]

It would be also helpful to "transform" theorems by applying a tactic:

theorem t1: forall a,b: meet a b = meet b a := sorry would be transformed into the dual theorem forall a,b: join a b = join b a by:

theorem t2 := dual(t1).

I am not sure however that this does not contradict proof irrelevance.

The same could be done also with definitions like the following:

definition meet := dual(@join)

Just a rough idea, syntax may be different.

Please comment if my idea is easy enough to implement without messing things in a complex way.

[avigad]

I think it will be possible to do something like this in a nice way. Leo is working on a way to use Lean itself as a programming language that can implement tactics. Given a theorem T, we want to transform that statement by replacing objects by their duals, and then prove the result by instantiating T to the dual lattice. That will be a nice test for the framework.

Leo has just started working on this, and he is doing a major rewrite of the system, so it will be a few months before we can try it. But it is a good goal to keep in mind.

[leodemoura]

This feature can be implemented by users using the new tactic framework available in the lean3 branch.