Excluding lemmas from library_search

Stream: new members

[ebp]

Hi all!

I was wondering what is the best way to omit certain lemmas from the library. I would like students to give proofs to relatively simple statements from propositional logic, such as p \or q \imp q \or p. I want them to give all the steps you would do in an ordinary deduction proof, with all the steps being "justifiable" by library_search. However, the problem is that library_search can already justify the statement p \or q \imp q \or p itself, which is not preferable in this situation.

I could imagine that for example removing the particular unwanted lemmas from the library could work, but I can also imagine that this ruins the logical structure of the library and thereby giving an error to mathlib as a whole.

Hope to hear some ideas on this!

[Eric Wieser]

Do you want to omit the lemmas from the library completely, or just from the search results?

[Eric Wieser]

Note that docs#or.symm is part of Lean itself, and appears long before library_search even exists

[ebp]

I want to omit them from the collection that is used by library_search. So that the code

example (p q : Prop) : p ∨ q → q ∨ p := by library_search

is not recognized as a correct proof.

[Johan Commelin]

One option might be to build a tiny library yourself

namespace propositional_logic_course

inductive or (P Q : Prop) : Prop
| left (p : P) := or P Q
| right (q :Q) := or P Q

-- some basic lemma that students are allowed to use
lemma foobar : ... etc ...

end propositional_logic_course

But I'm not sure if you can reuse the nice notation ∨ if you do this.

[Johan Commelin]

The benefit is that you can be sure that students can only use the helper lemmas that you've provided. (Unless the prove by themselves that the new definition is equivalent to the one in mathlib :rofl: Then they can rw it to the mathlib def, and use the whole library.)

[Kyle Miller]

If you want to do the opposite, you could consider hand-curating lemmas and using tactic#solve_by_elim directly (which is what library_search is essentially a wrapper around), but that doesn't give you a suggestion.

[Kyle Miller]

It might actually work doing library_search [-offending_lemma], but I haven't checked.

[Eric Wieser]

If you don't want library_search to find or.symm, then what type of thing _do_ you want it to find?

[ebp]

I want library_search to find for example or.inr and things like that; so the most fundamental deduction rules. Building a separate library might be an idea. What is the best way to use library_search to such a hand made library?

I will try the [-offending_lemma] idea as well!

[Johan Commelin]

library_search should automatically work on your hand made library.

[Kyle Miller]

It looks like library_search will always use the entire library, so [-offending_lemma] likely won't work.

It looks like library_search has the option to take simp sets, but I'm not sure you can limit it to only using lemmas from a simp set. If that could work, that might be a nice way to say "do a library search using this particular collection of lemmas".

[Patrick Massot]

The solution I use is to hide the existence of library_search

[ebp]

What is the way to include the hand-made library in the existing library in such a way that library_search still works, but only on the specific library? Library_search itself is defined inside mathlib so removing mathlib and replacing it by the hand-made library will not work either.

[Johan Commelin]

If you give your own definition of or then mathlibs results don't apply to it. So library_search will not find them.

[Kyle Miller]

Johan Commelin said:

But I'm not sure if you can reuse the nice notation ∨ if you do this.

If you use local notation it'll override the pre-existing one completely.

It seems like the "right" way would be to modify suggest_core so that library_search with simp_set_names... causes it to not use the entire library. It already has this ability to use simp sets I believe, and I'm not sure what the point is if it's going to use the entire library anyway...

[Eric Wieser]

ebp said:

I want library_search to find for example or.inr and things like that; so the most fundamental deduction rules.

I think that just amounts to show_term {constructor}?

[Kevin Buzzard]

If my understanding is correct, the motivation behind the question is that @ebp only wants to allow students to use certain lemmas, and I suspect the total number of allowable lemmas is very small (e.g. or elimination, or introduction, and elimination, and introduction etc). So why not just explicitly list the lemmas which the students are allowed to use and give them that list, and not tell them about library_search at all? I have done this before: I introduce a new concept to the class (i.e. a definition from mathlib) and then just give them an incomplete but totally explicit API for the concept and say "using these theorems, whose proofs you can assume, go on to prove the following things".

[Kevin Buzzard]

The alternative approach which I've tried (make a new copy of the definition yourself) typically works less well because you get notation clashes (unless you use weird notation), declaration name clashes (unless you call things mygroup or group' -- even using namespaces like xena.group doesn't work too well), and general confusion (none of the tactics work e.g. tauto wouldn't work for home-rolled or etc).

[Eric Wieser]

I assume that working in a prelude probably does more harm than good - it will remove any problems with namespace or notation clashes, but you'll have exactly nothing to start from (which both means your students can't cheat, but also means they get a lot of missing nice things)

[Kevin Buzzard]

I've also tried this and it's even worse because far more things are broken/unavailable than you might imagine.

[Eric Wieser]

I guess you probably lose widgets?

[Kevin Buzzard]

Maybe for stuff like or it might be OK, who knows.

[Kevin Buzzard]

Yes you definitely lose widgets (at least IIRC), and also the tada emoji when you've finished a proof.

[Kevin Buzzard]

This alone is a good reason not to do it ;-)

[ebp]

Sorry for the late response; didn't have any time to work on this the past days.

I don't want to bother the students with the precise formulation of all the definitions and deduction rules from Lean, this is beyond the scope of the level of logic I'll be using this for. Using library_search gives the possibility to write proofs easily, but in its current state it makes things too easy. As it probably looks like it is not possible to remove certain rules from the library, I have to think about another way.

[Kevin Buzzard]

If the goal is "prove these lemmas in a certain way" and a student just looks them up in the library and hence proves them the wrong way, then surely they don't get the points?

[Kevin Buzzard]

You talk about an "ordinary deduction proof" but what does that even mean? If the formal definition of this is "you can use only the following 15 facts" then you can just tell them the facts and say they can only use those, or just write your own tactic which is "library search but it only knows these 15 theorems", which would be quite easy to do.

[Kevin Buzzard]

In the first problem sheet of the course I teach, I even tell the students that every single goal can be solved with the tauto! tactic but that the object of the exercise is not to solve the goals, but to learn the basic tactics which they'll need in all the other sheets.

[ebp]

"Writing your own tactic which is library_search but it only knows these 15 theorems" sounds like the most probable solution to the problem. I will try and look into this. The thing is that I only use Lean as some kind of "back end" which is not visible for the user. Maybe I have not explained the situation well enough yet here!

[Kevin Buzzard]

When I wrote the natural number game (a website with lean as a back end) I found that the rw tactic was not exactly what I wanted, but I asked for help here and was shown how to modify the tactic slightly so that it behaved the way I wanted it to behave.