Zulip Chat Archive

Stream: new members

Topic: Using tfae theorem


view this post on Zulip Paul Rowe (Aug 14 2020 at 14:48):

I'm having trouble finding a simple explanation of how to use a tfae theorem. I have a theorem that basically looks like this

theorem thm1 : tfae [ a b c ] := sorry

(I have completed the proof.) I now need to use the fact that b -> c in the proof of another theorem. How do I access this fact from thm1?

I have run across some discussion of tfae.out but I can't immediately figure out how it works.

view this post on Zulip Mario Carneiro (Aug 14 2020 at 15:00):

I think tfae.out thm1 1 2 should be a proof of b -> c

view this post on Zulip Paul Rowe (Aug 14 2020 at 15:05):

That's what I tried first, but I get an error.

exact tactic failed, type mismatch, given expression has type
  true
but is expected to have type
  as_true (1 < [church_rosser ?m_2, confluent ?m_2, semiconfluent ?m_2].length)

(In this case, my a, b, c correspond to the properties church_rosser, confluent, semiconfluent.)

view this post on Zulip Mario Carneiro (Aug 14 2020 at 15:07):

Actually, try this version instead:

namespace list
theorem tfae.out' {l} (h : tfae l) (n₁ n₂) {a b}
  (h₁ : list.nth l n₁ = some a . control_laws_tac)
  (h₂ : list.nth l n₂ = some b . control_laws_tac) :
  a  b :=
h _ (list.nth_mem h₁) _ (list.nth_mem h₂)
end list

example {a b c} (h : [a, b, c].tfae) : true :=
begin
  have := h.out' 1 2,
end

view this post on Zulip Mario Carneiro (Aug 14 2020 at 15:08):

that error is a bit odd. You might have to specify ?m_2 (it should probably be an explicit argument to the theorem) but it should reduce even without that

view this post on Zulip Paul Rowe (Aug 14 2020 at 15:13):

Sorry. I'm still a newbie. How do I use that new version? Is that included in some library? If not, I am having trouble putting it into my file to use.

view this post on Zulip Mario Carneiro (Aug 14 2020 at 15:14):

I wrote it just now. You should just be able to put it at the top of your file

view this post on Zulip Mario Carneiro (Aug 14 2020 at 15:14):

make sure it's not in a namespace of yours

view this post on Zulip Paul Rowe (Aug 14 2020 at 15:23):

That works! I did end up having to make the implicit variable an explicit argument to the theorem. It didn't work otherwise. But that makes sense to me in my context. Thanks for the help!


Last updated: May 16 2021 at 21:11 UTC