Zulip Chat Archive

Stream: general

Topic: f x = x


view this post on Zulip Kevin Buzzard (Apr 28 2018 at 23:59):

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

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 23:59):

@Kenny Lau

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 23:59):

I will think about your rec problem

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 23:59):

can you remind me of it

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 23:59):

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

view this post on Zulip Kevin Buzzard (Apr 29 2018 at 00:01):

Maybe one should make some counterexample

view this post on Zulip Kevin Buzzard (Apr 29 2018 at 00:02):

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

view this post on Zulip Kevin Buzzard (Apr 29 2018 at 00:02):

and this structure is nat

view this post on Zulip Kevin Buzzard (Apr 29 2018 at 00:02):

and x is 0 and f is succ

view this post on Zulip Kevin Buzzard (Apr 29 2018 at 00:03):

so maybe try to build a counterexample...

view this post on Zulip Kevin Buzzard (Apr 29 2018 at 00:32):

I did your acc question

view this post on Zulip Kevin Buzzard (Apr 29 2018 at 00:32):

It is really fun to do it in tactic mode

view this post on Zulip Kevin Buzzard (Apr 29 2018 at 00:32):

you are in a pretty tight spot

view this post on Zulip Kevin Buzzard (Apr 29 2018 at 00:32):

but there's only one way out

view this post on Zulip Kevin Buzzard (Apr 29 2018 at 00:32):

and there are loops

view this post on Zulip Kevin Buzzard (Apr 29 2018 at 00:32):

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

view this post on Zulip Kevin Buzzard (Apr 29 2018 at 00:42):

But my maze is impossible to get out of

view this post on Zulip Kevin Buzzard (Apr 29 2018 at 00:42):

and yours I can escape from

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 29 2018 at 01:08):

Did you see the "theorems for free" paper?

view this post on Zulip Kevin Buzzard (Apr 29 2018 at 01:08):

@Kenny Lau

view this post on Zulip Kevin Buzzard (Apr 29 2018 at 01:20):

Kenny apparently this theorem is free

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 29 2018 at 05:11):

but you can't prove it

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 29 2018 at 05:12):

(which I think is what Kevin meant to say)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 29 2018 at 05:14):

did you just use a colon lol

view this post on Zulip Mario Carneiro (Apr 29 2018 at 05:14):

of course not, what do you take me for

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 29 2018 at 05:16):

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

view this post on Zulip Mario Carneiro (Apr 29 2018 at 05:17):

no, it would be a metatheorem

view this post on Zulip Mario Carneiro (Apr 29 2018 at 05:17):

i.e. a section in my paper

view this post on Zulip 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

view this post on Zulip Reid Barton (Apr 29 2018 at 05:20):

Dang, I was only thinking about Prop being erasable.

view this post on Zulip 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