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: Dec 20 2023 at 11:08 UTC