Forward type proofs using fix-assume-show layout

Stream: new members

[Ayush Agrawal]

Hi guys! I was trying out this 'Structured' proof from hitchhikers_guide_Lean book.

lemma fst_of_two_props : ∀a b : Prop, a → b → a :=
fix a b : Prop,
assume ha : a,
assume hb : b,
show a, from
ha

But it is not able to recognize fix. Which library should I import to make it work? Thanks in advance!

[Kevin Buzzard]

fix is not a thing in Lean AFAIK. Maybe it's something specific to the Hitchhiker's guide book?

[Kevin Buzzard]

Just change it to assume or λ

[Ayush Agrawal]

Thanks @Kevin Buzzard for the info! I thought that the book is purely based on Lean.

[Reid Barton]

https://raw.githubusercontent.com/blanchette/logical_verification_2020/master/hitchhikers_guide.pdf page 33 (43)

[Reid Barton]

aha https://raw.githubusercontent.com/blanchette/logical_verification_2020/master/lean/lovelib.lean

[Reid Barton]

So basically fix is a lambda--I guess they wanted a better name than "lambda" without the propositional connotations of "assume"

[Ayush Agrawal]

Oh! now getting it. Thanks @Reid Barton

[Anne Baanen]

See also this discussion on introducing fix