Using tfae theorem

Stream: new members

[Paul Rowe]

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.

[Mario Carneiro]

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

[Paul Rowe]

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.)

[Mario Carneiro]

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

[Mario Carneiro]

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

[Paul Rowe]

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.

[Mario Carneiro]

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

[Mario Carneiro]

make sure it's not in a namespace of yours

[Paul Rowe]

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!