applying a function to itself

Stream: new members

[Kenny Lau]

meta def foo : Type :=
foo → foo

#check λ f g : foo, f g

[Kenny Lau]

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

[Kenny Lau]

how do I make it work?

[Kenny Lau]

I want to apply a function to itself

[Kenny Lau]

why does foo have no equational lemma?

[Pedro Minicz]

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]

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]

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]

Another example of interest:

variable β : Type*

#check @id' (β → β) id'

[Kenny Lau]

@Mario Carneiro

[Mario Carneiro]

hi

[Mario Carneiro]

it's not going to work

[Kenny Lau]

why not

[Mario Carneiro]

because this would make the typechecker diverge

[Kenny Lau]

what does diverge mean?

[Mario Carneiro]

not stop

[Mario Carneiro]

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

[Kenny Lau]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kenny Lau]

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]

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

[Mario Carneiro]

a macro

[Kevin Buzzard]

I just thought it meant "you dunfolded too much"

[Kenny Lau]

how is [] defined?

[Mario Carneiro]

You are thinking of the projection macro

[Mario Carneiro]

It is expr.macro

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

You can't

[Mario Carneiro]

seriously, this is super annoying

[Kenny Lau]

alright sorry

[Mario Carneiro]

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

[Mario Carneiro]

no, not you, macros are annoying

[Kenny Lau]

can I use unchecked_cast?

[Mario Carneiro]

I think that will work

[Kenny Lau]

#check λ f : foo, f $ unchecked_cast f

[Kenny Lau]

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

[Mario Carneiro]

hm, best think of a better test

[Mario Carneiro]

maybe use the Y combinator so that it halts

[Mario Carneiro]

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

[Kenny Lau]

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]

oh no

[Kenny Lau]

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

[Kevin Buzzard]

#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]

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

[Kenny Lau]

so we have proved that foo \equiv unit

[Kenny Lau]

meta def cantor := cantor → Prop

[Kenny Lau]

yay I broke Lean

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kenny Lau]

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

[Mario Carneiro]

you can prove false using just unchecked_cast

[Kenny Lau]

meta def cantor := cantor → Prop

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

[Kenny Lau]

i.e. something like this

[Mario Carneiro]

meta example : false := unchecked_cast trivial

[Kenny Lau]

i.e. can you translate cantor's paradox

[Mario Carneiro]

yes

[Mario Carneiro]

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

[Mario Carneiro]

so it's not very impressive

[Mario Carneiro]

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

[Kenny Lau]

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

[Kenny Lau]

you mean this is unchecked_cast H?

[Mario Carneiro]

It's unchecked_cast of anything you want

[Mario Carneiro]

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

[Kenny Lau]

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

[Kenny Lau]

oh right, in meta land everything is true

[Mario Carneiro]

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]

however unchecked_cast breaks even that

[Kenny Lau]

oh no this doesn't terminate:

#reduce @unchecked_cast true false trivial

[Mario Carneiro]

unchecked_cast is implemented as a loop IIRC

[Mario Carneiro]

oh nvm

[Kenny Lau]

#eval @unchecked_cast ℕ ℤ 3 -- 3

[Mario Carneiro]

try it for larger numbers :)

[Kenny Lau]

guess the outputs:

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

[Mario Carneiro]

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]

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]

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]

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

[Patrick Massot]

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]

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

[Gabriel Ebner]

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]

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

[Rob Lewis]

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]

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]

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)