# Zulip Chat Archive

## Stream: general

### Topic: f x = x

#### Kevin Buzzard (Apr 28 2018 at 23:59):

`theorem is_it_true (X : Type) (f : X → X) (x : X) : f x = x := sorry`

#### Kevin Buzzard (Apr 28 2018 at 23:59):

@Kenny Lau

#### Kevin Buzzard (Apr 28 2018 at 23:59):

I will think about your rec problem

#### Kevin Buzzard (Apr 28 2018 at 23:59):

can you remind me of it

#### Kevin Buzzard (Apr 28 2018 at 23:59):

but in the mean time what do you think of that one

#### Kevin Buzzard (Apr 29 2018 at 00:01):

Maybe one should make some counterexample

#### Kevin Buzzard (Apr 29 2018 at 00:02):

maybe create a structure generated by `x`

and `f x`

and use `no_confusion`

#### Kevin Buzzard (Apr 29 2018 at 00:02):

and this structure is nat

#### Kevin Buzzard (Apr 29 2018 at 00:02):

and x is 0 and f is succ

#### Kevin Buzzard (Apr 29 2018 at 00:03):

so maybe try to build a counterexample...

#### Kevin Buzzard (Apr 29 2018 at 00:32):

I did your acc question

#### Kevin Buzzard (Apr 29 2018 at 00:32):

It is really fun to do it in tactic mode

#### Kevin Buzzard (Apr 29 2018 at 00:32):

you are in a pretty tight spot

#### Kevin Buzzard (Apr 29 2018 at 00:32):

but there's only one way out

#### Kevin Buzzard (Apr 29 2018 at 00:32):

and there are loops

#### Kevin Buzzard (Apr 29 2018 at 00:32):

example (α : Type*) (r : α → α → Prop) (x : α) (H : acc r x) : r x x → false :=

#### Kevin Buzzard (Apr 29 2018 at 00:42):

But my maze is impossible to get out of

#### Kevin Buzzard (Apr 29 2018 at 00:42):

and yours I can escape from

#### Kevin Buzzard (Apr 29 2018 at 00:43):

example (α : Type*) (r : α → α → Prop) (x : α) (H : acc r x) : r x x → false := begin intro H1, -- only one move induction H with y Hy Hcomplicated, -- let's leave the scary term till last clear x, -- works! x is no longer relevant -- only one move have H2 : acc r y := Hy y H1, -- never even use this -- must use complicated thing exact Hcomplicated y H1 H1, end

#### Kevin Buzzard (Apr 29 2018 at 01:08):

Did you see the "theorems for free" paper?

#### Kevin Buzzard (Apr 29 2018 at 01:08):

@Kenny Lau

#### Kevin Buzzard (Apr 29 2018 at 01:20):

Kenny apparently this theorem is free

#### Kevin Buzzard (Apr 29 2018 at 01:20):

theorem free_fun (r : ∀ (X : Type), X → X) : ∀ (A B : Type), ∀ f : A → B, ∀ a : A, r B (f a) = f (r A a) := sorry

#### Kenny Lau (Apr 29 2018 at 04:30):

`theorem is_it_true (X : Type) (f : X → X) (x : X) : f x = x := sorry`

well that is indeed the Church encoding of the unit type

#### Kenny Lau (Apr 29 2018 at 04:32):

but, I mean, if X is `int`

and `f`

is negation then we all know it's false

#### Mario Carneiro (Apr 29 2018 at 05:11):

In the formalism of "theorems for free", you can state something even stronger than `free_fun`

there: every closed term of type `∀ (X : Type), X → X`

is the identity function

#### Kenny Lau (Apr 29 2018 at 05:11):

but you can't prove it

#### Kenny Lau (Apr 29 2018 at 05:12):

I mean, you can prove it, but you can't assume in Lean that every function has a closed term

#### Mario Carneiro (Apr 29 2018 at 05:12):

right, it's a metatheorem of the logic, so it's not to say that `\forall (r : ∀ (X : Type), X → X) (a : Type) (x : a), r a x = x`

is inhabited

#### Mario Carneiro (Apr 29 2018 at 05:12):

(which I think is what Kevin meant to say)

#### Mario Carneiro (Apr 29 2018 at 05:13):

it is of course false that `\forall (X : Type) (f : X → X) (x : X), f x = x`

#### Mario Carneiro (Apr 29 2018 at 05:13):

and in lean, it's not even true at the meta level because of non-parametric functions based on `choice`

#### Kenny Lau (Apr 29 2018 at 05:14):

did you just use a colon lol

#### Mario Carneiro (Apr 29 2018 at 05:14):

of course not, what do you take me for

#### Kenny Lau (Apr 29 2018 at 05:14):

theorem but_it_is_false : ¬∀ (X : Type) (f : X → X) (x : X), f x = x := λ H, nat.no_confusion $ H nat nat.succ 0

#### Mario Carneiro (Apr 29 2018 at 05:15):

Reid asks if it's true for computable functions, and it's not, trivially; every functor `Type -> Type`

is computable simply because `Type`

is erasable

#### Mario Carneiro (Apr 29 2018 at 05:16):

However, if you avoid choice according to `#print axioms`

, then I believe it to be true, although that's a future project

#### Kenny Lau (Apr 29 2018 at 05:16):

project? can you ever check whether a function uses an axiom inside?

#### Mario Carneiro (Apr 29 2018 at 05:17):

no, it would be a metatheorem

#### Mario Carneiro (Apr 29 2018 at 05:17):

i.e. a section in my paper

#### Mario Carneiro (Apr 29 2018 at 05:18):

but you could formalize such a proof in lean by creating tactics that produce the appropriate free theorem and prove it, failing if they run across an instance of choice

#### Reid Barton (Apr 29 2018 at 05:20):

Dang, I was only thinking about `Prop`

being erasable.

#### Mario Carneiro (Apr 29 2018 at 05:22):

Furthermore, Kevin claims that he uses `choice`

in his definitions, and I actually doubt it, since I'm talking about the type operator itself

Last updated: May 13 2021 at 04:21 UTC