Zulip Chat Archive

Stream: new members

Topic: applying a function to itself


Kenny Lau (Jun 03 2020 at 15:37):

meta def foo : Type :=
foo  foo

#check λ f g : foo, f g

Kenny Lau (Jun 03 2020 at 15:37):

type mismatch at application
  f g
term
  g
has type
  foo
but is expected to have type
  [foo._main]

Kenny Lau (Jun 03 2020 at 15:37):

how do I make it work?

Kenny Lau (Jun 03 2020 at 15:37):

I want to apply a function to itself

Kenny Lau (Jun 03 2020 at 15:37):

why does foo have no equational lemma?

Pedro Minicz (Jun 06 2020 at 04:52):

I am not familiar with meta definitions in Lean, but meta def foo : Type := foo → foo seems to be a hack-y attempt at an untyped identity function.

Pedro Minicz (Jun 06 2020 at 04:56):

You cannot apply a strictly one argument function to itself, because that necessarily would lead to a type mismatch. That is, you would have α → b and α = α → b, so α would have to be a fix-point ((... → b) → b) → b, which is not possible, because terms themselves can't be infinite.

Pedro Minicz (Jun 06 2020 at 05:02):

You can, however, (kind-of) apply an identify function to itself.

def id' {α : Type*} : α  α := λ x, x

id is a function of two arguments, the first of which is implicit, so Lean will try to figure it out for us if it can.

#check id' id'

Lean will figure out that the type α for the leftmost id' is Π {α : Type*}, α → α. You can make implicit arguments explicit using @:

#check @id' (Π {α : Type*}, α  α) @id'

Pedro Minicz (Jun 06 2020 at 05:03):

Another example of interest:

variable β : Type*

#check @id' (β  β) id'

Kenny Lau (Jun 10 2020 at 14:05):

@Mario Carneiro

Mario Carneiro (Jun 10 2020 at 14:06):

hi

Mario Carneiro (Jun 10 2020 at 14:06):

it's not going to work

Kenny Lau (Jun 10 2020 at 14:06):

why not

Mario Carneiro (Jun 10 2020 at 14:06):

because this would make the typechecker diverge

Kenny Lau (Jun 10 2020 at 14:07):

what does diverge mean?

Mario Carneiro (Jun 10 2020 at 14:07):

not stop

Mario Carneiro (Jun 10 2020 at 14:07):

recursive meta definitions use macros to indicate the recursion, they aren't defeq to their unfolding

Kenny Lau (Jun 10 2020 at 14:08):

but can we prove foo = [foo._main]?

Mario Carneiro (Jun 10 2020 at 14:08):

I'm not even sure the concept makes sense since the kernel never sees meta defs

Mario Carneiro (Jun 10 2020 at 14:09):

what does that even mean? In meta land everything is provable

Kenny Lau (Jun 10 2020 at 14:09):

meta def foo : Type :=
foo  foo

#print prefix foo
/-
foo : Type
foo._main : Type
-/

#print foo
/-
meta def foo : Type :=
foo._main
-/

#print foo._main
/-
meta def foo._main : Type :=
id_rhs Type ([foo._main] → [foo._main])
-/

Kenny Lau (Jun 10 2020 at 14:10):

what is the [] in [foo._main]?

Mario Carneiro (Jun 10 2020 at 14:10):

a macro

Kevin Buzzard (Jun 10 2020 at 14:10):

I just thought it meant "you dunfolded too much"

Kenny Lau (Jun 10 2020 at 14:11):

how is [] defined?

Mario Carneiro (Jun 10 2020 at 14:11):

You are thinking of the projection macro

Mario Carneiro (Jun 10 2020 at 14:11):

It is expr.macro

Mario Carneiro (Jun 10 2020 at 14:11):

it is a separate constructor from pi, lam, var,mvar and everything else

Mario Carneiro (Jun 10 2020 at 14:12):

Here's a projection macro:

#print and.left
-- @[reducible]
-- def and.left : ∀ {a b : Prop}, a ∧ b → a :=
-- λ (a b : Prop) (c : a ∧ b), [and.left c]

Kenny Lau (Jun 10 2020 at 14:12):

how do I produce a term of type [\a]?

Mario Carneiro (Jun 10 2020 at 14:12):

You can't

Mario Carneiro (Jun 10 2020 at 14:12):

seriously, this is super annoying

Kenny Lau (Jun 10 2020 at 14:12):

alright sorry

Mario Carneiro (Jun 10 2020 at 14:12):

but expr.macro uses an opaque type macro_def that lean code can't create

Mario Carneiro (Jun 10 2020 at 14:13):

no, not you, macros are annoying

Kenny Lau (Jun 10 2020 at 14:13):

can I use unchecked_cast?

Mario Carneiro (Jun 10 2020 at 14:13):

I think that will work

Kenny Lau (Jun 10 2020 at 14:13):

#check λ f : foo, f $ unchecked_cast f

Kenny Lau (Jun 10 2020 at 14:13):

but would it "work" like I want it to?

Mario Carneiro (Jun 10 2020 at 14:14):

hm, best think of a better test

Mario Carneiro (Jun 10 2020 at 14:14):

maybe use the Y combinator so that it halts

Mario Carneiro (Jun 10 2020 at 14:15):

You can at least use expr.macro_def_name to see what kind of macro you are looking at

Kenny Lau (Jun 10 2020 at 14:17):

variable {α : Type*}

meta def Y : (α  α)  α | f := f (Y f)

#check λ f : α  α, (rfl : Y f = f (Y f))
/-
invalid type ascription, term has type
  ?m_2 = ?m_2
but is expected to have type
  Y f = f (Y f)
-/

Kenny Lau (Jun 10 2020 at 14:17):

oh no

Kenny Lau (Jun 10 2020 at 14:21):

is it true that |A| = |A^A| iff |A| = 1?

Kevin Buzzard (Jun 10 2020 at 14:21):

#print has_add.add
/-
@[pattern, reducible]
def has_add.add : Π {α : Type u} [c : has_add α], α → α → α :=
λ (α : Type u) [c : has_add α], [has_add.add c]
-/

Is that also a macro?

Kevin Buzzard (Jun 10 2020 at 14:21):

If |A|>1 then |A^A|>=|2^A|>|A|

Kenny Lau (Jun 10 2020 at 14:22):

so we have proved that foo \equiv unit

Kenny Lau (Jun 10 2020 at 14:23):

meta def cantor := cantor  Prop

Kenny Lau (Jun 10 2020 at 14:23):

yay I broke Lean

Kevin Buzzard (Jun 10 2020 at 14:23):

You only meta-broke it -- that's allowed

Kevin Buzzard (Jun 10 2020 at 14:24):

Reid proved false the other day in meta land -- it wasn't hard

Kenny Lau (Jun 10 2020 at 14:26):

@Mario Carneiro how about this as a test: can you prove false using unchecked_cast and cantor?

Mario Carneiro (Jun 10 2020 at 14:26):

you can prove false using just unchecked_cast

Kenny Lau (Jun 10 2020 at 14:26):

meta def cantor := cantor  Prop

meta example : false :=
let R : cantor := λ A, ¬ (@unchecked_cast _ cantor A) A in
sorry

Kenny Lau (Jun 10 2020 at 14:26):

i.e. something like this

Mario Carneiro (Jun 10 2020 at 14:27):

meta example : false := unchecked_cast trivial

Kenny Lau (Jun 10 2020 at 14:27):

i.e. can you translate cantor's paradox

Mario Carneiro (Jun 10 2020 at 14:27):

yes

Mario Carneiro (Jun 10 2020 at 14:28):

you need to use unchecked_cast to prove the side condition on cantor_injective though

Mario Carneiro (Jun 10 2020 at 14:28):

so it's not very impressive

Mario Carneiro (Jun 10 2020 at 14:30):

Without the theorem that says that cantor = (cantor → Prop), you won't get anywhere in the proof

Kenny Lau (Jun 10 2020 at 14:30):

A B : set cantor,
H : unchecked_cast A = unchecked_cast B
 A = B

Kenny Lau (Jun 10 2020 at 14:30):

you mean this is unchecked_cast H?

Mario Carneiro (Jun 10 2020 at 14:31):

It's unchecked_cast of anything you want

Mario Carneiro (Jun 10 2020 at 14:31):

I think you are ascribing more meaning to this than is warranted

Kenny Lau (Jun 10 2020 at 14:31):

do we even "know" that cantor = (cantor \to Prop)?

Kenny Lau (Jun 10 2020 at 14:32):

oh right, in meta land everything is true

Mario Carneiro (Jun 10 2020 at 14:32):

In meta land, it's not a complete free for all, there is a semantics but it is more like the semantics of Haskell

Mario Carneiro (Jun 10 2020 at 14:32):

however unchecked_cast breaks even that

Kenny Lau (Jun 10 2020 at 14:32):

oh no this doesn't terminate:

#reduce @unchecked_cast true false trivial

Mario Carneiro (Jun 10 2020 at 14:33):

unchecked_cast is implemented as a loop IIRC

Mario Carneiro (Jun 10 2020 at 14:33):

oh nvm

Kenny Lau (Jun 10 2020 at 14:33):

#eval @unchecked_cast   3 -- 3

Mario Carneiro (Jun 10 2020 at 14:33):

try it for larger numbers :)

Kenny Lau (Jun 10 2020 at 14:34):

guess the outputs:

#eval @unchecked_cast empty  (unchecked_cast tt)
#eval @unchecked_cast empty  (unchecked_cast ff)

Mario Carneiro (Jun 10 2020 at 14:36):

One of these is not like the others:

#eval (list.range 34).map (λ n, @unchecked_cast   (2^n - 1))
-- [0, 1, 3, 7, 15, 31, 63, 127, 255, 511, 1023, 2047, 4095, 8191, 16383,
--  32767, 65535, 131071, 262143, 524287, 1048575, 2097151, 4194303, 8388607,
--  16777215, 33554431, 67108863, 134217727, 268435455, 536870911, 1073741823,
--  -1, 4294967295, 8589934591]

Mario Carneiro (Jun 10 2020 at 14:38):

Oh haha the reason #reduce @unchecked_cast true false trivial doesn't terminate is for the very silly reason that strings are involved

Mario Carneiro (Jun 10 2020 at 14:40):

this works fine

meta def {u} unchecked_cast' {α : Sort u} {β : Sort u} : α  β :=
cast (undefined_core "")

#reduce @unchecked_cast' true false trivial
-- eq.rec true.intro (undefined_core {data := list.nil char})

Kenny Lau (Jun 10 2020 at 14:40):

why does it being "undefined" make it not terminate?

Patrick Massot (Jun 10 2020 at 14:41):

It reminds me that we have something for @Gabriel Ebner who is already hunting down ideas for Lean 3.17.0: fix https://github.com/leanprover-community/doc-gen/blob/master/src/export_json.lean#L284-L287. I had to use the same itersplit trick in the sphere eversion infrastructure.

Mario Carneiro (Jun 10 2020 at 14:41):

it terminates but only after about O(size of unicode * length of string * very large #reduce constant) steps

Gabriel Ebner (Jun 10 2020 at 14:42):

I'm not sure if these two are related, but this applies for both of them: please file a #mwe at the lean bug tracker!

Mario Carneiro (Jun 10 2020 at 14:42):

wait, is there a lean feature suggestion in this thread?

Rob Lewis (Jun 10 2020 at 14:42):

Mario Carneiro said:

One of these is not like the others:

#eval (list.range 34).map (λ n, @unchecked_cast   (2^n - 1))
-- [0, 1, 3, 7, 15, 31, 63, 127, 255, 511, 1023, 2047, 4095, 8191, 16383,
--  32767, 65535, 131071, 262143, 524287, 1048575, 2097151, 4194303, 8388607,
--  16777215, 33554431, 67108863, 134217727, 268435455, 536870911, 1073741823,
--  -1, 4294967295, 8589934591]

https://oeis.org/search?q=0%2C+1%2C+3%2C+7%2C+15%2C+31%2C+63%2C+127%2C+255%2C+511%2C+1023%2C+2047%2C+4095%2C+8191%2C+16383%2C+32767%2C+65535%2C+131071%2C+262143%2C+524287%2C+1048575%2C+2097151%2C+4194303%2C+8388607%2C++16777215%2C+33554431%2C+67108863%2C+134217727%2C+268435455%2C+536870911%2C+1073741823%2C++-1%2C+4294967295%2C+8589934591&sort=&language=english&go=Search
:(

Kevin Buzzard (Jun 10 2020 at 14:49):

When I've got my number theorists hat on and I find a non-OEIS sequence I add it! But I'm not sure they'll like this one...

Kevin Buzzard (Jun 10 2020 at 14:50):

Kenny Lau said:

guess the outputs:

#eval @unchecked_cast empty  (unchecked_cast tt)
#eval @unchecked_cast empty  (unchecked_cast ff)

http://bash.org/?10958 (aah, the old days)


Last updated: Dec 20 2023 at 11:08 UTC