Zulip Chat Archive

Stream: new members

Topic: names of theorems in 3.6

Michael Beeson (Jul 13 2020 at 07:35):

section 3.6 of Theorem Proving in Lean has a bunch of propositional identities and says "you can use them in your proofs".
So where can I find a list of names of these theorems, as I will need their names to use them, right?
For example I have h: P->Q and h2 : P', where P' is almost the same as P but two conjuncts somewhere deep inside
have the wrong order. So I want to rewrite it using p \and q = q \and p.

Rob Lewis (Jul 13 2020 at 07:42):

You can use rw [and_comm] at h2. If there are other ands around you might need to give it more information, e.g. rw [and_comm p q].

Jasmin Blanchette (Jul 13 2020 at 07:47):

That solves the specific example Michael gave, but not the general problem that the identities are not named.

Rob Lewis (Jul 13 2020 at 07:53):

I don't know why they're not named there. Maybe guessing them is good practice to learn the mathlib naming conventions? You can find a lot of them with e.g. #find _ ∧ _ ↔ _ ∧ _.

Kenny Lau (Jul 13 2020 at 08:16):


Michael Beeson (Jul 13 2020 at 19:11):

I tried rw [and_comm] at h2 as suggested. It seems you do need to supply arguments to and_comm, which has a universally quantified type. The conjunction I want to commute is inside a quantifier so I used simp_rw. But one of the propositions I want to commute mentions the quantified variable u. And I get the error message "unknown variable u". What now?

Jalex Stark (Jul 13 2020 at 19:15):

i don't have advice, but I probably would if you posted code

Jalex Stark (Jul 13 2020 at 19:16):

when I get in situations where I want to do things like rw add_comm, I try to reduce to a subproblem that tauto can solve by itself

Michael Beeson (Jul 13 2020 at 19:29):

tauto is not available as I am working with intuitionistic logic. There is ifinish but it usually fails or times out. I understand that I should post a working example if I want specific advice. Maybe I will do that later. For now I'm just going to tear the formulas down and get on with the proof.

Jalex Stark (Jul 13 2020 at 19:43):

i think tauto is intuitionistic

Jalex Stark (Jul 13 2020 at 19:43):

and tauto! is not

Jalex Stark (Jul 13 2020 at 19:43):

tactic#tautology says that tauto! uses LEM and implies that tauto does not, but maybe you're worried about something else

Jalex Stark (Jul 13 2020 at 19:46):

if "tear the formulas down" means "get rid of the quantifiers with e.g. intro, function application", then I agree that's a fine way to proceed

Last updated: Dec 20 2023 at 11:08 UTC