Zulip Chat Archive

Stream: new members

Topic: force lambda reduction


Michael Beeson (Mar 29 2021 at 04:50):

I have this expression in a current proof:

h5:  (x_1 : M), ¬¬(λ (k : M), k  𝔽  x  k  ¬¬x  SSC U) x_1

and I want to force it to be lambda-reduced (without using classical logic) i.e., k will be replaced by x_1 and the lambda erased.

Yury G. Kudryashov (Mar 29 2021 at 04:53):

Try simp only.

Yury G. Kudryashov (Mar 29 2021 at 04:53):

with no lemmas

Yury G. Kudryashov (Mar 29 2021 at 04:54):

This is counter-intuitive but we have no dedicated tactic yet.

Michael Beeson (Mar 29 2021 at 04:59):

Thanks, that appeared to work. (Only when I finish the proof can I check if it really didn't use classical axioms, but it looks good.)

Michael Beeson (Mar 29 2021 at 05:00):

Is there a way to manually rename the bound variable x_1 (to something more pleasant to read)?

Johan Commelin (Mar 29 2021 at 05:06):

tactic#rename

Yury G. Kudryashov (Mar 29 2021 at 05:48):

replace h5 := λ x, h5 x?

Mario Carneiro (Mar 29 2021 at 09:15):

I usually use dsimp only to do "just beta reduction"


Last updated: Dec 20 2023 at 11:08 UTC