Kaminski's Equation

Stream: Is there code for X?

[Aaron Bies]

Hi, I would like to add the following identity to the mathlib, but I'm unsure what to call it.

@[simp] theorem kaminski (f : bool → bool) (x : bool) : f (f (f x)) = f x :=
by cases x; cases h₁ : f tt; cases h₂ : f ff; simp only [h₁, h₂]

I guess by #naming, it should be bool.f_f_f_eq_f or bool.f_of_f_f_f or maybe just bool.f_f_f?

[Yaël Dillies]

... except that f is the name of a free variable. I would rather call it bool.apply_apply_apply or bool.apply_apply_apply_eq_apply

[Eric Wieser]

Yeah, naming things after a free variable is generally not so good

[Aaron Bies]

Fair point, bool.apply_apply_apply it is

[Patrick Johnson]

An alternative proof using fin_cases:

example {f : bool → bool} {x : bool} : f (f (f x)) = f x :=
by fin_cases f; cases x; refl

[Scott Morrison]

Note that this can't be a @[simp] lemma, as the head of the LHS is a metavariable.

[Scott Morrison]

Wow, I'm happy that fin_cases works here. :-)

[Scott Morrison]

I'm curious, is this identity actually "good for anything"? Is it "true for any reason" besides case bashing? I want (being highly prejudiced) to say that because it isn't "true for any reason" it can't be "good for anything". Convince me I'm wrong. :-)

[Kevin Buzzard]

Is there an analogous statement for endomorphisms of finite types? Hmm, I guess by pure thought there exist smallest numbers a(n) < b(n) such that f^a = f^b for all f:fin n -> fin n and this proof above shows a(2)=1, b(2)=3.

[Scott Morrison]

Okay, I guess that general fact is more or less good for something. But since it was true by pure thought, that's okay. (I think we've exhausted this line of thought, sorry. :-)

[Kevin Buzzard]

Quick let's call it the Buzzard-Morrison Equation in case it's useful for something.

[Kevin Buzzard]

My guess is that a(n)=O(n) and b(n)=O(n!)

[Eric Rodriguez]

To me, it's because functions bool -> bool are involutive, constant, or identity, and only because of the constant functions does f(f(x)) = x not hold. I guess this means b(n) = lcm(1...n) which surely has a nice value

[Yaël Dillies]

... it is asymptotically $e^n$

[Eric Rodriguez]

Wow, according to oeis: "An assertion equivalent to the Riemann hypothesis is: | log(a(n)) - n | < sqrt(n) * log(n)^2. " (for a(n) our b(n))

[Yaël Dillies]

Whoops :rofl:

[Eric Rodriguez]

Maybe you just solved RH, Yaël ;b

[Scott Morrison]

Who's going to PR it?

[Yaël Dillies]

RH? I skip my turn :grinning:

[Eric Wieser]

Patrick Johnson said:

An alternative proof using fin_cases:

Here's an even easier proof:

example : ∀ {f : bool → bool} {x : bool}, f (f (f x)) = f x :=
dec_trivial

[Kevin Buzzard]

The issue is not about the growth (which is equivalent to the prime number theorem), it's about the error bounds (which is equivalent to the Riemann Hypothesis).

[Aaron Bies]

Damn this thread exploded while I was doing the dishes

[Aaron Bies]

My PR for this is #14159

[Eric Rodriguez]

Where did you find this name for this equation, Aaron? I can't seem to find kaminski's equation on Google...

[Aaron Bies]

It was taught to me by Gert Smolka; He also mentions it in his script in chapter 3.8

[Eric Wieser]

It says there:

The equation was brought up as a proof challenge by Mark Kaminski in 2005 when he wrote
his Bachelor’s thesis on classical higher-order logic.

[Eric Wieser]

The thesis at at https://www.ps.uni-saarland.de/Publications/documents/kaminski-bthesis.pdf, but I can't find the thing being referenced

[Aaron Bies]

hmm, I guess it came up while he was writing his thesis, but it didn't actually make it into the thesis

[Aaron Bies]

The thesis does reason about functions on booleans a lot, so it makes sense he'd stumble across this identity

[Eric Wieser]

It's entirely possible it's in there, just not in a form that's easy to spot

[Kyle Miller]

It would have been funny if

example (f : Prop → Prop) (p : Prop) : f (f (f p)) ↔ f p := sorry

were constructively true, since then docs#not_of_not_not_not would just be a consequence.

It's not constructively true though. Using the Heyting algebra of open sets of the real line, f could be a translation one unit to the right, and that translation turns out not to have finite order.

[Kevin Buzzard]

so you can even prove that there's no distinct a and b with f^a=f^b :-(

[Mario Carneiro]

Something seems fishy about that argument; you can give the same counterexample for the boolean algebra of sets on the real line

[Yaël Dillies]

Well, I think that shows

example {α : Type*} [boolean_algebra α] (f : α → α) (a : α) : f (f (f a)) = f a := sorry

is false.

[Mario Carneiro]

I think I found a definable counterexample:

import tactic.itauto

def f (p : Prop) := ¬ p ∨ ¬ ¬ p
theorem T (p : Prop) : f (f (f p)) → f p :=
by unfold f; itauto -- fail

itauto is super useful here for being a complete decision procedure for intuitionistic logic

[Mario Carneiro]

here's a more comprehensible explanation of why it fails:

theorem T (p : Prop) : f (f (f p)) → f p :=
begin
  unfold f,
  intro h,
  cases h,
  { itauto },
  { simp only [show ¬ (¬ p ∨ ¬ ¬ p) ↔ false, by itauto, false_or, not_false_iff, not_true] at h,
    -- the hypothesis was useless, the goal is now
    -- h: true ⊢ ¬p ∨ ¬¬p
    itauto, } -- fails
end

[Mario Carneiro]

alternatively:

import tactic.itauto

def f (p : Prop) := ¬ p ∨ ¬ ¬ p
example (p : Prop) (h : f (f (f p)) → f p) : ¬p ∨ ¬¬p :=
by unfold f at h; itauto -- ok

[Aaron Bies]

Related to the generalized case, how does one arrive at the conclusion that A0665500 is equivalent to $lcm(1...n)+n-1$?

[Kyle Miller]

Mario Carneiro said:

Something seems fishy about that argument; you can give the same counterexample for the boolean algebra of sets on the real line

I was wondering about that -- I guess it comes down to what Prop -> Prop is supposed to mean? The translation example is at least an isomorphism of Heyting algebras induced by a symmetric of the underlying space, but, beyond that, it seems like you might not want to allow arbitrary functions on a Heyting algebra...

[Kyle Miller]

That's cool that you can prove the weak law of the excluded middle with this.

[Mauricio Collares]

I've had this question for a while, apologies for jumping in with a slightly off-topic question: In intuitionistic logic, is the weak law of the excluded middle both unprovable and strictly weaker than actual excluded middle? It feels like that's the case but I've never seen a proof.

[Kyle Miller]

I don't know the answer, but at least itauto can't prove it, and it can't prove em from the weak em applied to the same p.

example (p : Prop) : ¬p ∨ ¬¬p :=
by itauto -- not ok

example (p : Prop) (h : p ∨ ¬p) : ¬p ∨ ¬¬p :=
by itauto -- ok

example (p : Prop) (h : ¬p ∨ ¬¬p) : p ∨ ¬p :=
by itauto -- not ok

[Mauricio Collares]

I guess the interesting alternative would be "weak EM => EM" being unprovable.

[Eric Rodriguez]

Afair, there's a hierarchy of Em's, but this isn't it. @Mario Carneiro sent me the link before.

[Kyle Miller]

@Eric RodriguezAre you referring to this? mario's post

Direct link to an illustration of the Rieger-Nishimura lattice

[Eric Rodriguez]

Yea, that's the one!!!

[Yaël Dillies]

Yep exactly. This is also the free lattice on three elements.

[Mauricio Collares]

This is very interesting! It seems to suggest that "weak EM => EM" is really unprovable, but I am not 100% sure this is the same question. In the lattice, it looks like everything is specialized to a particular proposition.

[Mario Carneiro]

yes, weak EM => EM is unprovable, but it's true that the distinctness of the relevant points in the Rieger-Nishimura lattice does not prove this, only that weak_EM(p) -> EM(p) is unprovable (it could be that weak_EM(f(p)) -> EM(p) for some f)

[Mario Carneiro]

In fact, weak EM is the only thing you can deduce from kaminski's equation (on definable formulas f). More precisely, if f is a univariate function on propositions built from [p, ⊤, ⊥, →, ¬, ∧, ∨], then ¬p ∨ ¬¬p → f (f (f p)) ↔ f p holds.

Proof: By cases on ¬p ∨ ¬¬p.

• If ¬p is true, then p <-> false so we are in the bool subset of the logic and therefore f (f (f p)) ↔ f p by evaluating it to true or false and observing that this is a classical theorem.
• If ¬¬p, we end up in a three-valued logic, because ¬p <-> false and all the other operators are closed in the set [p, ⊤, ⊥]. There are only six reachable functions in this logic: ⊥, ⊤, x, ¬x, ¬¬x, x ∨ ¬x, and for all of these functions Kaminski's theorem holds:

@[derive [decidable_eq, fintype]] inductive val | true | false | p

def val.not : val → val
| val.true := val.false
| val.false := val.true
| val.p := val.false

def val.and : val → val → val
| val.true p := p
| p val.true := p
| val.false _ := val.false
| _ val.false := val.false
| val.p val.p := val.p

def val.or : val → val → val
| val.false p := p
| p val.false := p
| val.true _ := val.true
| _ val.true := val.true
| val.p val.p := val.p

def val.imp : val → val → val
| val.false p := val.true
| p val.false := val.not p
| val.true p := p
| _ val.true := val.true
| val.p val.p := val.true

@[derive decidable] def is_valid (f : val → val) : Prop :=
  (∀ v, f v = val.p → v = val.p) ∧
  (f = id ∨ f = (λ i, i.or i.not) ∨ f val.true = f val.p)

theorem true.is_valid : is_valid (λ _, val.true) := dec_trivial
theorem false.is_valid : is_valid (λ _, val.false) := dec_trivial
theorem id.is_valid : is_valid id := dec_trivial
theorem not.is_valid : ∀ (f : val → val),
  is_valid f → is_valid (λ i, (f i).not) := dec_trivial
theorem and.is_valid : ∀ (f g : val → val),
  is_valid f → is_valid g → is_valid (λ i, (f i).and (g i)) := dec_trivial
theorem or.is_valid : ∀ (f g : val → val),
  is_valid f → is_valid g → is_valid (λ i, (f i).or (g i)) := dec_trivial
theorem imp.is_valid : ∀ (f g : val → val),
  is_valid f → is_valid g → is_valid (λ i, (f i).imp (g i)) := dec_trivial

theorem kaminski : ∀ (f : val → val),
  is_valid f → ∀ v, f (f (f v)) = f v := dec_trivial

[Kevin Buzzard]

ha ha this is funny because abstractly the answer for f : fin 3 -> fin 3 is: if it's a 3-cycles then f^3=f^0 and if it's not then the image has size <= 2 so Kaminski kicks in after one application and we deduce f^4=f^2, so always f^8=f^2 (in particular strictly worse).

[Patrick Johnson]

Kevin Buzzard said:

Is there an analogous statement for endomorphisms of finite types? Hmm, I guess by pure thought there exist smallest numbers a(n) < b(n) such that f^a = f^b for all f:fin n -> fin n and this proof above shows a(2)=1, b(2)=3.

Do we actually have this (or similar) in mathlib?

example {n : ℕ} : ∃ (a b : ℕ), a < b ∧ ∀ {f : fin n → fin n}, (f^[a]) = (f^[b]) :=
begin
  sorry
end

[Aaron Bies]

I actually looked into a more generalised version of kaminski for my own practice and this is how far I got

[Aaron Bies]

(Also, if anyone here has an idea on how to prove the last statement, please let me know)

[Floris van Doorn]

Patrick Johnson said:

Do we actually have this (or similar) in mathlib?

example {n : ℕ} : ∃ (a b : ℕ), a < b ∧ ∀ {f : fin n → fin n}, (f^[a]) = (f^[b]) :=
begin
  sorry
end

It's basically docs#not_injective_infinite_fintype applied to (fin n → fin n) → (fin n → fin n)

import data.fintype.basic

open function
lemma linear_order.injective_iff {α β} [linear_order α] {f : α → β} :
  injective f ↔ ∀ a b, a < b → f a ≠ f b :=
⟨λ h a b hab hfab, hab.ne $ h hfab, λ h a b hfab, by_contra $ λ hab : a ≠ b,
  hab.lt_or_lt.elim (λ hab, h a b hab hfab) (λ hba, h b a hba hfab.symm)⟩

example {n : ℕ} : ∃ (a b : ℕ), a < b ∧ ∀ {f : fin n → fin n}, (f^[a]) = (f^[b]) :=
begin
  have : ¬ injective (λ (k : ℕ) (f : fin n → fin n), f^[k]) :=
  not_injective_infinite_fintype _,
  simp_rw [linear_order.injective_iff] at this,
  push_neg at this,
  simp only [funext_iff] at this {single_pass := tt},
  exact this
end

[Reid Barton]

Or docs#fintype.exists_ne_map_eq_of_infinite

[Floris van Doorn]

Oh, that one is a little closer indeed (with the negation of injective unfolded).

[Alex J. Best]

Reminds me of https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/.E2.9C.94.20f.5E.5Bn.5D.20x.20.3D.20x/near/266557825, so I ended up with:

import data.fintype.basic
import group_theory.exponent
import algebra.hom.iterate
import group_theory.group_action.defs
import data.set.finite
.

lemma key {M : Type*} [fintype M] (f : M → M) (a) : (id (f^[a]) : function.End M) = f ^ a :=
begin
  simp,
  induction a,
  refl,
  simpa [a_ih, pow_succ'],
end
open monoid
open_locale classical
noncomputable theory
instance {M : Type*} [fintype M] : fintype (function.End M) := by delta_instance function.End
example {M : Type*} [fintype M] : ∃ (a b : ℕ), a < b ∧ ∀ {f : M → M}, (f^[a]) = (f^[b]) :=
begin
  suffices : ∃ (a b : ℕ), a < b ∧ (λ f : function.End M, f) ^ a = (λ f : function.End M, f) ^ b,
  { apply Exists₂.imp _ this,
    rintros a b ⟨h₁, h₂⟩,
    simp only [h₁, true_and],
    intro f,
    have := congr_fun h₂ f,
    rwa [pi.pow_apply, pi.pow_apply, ← key, ← key] at this, },
  simpa using set.infinite_univ.exists_lt_map_eq_of_maps_to (set.maps_to_univ (λ n : ℕ, (λ f : function.End M, f) ^ n) _) set.finite_univ,
end

Floris's is much cleaner!

[Kyle Miller]

@Patrick Johnson That reminded me that a while back I built out some theory as an exercise, and it could be used to prove this. The core idea is that for a fintype, there's some positive n such that f^[n] is a bijection when restricted to its image, and then you can take the order k of that permutation to get that f^[n] = f^[n+k].

[Kyle Miller]

Oh, that's in the same thread Alex just linked to.

[Kyle Miller]

I think the "Kaminski-Buzzard-Morrison" numbers can be found the following way:

Supposing a < b and f^a = f^b, then f restricted to f^a is a bijection. Hence b-a <= g(|im f^a|), where g(n) is the Landau function (the largest order of an element of the symmetric group).

Given any finite set X, subset S, and permutation p of S, then that permutation can be extended to be a function f : X -> X such that the image of some power of f is S. There is such an f such that the least such power is |X - S|, and this is the maximal least power over all f. In this case, a=|X-S| and b=a+order(p). So, one can maximize b by taking p with maximal order, getting a=|X-S| and b=a+g(|S|).

Hence, the set of all Kaminski-Buzzard-Morrison numbers for a particular set X of cardinality n is {(n-k, n-k+g(k)) | k in 1..n}. I'm defining the numbers to be pairs (a,b) from those equations f^a=f^b with a<b such that there is no smaller a for the given f and, for that a, no other f that can make b larger.

[Kyle Miller]

I just realized I made a mistake there -- these aren't the universal numbers since you do need to take the lcm of all the orders.

[Kyle Miller]

Anyway, you need a(n) = n-1 since f could be pred on fin n, and then b(n) = lcm(1,2,...,n) + n - 1. That matches what Kevin said for the n=3 case (f^8 = f^2).

[Kyle Miller]

Aaron Bies said:

Related to the generalized case, how does one arrive at the conclusion that A0665500 is equivalent to $lcm(1...n)+n-1$?

I see you already mentioned this formula. I think what's going on is that the only functions you can really define using the typed lambda calculus are iterates, so 1, f, f^1, f^2, ..., f^(b-1) are the only functions.

[Mario Carneiro]

Kevin Buzzard said:

ha ha this is funny because abstractly the answer for f : fin 3 -> fin 3 is: if it's a 3-cycles then f^3=f^0 and if it's not then the image has size <= 2 so Kaminski kicks in after one application and we deduce f^4=f^2, so always f^8=f^2 (in particular strictly worse).

Note that it's not really fin 3 -> fin 3; although there are three values in the domain the third element is rather special since you can't just map it arbitrarily, and true and false can never map to p. I ended up with the list of conditions in is_valid more or less by seeing what things were preserved by the operations.

[Kevin Buzzard]

Yes exactly, the weird logic stuff saves you; the fin 3 argument is what you get for free but you teased more out of it

[Patrick Johnson]

Aaron Bies said:

I actually looked into a more generalised version of kaminski for my own practice and this is how far I got
(Also, if anyone here has an idea on how to prove the last statement, please let me know)

I proved it for a = n and b = n + n.factorial (proof). It's probably easy to reduce it to b = list.foldr nat.lcm 1 (list.iota n) + n, but the problem is -1 both in a and b, which I didn't manage to prove.