names of theorems in 3.6

Stream: new members

[Michael Beeson]

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]

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]

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

[Rob Lewis]

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]

https://github.com/leanprover-community/leanprover-community.github.io/pull/93

[Michael Beeson]

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]

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

[Jalex Stark]

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]

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]

i think tauto is intuitionistic

[Jalex Stark]

and tauto! is not

[Jalex Stark]

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

[Jalex Stark]

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