Zulip Chat Archive

Stream: new members

Topic: names of theorems in 3.6


view this post on Zulip 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.

view this post on Zulip 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].

view this post on Zulip 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.

view this post on Zulip 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 _ ∧ _ ↔ _ ∧ _.

view this post on Zulip Kenny Lau (Jul 13 2020 at 08:16):

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

view this post on Zulip 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?

view this post on Zulip Jalex Stark (Jul 13 2020 at 19:15):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Jalex Stark (Jul 13 2020 at 19:43):

i think tauto is intuitionistic

view this post on Zulip Jalex Stark (Jul 13 2020 at 19:43):

and tauto! is not

view this post on Zulip 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

view this post on Zulip 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: May 14 2021 at 06:16 UTC