Set of all compositions of given multivariate functions II

Stream: new members

[Justus Willbad]

Now I have the following from GitHub Copilot.
How can it be corrected?

theorem Theorem1a (X0 : Set X) (f : Fin n → X → X)
  (F0 : Set (X → X) := {g | ∃ i, g = f i})
  (F : Set (X → X) := {g | ∃ (l : List (X → X)), (∀ h ∈ l, h ∈ F0) ∧ g = List.foldr (· ∘ ·) id l})
  (X1 : Set X := {x | ∃ g ∈ F, ∃ y ∈ X0, x = g y})
  (f : X → X) (hf : f ∈ F) (x0 : X) (hx0 : x0 ∈ X1) : f x0 ∈ X1 := by
   rcases hx0 with ⟨h, hF, y, hy, rfl⟩
   use [f ∘ h, ⟨f, hf, h, hF, rfl⟩, y, hy]
   rfl

Lean prints:

rcases tactic failed: hx0 : X1 x0 is not an inductive datatype

[Aaron Liu]

You have many parameters like ([name] : [Type] := [value]). This means to supply [value] as the default value for [name] if the user does not specify one. This does not mean "let [name] be a [Type] with value [value]". If you meant this instead, I would recommend substituting through your F0, F, and X1.

[Justus Willbad]

1.) I don't know how to do this.
2.) What does it mean that Lean prints "No goals", but also the error note?
3.) Which command do I have to replace the rcase command with?

[Aaron Liu]

You haven't posted a #mwe, so I don't know if this will work or not, but you can try this

theorem Theorem1a (X0 : Set X) (f : Fin n → X → X)
  (f' : X → X) (hf : f' ∈ {g | ∃ (l : List (X → X)), (∀ h ∈ l, h ∈ {g | ∃ i, g = f i}) ∧ g = List.foldr (· ∘ ·) id l}) (x0 : X) (hx0 : x0 ∈ {x | ∃ g ∈ {g | ∃ (l : List (X → X)), (∀ h ∈ l, h ∈ {g | ∃ i, g = f i}) ∧ g = List.foldr (· ∘ ·) id l}, ∃ y ∈ X0, x = g y}) : f' x0 ∈ {x | ∃ g ∈ {g | ∃ (l : List (X → X)), (∀ h ∈ l, h ∈ {g | ∃ i, g = f i}) ∧ g = List.foldr (· ∘ ·) id l}, ∃ y ∈ X0, x = g y} := by
   rcases hx0 with ⟨h, hF, y, hy, rfl⟩
   use [f' ∘ h, ⟨f', hf, h, hF, rfl⟩, y, hy]
   rfl

or this

theorem Theorem1a (X0 : Set X) (f : Fin n → X → X) :
  let F0 : Set (X → X) := {g | ∃ i, g = f i}
  let F : Set (X → X) := {g | ∃ (l : List (X → X)), (∀ h ∈ l, h ∈ F0) ∧ g = List.foldr (· ∘ ·) id l}
  let X1 : Set X := {x | ∃ g ∈ F, ∃ y ∈ X0, x = g y}
  (f : X → X) → (hf : f ∈ F) → (x0 : X) → (hx0 : x0 ∈ X1) → f x0 ∈ X1 := by
   intro F0 F x1 f hf x0 hx0
   rcases hx0 with ⟨h, hF, y, hy, rfl⟩
   use [f ∘ h, ⟨f, hf, h, hF, rfl⟩, y, hy]
   rfl

[Aaron Liu]

Note that it is discouraged to have lets in the theorem statement.

[Justus Willbad]

Both produce a lot of Lean error notes (Type mismacth and other).
I used import Mathlib.

[Aaron Liu]

Can you post a #mwe, so I know exactly which problems you're having?

[Justus Willbad]

See my code in the first post on the top and type in import Mathlib before.

[Aaron Liu]

The syntax of the use command doesn't use brackets. What were you intending by use [f ∘ h, ⟨f, hf, h, hF, rfl⟩, y, hy]?

[Justus Willbad]

I know neither tactics nor their syntax. The tactics came from GitHub Copilot. But that's horrible: it's for Lean 3 and I don't know the syntax of lean 3 and 4.

[Aaron Liu]

If you're on VSCode (or the web editor), you can hover over the text use and hopefully it will display a docstring explaining the tactic's purpose, syntax, and use.

[Justus Willbad]

I already found this, but that doesn't help if GitHub Copilot gives the working command rcase and Lean prints the error note

rcases tactic failed: hx0 : X1 x0 is not an inductive datatype

I don't know if this is really an error becuse Lean print "No goals".

[Aaron Liu]

This is because X1 could be anything! How do you know X1 x0 is an inductive datatype?

[Aaron Liu]

Basically, what is you reasoning for being able to do cases on the inhabitants of X1 x0?

[Justus Willbad]

I know neither tactics nor their syntax. The tactics came from GitHub Copilot. I want to learn Lean from these example proofs.
I don't know what X1 x0 mean and where it comes from.
I don't know if this is really an error becuse Lean print "No goals".
In fact, I want a proof without error comments.

[Aaron Liu]

What are you trying to prove exactly? Please write it out in words, because I don't think the Lean code that you gave me accurately reflects what you are trying to prove.

[Ilmārs Cīrulis]

I would suggest to change your approach towards learning Lean.
Throw Copilot in trash bin for now, if possible, but the main point is --- choose something simpler to tinker with / learn from.

My two cents... :sweat_smile:

[Justus Willbad]

I assumed GitHub translated it correctly from TEX to Lean, I think I understand the Lean 4 code.

Theorem1:
Let
$n\in\mathbb{N}_+$,
$X$ a set,
$X_0\subseteq X$,
$f_1,...,f_n\colon X\to X$,
$F_0=\{f_1,...,f_n\}$,
$F$ the set of all compositions of finite numbers of elements of $F_0$,
$X_1=\{f(x)\ |\ \forall f\in F, x\in X_0\}$,
$f\in F$
$x_0\in\mathrm{dom}(f)$.
a) $x_0\in X_1\implies f(x_0)\in X_1$
b) $f(x_0)\notin X_1\implies x_0\notin X_1$

[Aaron Liu]

(deleted)

[Justus Willbad]

Lean uses (f : Fin n → X → X)). Can I still use my variable names f and f₁ despite this?

[Aaron Liu]

Is this what you want?

import Mathlib

set_option autoImplicit false -- the cause of 30% of all problems (at the beginner level)

universe u
-- Let `n` ∈ ℕ₊, let `X` be a set, let `X₀` ⊆ `X`, let `f 0`, ..., `f (n - 1)` : `X → X`
variable {n : Nat} (hn : 0 < n) {X : Type u} (X₀ : Set X) (f : Fin n → Function.End X)

-- Let `F f` be set of finite compositions of `{f 0, f 1, ..., f (n - 1)}`
abbrev F : Set (Function.End X) := {f₁ | Monoid.InClosure (Set.range f) f₁}

-- Let `X₁ = {f₁ x | f₁ ∈ F f, x₀ ∈ X₀}`
abbrev X₁ : Set X := Set.seq (F f) X₀

-- Let `f₁` ∈ `F f`, let `x₀` ∈ dom(`f₁`)
variable {f₁ : Function.End X} (hf₁ : f₁ ∈ F f) (x₀ : X)

-- include hn in -- uncomment this line if you end up needing `hn : 0 < n`
theorem Theorem1a (hx₀ : x₀ ∈ X₁ X₀ f) : f₁ x₀ ∈ X₁ X₀ f := by
  -- fill in your proof here
  sorry

theorem Theorem1b (hx₀ : f₁ x₀ ∉ X₁ X₀ f) : x₀ ∉ X₁ X₀ f :=
  -- modus tollens
  mt (Theorem1a X₀ f x₀) hx₀

[Justus Willbad]

I don't know what X₀ f means in the theorem rows.

[Abraham Solomon]

Aaron Liu said:

This is because X1 could be anything! How do you know X1 x0 is an inductive datatype?

To be fair every type in Lean is an inductive type, for theorem proving.

[Aaron Liu]

Since the definition of X₁ depends on X₀ and f, and definitions must be self-contained, X₀ and f were abstracted out of X₁, so X₁ is a function that takes as input a X₀ and a f and returns {f₁ x | f₁ ∈ F f, x₀ ∈ X₀}.

[Aaron Liu]

Abraham Solomon said:

Aaron Liu said:

This is because X1 could be anything! How do you know X1 x0 is an inductive datatype?

To be fair every type in Lean is an inductive type, for theorem proving.

Quotient types, function types, type universes (like Prop, Type, ...) and types obtained using Classical.choice aren't inductive.

[Abraham Solomon]

Aaron Liu said:

Abraham Solomon said:

Aaron Liu said:

This is because X1 could be anything! How do you know X1 x0 is an inductive datatype?

To be fair every type in Lean is an inductive type, for theorem proving.

Quotient types and function types aren't inductive.

To quote:
'In fact, in Lean's library, every concrete type other than the universes and every type constructor other than dependent arrows is an instance of a general family of type constructions known as inductive types'

So only function types i think.

https://leanprover.github.io/theorem_proving_in_lean4/inductive_types.html

[Abraham Solomon]

Aaron Liu said:

Abraham Solomon said:

Aaron Liu said:

This is because X1 could be anything! How do you know X1 x0 is an inductive datatype?

To be fair every type in Lean is an inductive type, for theorem proving.

Quotient types, function types, type universes (like Prop, Type, ...) and types obtained using Classical.choice aren't inductive.

This isnt true, you can use choice to get a type of any kind from an exists statement. But sure.

[Aaron Liu]

If you #print Quot, you'll see that docs#Quot is actually a "Quotient primitive" which is built into Lean and defined using a special command called init_quot.

[Justus Willbad]

It's too late today for me to understand the special Lean functions used in the code.
GitHub CoPilot gave again a proof with a lot of error notes that I don't understand.

[Abraham Solomon]

Justus Willbad said:

It's too late today for me to understand the special Lean functions used in the code.
GitHub CoPilot gave again a proof with a lot of error notes that I don't understand.

AI is generally just not good at lean, and thats also partly because lean goes through huge changes from lean 1 to 4. Its trained on everything on github and Lean is very particular, Lean 4 being fairly new.

You should try going through Mathematics in Lean because that one has human written solutions and comments.

[Justus Willbad]

Abraham Solomon wrote:

AI is generally just not good at lean, and thats also partly because lean goes through huge changes from lean 1 to 4. Its trained on everything on github and Lean is very particular, Lean 4 being fairly new.

Is GitHub Copilot better with HOL, Coq, Isabelle?

[Kevin Buzzard]

I have had no experience with these systems but the fact that those languages are far more stable than Lean is probably a plus point as far as language models are concerned.

I might also comment that your questions here over the last few months seem to indicate that you are very much focussed on thinking about mathematics from a set-theoretic perspective so you might want to contemplate trying a set-theory-based prover such as Mizar or Isabelle/ZFC if you are going to experiment with other systems.