Design a tactic to find a finite set?

Stream: new members

[Laurent Bartholdi]

Sorry the title is very unclear -- I would very much like lean to be able to automatically solve a goal of the following form (a contrived M(N)WE).

In words: with fin sets, define the orbit of a point under a function. Then have Lean/mathlib automatically deduce that some other point belongs to the orbit. For a mathematician, this means starting from the singleton {point} and applying repeatedly the function till the orbit doesn't increase; then check whether the other point belongs to that set.

import analysis.special_functions.log
-- to have ⋂₀. Certainly not the minimal import, but what's in my current code

namespace test

variables {X : Type}

def orbit (f : X → X) (x : X) : set X := ⋂₀{O | x∈O ∧ ∀(x∈O), f(x)∈O}

def reaches (f : X → X) (x y : X) : Prop := y∈(orbit f x)

def myf : fin 4 → fin 4 := ![0,0,1,2]

theorem wow : reaches myf 3 0 := begin -- ideally, this would be "by mysimp" or "by simp[mymethod]"
    intros O h,
    have h3 : (3 : fin 4) ∈ O, by finish,
    have h2 : (2 : fin 4) ∈ O, by finish,
    have h1 : (1 : fin 4) ∈ O, by finish,
    finish
end

theorem wow2 : ¬ reaches myf 0 3 := sorry

end test

[Damiano Testa]

If all you care is the case in which X is fin n for some concrete n, like in your example where n = 4, then dec_trivial should be able to help.

However, though I might be wrong, your definition of orbit is "too abstract". Something like ∃ a : fin n, f^[a] x = y might work better.

Note that the existential is over a fin, (in this case, the same fin n where x y also live is enough).

[Damiano Testa]

When I said "too abstract" I meant "too abstract for dec_trivial to help". Of course, yours is perfectly valid!

[Damiano Testa]

With the quantification that I propose, the problem is clearly "finite".

[Damiano Testa]

For instance, this works:

variables {n : ℕ}

def fin_orbit (f : fin n → fin n) (x : fin n) : set (fin n) :=
{ y | ∃ (m : fin n), f^[m] x = y }

def fin_reaches (f : (fin n) → (fin n)) (x y : fin n) : Prop :=
y ∈ fin_orbit f x

def myf : fin 4 → fin 4 := ![0,0,1,2]

theorem wow : fin_reaches myf 3 0 :=
begin
  unfold fin_reaches myf fin_orbit,
  dec_trivial,
end

theorem wow2 : ¬ fin_reaches myf 0 3 :=
begin
  unfold fin_reaches myf fin_orbit,
  dec_trivial,
end

[Damiano Testa]

On the side, you would have to prove something like

lemma fin_orbit_eq_orbit (f : (fin n) → (fin n)) (x : fin n) : fin_orbit f x = orbit f x :=
sorry

to convert your definition of orbit into the fin_orbit that works with dec_trivial.

[Yakov Pechersky]

fin_orbit is related to docs#equiv.perm.cycle_of

[Laurent Bartholdi]

Thanks for all the feedback! However, I should have stated that this is really a MWE.

In my "real-life" situation, I'm not interating a map such as myf, but really a map on sets (or at least a map X\times Y\to X, treated as a collection of Y maps whose global orbit I am interested in.

In the cases I have in mind, I don't think I can avoid quantifying over a subset. However, as in @Damiano Testa's suggested answer, I can bound the number of iterations till the set stabilizes by #X.

[Alex J. Best]

I think whatever you are asking for is certainly possible as a tactic, provided lean has a way to normalize applications of the function you want the orbit of. This could either be through carefully chosen simp lemmas, or the function itself could be computable.
The first step of building most tactics though should be to produce a few proofs that do exactly what you want the tactic to do, in a rigid style so its clear exactly what the tactic will and will not do when it is called.
Then sometimes it becomes clear that the tactic is a combination of existing things such as norm_num and maybe some carefully chosen repeat and try statements, or it may be complicated enough that an actual procedure needs to be written in the tactic monad.

[Laurent Bartholdi]

Thanks @Alex J. Best ! I think what I really would like is the automatic computation of the orbits of semigroups acting on fin n. Here's a more detailed example (which however I haven't been able to complete cleanly, still lots of sorries): that of a 2-generated semigroup acting on fin 4, consisting of the two constant maps 0 and 2. (of course this is just for testing purposes). Prove that 0 is reachable from 3, by proving that the orbit of 3 is {0,2,3}.

The way a human would do it is start by {3} and keep applying all generators to enlarge the set; when it doesn't enlarge anymore, we found the orbit.

import analysis.special_functions.log

namespace test

variables {X Y : Type}

def orbit (f : Y → X → X) (x : X) : set X := ⋂₀{O | x∈O ∧ ∀(x∈O) y, f y x∈O}

def reaches (f : Y → X → X) (x y : X) : Prop := y∈(orbit f x)

def myf : fin 2 → fin 4 → fin 4 := ![![2,2,2,2],![0,0,0,3]]

lemma start (f : Y → X → X) (x : X) : {x} ⊆ orbit f x := begin
    intros _ h _ hO,
    rw set.eq_of_mem_singleton h,
    exact hO.1
end

lemma extend (f : Y → X → X) (x : X) (O : set X) : O ⊆ orbit f x → (O ∪ ⋃(y : Y), (f y) '' O) ⊆ orbit f x := begin
    intros h x' k,
    cases k,
    { exact h k },
    { rw set.mem_Union at k, cases k, cases k_h, sorry }
end

lemma foundorbit (f : Y → X → X) (x : X) (O : set X) : O ⊆ orbit f x → x ∈ O → ∀(y : Y), f y '' O ⊆ O → O = orbit f x := begin
    sorry
end

theorem myf_orbit3 : orbit myf 3 = {0,2,3} := begin
    have iter1 : ({3} : set (fin 4)) ⊆ orbit myf 3, exact start myf 3,
    have iter2 : ({2,3} : set (fin 4)) ⊆ orbit myf 3, { let temp := extend myf 3 {3} iter1, rw myf at temp, finish },
    have iter3 : ({0,2,3} : set (fin 4)) ⊆ orbit myf 3, exact extend myf 3 {2,3} iter2,
    exact foundorbit myf 3 {0,2,3} iter3 iter1 (by sorry)
end

theorem wow : reaches myf 3 0 := begin
    rw reaches,
    rw myf_orbit3,
    norm_num,
end

end test