How to formulate sets of functions in general?

Stream: new members

[Justus Willbad]

Could you please help to formulate my theorem and proof in Lean?

Theorem:
Let
$n\in\mathbb{N}_+$,
$X,Y$ sets,
$F$ the set of all functions that map out of $X$ into $Y$,
$f_1,...,f_n\in F$
$F_0=\{f_1,...,f_n\}$,
$F_1$ the set of all elements of $F$ that are compositions of finite numbers of elements of $F_0$,
$f_i\in F_1$ non-constant has an inverse $f_i^{-1}\in F_1$,
$f_j\in F_1$ non-constant has a right inverse $f_j^{-1}\in F_1$,
$g\in F\setminus F_1$ non-constant.
Then $f_i\circ g\circ f_j\notin F_1$.

Proof:
$f=f_i\circ g\circ f_j$
$f_i^{-1}\circ f\circ f_j^{-1}=g$
We are conducting a proof of contradiction.
Assumption: $f\in F_1$.
Because $f_i^{-1},f,f_j^{-1}\in F_1$ and $F_1$ is closed regarding composition, $g\in F_1$. This is in contradiction to the preconditions.
q.e.d.

Until now, I have only the following.

import Mathlib
variable (n : ℕ)
variable (X Y : Type*)

theorem MyTheorem : fi ∘ g ∘ fj ∉ F1 := by
 by_contra! assumption
sorry

[Ilmārs Cīrulis]

What's non-constant compositions? Like functions that are compositions and also they aren't constant functions, yes?

[Ilmārs Cīrulis]

Ok, I started tinkering...

import Mathlib

def is_constant_function {A B: Type} (f: A → B): Prop := ∃ y, ∀ x, f x = y
def is_nonconstant_function {A B: Type} (f: A → B): Prop := ¬ is_constant_function f

[Ilmārs Cīrulis]

How do you do compositions of more than one function if all elements of $F_0$ is functions that map out of $X$ into $Y$? And, presumably, sets $X$ and $Y$ are different.

Probably I'm not understanding something...

[Etienne Marion]

I agree with Lessness, you can't compose the functions in $F_0$.

[Justus Willbad]

You are right. We have to set $Y=X$. We can remove $Y$.

[Etienne Marion]

Here is a way of introducing the variables and the statement:

import Mathlib

open List Function

variable {X : Type*} (F0 : List (X → X))

def F1 : Set (X → X) := {f | ∃ l, l ⊆ F0 ∧ f = l.foldr (· ∘ ·) id ∧ ∃ x y, f x ≠ f y}

variable (fi fj : X → X) (hfi : fi ∈ F1 F0) (hfj : fj ∈ F1 F0)
  (fi_inv fj_inv : X → X) (hfi_inv : fi_inv ∈ F1 F0) (hfj_inv : fj_inv ∈ F1 F0)
  (hi : LeftInverse fi_inv fi) (hj : RightInverse fj_inv fj)
  (g : X → X) (hg1 : ∃ x y, g x ≠ g y) (hg2 : g ∉ F1 F0)

example : fi ∘ g ∘ fj ∉ F1 F0 := by sorry

[Justus Willbad]

I have some questions.

1.) Why does variable {X : Type*} work, but variable (X : Type*) doesn't?

2.) What does the identity id mean in l.foldr (· ∘ ·) id?

3.) What does g x ≠ y mean in hg1? Do you mean g x ≠ g y?

4.) A function is a trivial composition. How can we formulate trivial compositions and nontrivial compositions together in one expression?

5.) You used example and not theorem. Is your example my theorem?

6.) Lean prints "No goals". Does this mean my theorem is true?

[Etienne Marion]

Justus Willbad said:

1.) Why does variable {X : Type*} work, but variable (X : Type*) doesn't?

It also works. The {} means that the argument is implicit so when using the theorem you don't need to specify it and Lean will try to infer it form the context.

Justus Willbad said:

2.) What does the identity id mean in l.foldr (· ∘ ·) id?

The foldr function works as follows: given a list [f, g, h] for instance it will return f ∘ g ∘ h ∘ id. You need to specify what function you take at the beginning so that foldr will also work on the empty list.

Justus Willbad said:

3.) What does g x ≠ y mean in hg1? Do you mean g x ≠ g y?

This is a typo, I edited it.

Justus Willbad said:

4.) A function is a trivial composition. How can we formulate trivial compositions and nontrivial compositions together in one expression?

Not sure what you mean here, but you can prove that List.foldr (· ∘ ·) id [f] = f.

Justus Willbad said:

5.) You used example and not theorem. Is your example my theorem?

example is the same as theorem but without a name provided, I used it because I did ont bother to find a name for the theorem. But you should use theorem if you want to be able to reuse it somewhere else.

Justus Willbad said:

6.) Lean prints "No goals". Does this mean my theorem is true?

No, here I wrote by sorry after the statement. sorry is a keyword saying "I do not prove this now I will prove it later, no need to raise an error". But I did not write a proof of the statement, I just wrote the statement.

[Justus Willbad]

Thanks. I understand that now. It seems cumbersome compared to mathematical language, but it works.

But how should the proof be formulated in Lean?

I have to introduce an equation f = fi ∘ g ∘ fj, rearrange it to fi_inv ∘ f = g ∘ fj, fi_inv ∘ f ∘ fj_inv = g and conclude that fi_inv ∘ f ∘ fj_inv ∈ F1.

[Etienne Marion]

It seems cumbersome mainly because iterating function composition is never written formally on paper. Also, before you get into the lean proof I'd suggest that you put more details in your paper proof. In particular you wrote that $F_1$ is closed under composition, but this is not true. You excluded constant compositions in $F_1$ so if I take functions in $F_0 \subset F_1$ such that their composition is constant I'll end up with a composition of functions in $F_1$ which is constant and thus not in $F_1$.

[Justus Willbad]

I made a mistake in defining $F1$ in my question above in contrast to my formulation at home. I corrected that now. $f_i$ and $f_j$ has to be non-conctant now.

Now I have the following.

import Mathlib
-- open List
variable {X : Type*} (F0 : List (X → X))
def F1 : Set (X → X) := {f | ∃ l, l ⊆ F0 ∧ ((f ∈ F0) ∨ f = l.foldr (· ∘ ·) id)}
variable (fi fj : X → X) (hfi : fi ∈ F1 F0) (hfj : fj ∈ F1 F0)
   (fi_inv fj_inv : X → X) (hfi_inv : fi_inv ∈ F1 F0) (hfj_inv : fj_inv ∈ F1 F0)
   (hi : Function.LeftInverse fi_inv fi) (hj : Function.RightInverse fj_inv fj)
   (g : X → X) (hg1 : ∃ x y, g x ≠ g y) (hg2 : g ∉ F1 F0)
theorem MyTheorem : fi ∘ g ∘ fj ∉ F1 F0 := by
 by_contra! assumption

What does ∈ F1 F0 mean? Does it mean that it is an element of both $F1$ and $F0$? I wanted to exclude $F0$ here, but Lean prints an error then.

[Etienne Marion]

Justus Willbad said:

What does ∈ F1 F0 mean?

This is a bit subtle if you are not used to it. In lean you can't introduce an object as a constant if it depends on parameters. In the definition of F1 I make use of F0 and this interpreted as saying that F1 is a function which given a list F0 outputs a set F1 F0. The notation F1 F0 is just saying that I am applying the function F1 to the list F0.

[Etienne Marion]

Here is a complete proof, you'll notice that some hypotheses were not needed.

import Mathlib.Data.List.Basic

open List Function

variable {X : Type*}

def F1 (F0 : List (X → X)) : Set (X → X) := {f | ∃ l, l ⊆ F0 ∧ f = l.foldr (· ∘ ·) id}

variable {F0 : List (X → X)}

lemma comp_mem_F1 {f g : X → X} (hf : f ∈ F1 F0) (hg : g ∈ F1 F0) : f ∘ g ∈ F1 F0 := by
  obtain ⟨lf, hlf, rfl⟩ := hf
  obtain ⟨lg, hlg, rfl⟩ := hg
  refine ⟨lf ++ lg, append_subset_of_subset_of_subset hlf hlg, ?_⟩
  induction lf with
  | nil => simp
  | cons a l hl =>
    rw [foldr_cons, cons_append, foldr_cons, comp_assoc, hl]
    exact subset_of_cons_subset hlf

theorem my_theorem (fi fj : X → X) (fi_inv fj_inv : X → X) (hfi_inv : fi_inv ∈ F1 F0)
  (hfj_inv : fj_inv ∈ F1 F0) (hi : LeftInverse fi_inv fi) (hj : RightInverse fj_inv fj)
  (g : X → X) (hg : g ∉ F1 F0) : fi ∘ g ∘ fj ∉ F1 F0 := by
  by_contra! h
  have := comp_mem_F1 (comp_mem_F1 hfi_inv h) hfj_inv
  rw [← comp_assoc, hi.id, comp_assoc, comp_assoc, hj.id] at this
  contradiction

[Justus Willbad]

I think I can now formulate simple theorems like mine myself. But I'm afraid that I will never be able to formulate such simple proofs on my own in Lean.

Can LeanCopilot and LeanDojo prove my theorem above automatically? Could you please try this is in Lean for me?

Can we use LeanCopilot and LeanDojo online?

[Kevin Buzzard]

Right now one hour of reading a reference like #mil will make you better at lean than any publically-available language model, so this would be a more productive use of your time.

[Justus Willbad]

Now I installed Lean with VSCode. But how can I get Mathlib? Lean prints "unknown module prefix 'Mathlib'".

[Daniel Weber]

See https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency

[Justus Willbad]

I asked these installing problems in another discussion here.

[Justus Willbad]

I asked these installing problems in another discussion.

[Justus Willbad]

The solutions above define only unary functions, but I have to consider unary and multiary functions (and their compositions).

How can I formulate the following mathematical objects in Lean?

Let $n\in\mathbb{N}$ and $S$ a set.

1.) $F$: the set of all unary and all multiary functions in $S$ (means the set of all unary and all multiary functions that map out from $S$ into $S$)

2.) for $n\in\mathbb{N}$, $f_1,...,f_n\in F$, $F_0=\{f_1,...,f_n\}$:
$F_1$: the set of all functions that are compositions of finite numbers of elements of $F_0$
Consider that $f_1,...f_n$ can be unary and multiary functions now.

[Daniel Weber]

Perhaps you should consider an inductive definition like docs#Nat.Partrec