contrapos_final without tactics?

Stream: new members

[Joseph Corneli]

I'm looking at https://github.com/kbuzzard/xena/blob/master/lean_together/contrapos_final.lean

The question at the end is:

theorem both_ways (P Q : Prop) : (P → Q) ↔ (¬ Q → ¬ P) := by ??

Here's a sensible seeming answer with tactics:

theorem both_ways (P Q : Prop) : (P → Q) ↔ (¬ Q → ¬ P) :=
begin
 split,
 apply contrapositive,
 apply other_way
end

I'm wondering how to do it without tactics. I got started this way but this doesn't work.

theorem both_ways_again (P Q : Prop) : (P → Q) ↔ (¬ Q → ¬ P) :=
iff.intro (assume h1 : (P → Q), have (¬ Q → ¬ P), from contrapositive h1)
          (assume h2 : (¬ Q → ¬ P), have (P → Q), from other_way h2)

[Chris Hughes]

You want show instead of have I think.

[Rob Lewis]

The (P Q : Prop) arguments in contrapositive and other_way should be implicit, or you should put in placeholders when you use them.

[Rob Lewis]

Also what Chris says.

[Joseph Corneli]

OK, show is a definite, thanks.

Revision:

theorem both_ways' {P Q : Prop} : (P → Q) ↔ (¬ Q → ¬ P) :=
iff.intro (assume h1 : (P → Q), show (¬ Q → ¬ P), from (contrapositive h1))
          (assume h2 : (¬ Q → ¬ P), show (P → Q), from (other_way h2))

I've modified the arguments for the lemmas be implicit, but Lean complains that it can't synthesise the placeholder. I can't either!

don't know how to synthesize placeholder
context:
P Q : Prop
⊢ Type ?

[Joseph Corneli]

oh, wait a second, now the server has refreshed and it seems to be fine.

[Joseph Corneli]

:tada: