f x = x

Stream: general

[Kevin Buzzard]

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

[Kevin Buzzard]

@Kenny Lau

[Kevin Buzzard]

I will think about your rec problem

[Kevin Buzzard]

can you remind me of it

[Kevin Buzzard]

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

[Kevin Buzzard]

Maybe one should make some counterexample

[Kevin Buzzard]

maybe create a structure generated by x and f x and use no_confusion

[Kevin Buzzard]

and this structure is nat

[Kevin Buzzard]

and x is 0 and f is succ

[Kevin Buzzard]

so maybe try to build a counterexample...

[Kevin Buzzard]

I did your acc question

[Kevin Buzzard]

It is really fun to do it in tactic mode

[Kevin Buzzard]

you are in a pretty tight spot

[Kevin Buzzard]

but there's only one way out

[Kevin Buzzard]

and there are loops

[Kevin Buzzard]

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

[Kevin Buzzard]

But my maze is impossible to get out of

[Kevin Buzzard]

and yours I can escape from

[Kevin Buzzard]

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]

Did you see the "theorems for free" paper?

[Kevin Buzzard]

@Kenny Lau

[Kevin Buzzard]

Kenny apparently this theorem is free

[Kevin Buzzard]

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]

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]

but, I mean, if X is int and f is negation then we all know it's false

[Mario Carneiro]

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]

but you can't prove it

[Kenny Lau]

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

[Mario Carneiro]

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]

(which I think is what Kevin meant to say)

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kenny Lau]

did you just use a colon lol

[Mario Carneiro]

of course not, what do you take me for

[Kenny Lau]

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]

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]

However, if you avoid choice according to #print axioms, then I believe it to be true, although that's a future project

[Kenny Lau]

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

[Mario Carneiro]

no, it would be a metatheorem

[Mario Carneiro]

i.e. a section in my paper

[Mario Carneiro]

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]

Dang, I was only thinking about Prop being erasable.

[Mario Carneiro]

Furthermore, Kevin claims that he uses choice in his definitions, and I actually doubt it, since I'm talking about the type operator itself