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

@Kenny Lau

#### 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):

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


@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