Symmetric group

Stream: new members

[metakuntyyy]

Lately I have tried to figure out how permutations work.

I have figured out I can use Fin and Equiv.Perm to atleast get stuff working. But some things were just hard. Here is something I've played around with.

def a := 2

def b := Cycle.ofList [1,2,3]

#check b.next

def c := [[1,2,3],[2,1,3],[3,2,1]]
#eval c[3] 8

def d := (2:Fin 4)
#check d
def e := c[(1 : Fin 7), 2, 3] * c[0, 5]


def f := c[(2:Fin 5 ),1]

So I've played around a little bit with it but it seems that the Cycle generator doesn't want to work.
Also for some reason I can't index lists.

The point I want to make is eventually I want to define a function that depends on an upper size n and some value i. It maps some values based on i bijectively to 1 to n. And I want to show that this is actually a permutation.

Here is an example in prosa. Map 1 to i to n-i+1 to n and map i+1 to n to 1 to n-i.

What would be the steps to show that this is a permutation. I need to show bijection which means I would likely need to construct the inverse. In our case the inverse is quite easy to construct namel y map 1.. n-j to j+1.. n and map n-j+1..n to 1..j

However I don't know what the idiomatic lean way of writing this down is. Is it just defining a function and showing that it is an inverse or are you using some tools developed in Equiv.Perm.

[Martin Dvořák]

You probably want to write something like

#eval b.next sorry 1 sorry

where each sorry should be replaced by a proof.

[Martin Dvořák]

For example

import Mathlib

def b := Cycle.ofList [1,5,9,2,6,4,8,3,7]

#eval b.next (by simp [b]) 7 (by simp [b])

prints 1.

[metakuntyyy]

Thanks for the quick answer.

Ok hey that works, it evaluates that one correctly but I still fail to get why I need to prove it and what I need to prove.
You just used simp[b] and I fail to get what that accomplishes.

[metakuntyyy]

However it shows the correct result

[Martin Dvořák]

Look at the definition of the function you call. One of the arguments is a proof that there are no duplicates. The last argument is a proof that 7 is there.

[Martin Dvořák]

As an easy exercise, try to manually edit b so that; (1) the first proposition is false, (2) the second proposition is false, (3) both propositions are false; and observe what is underlined in red.

[Martin Dvořák]

You can also use by decide in place of either proof.

[metakuntyyy]

Ah got it. Assuming I want to feel pain, what would the manual proof look like? Let's say for a simple case of [1,2] I wanted to evaluate b.next sorry 1 sorry without using the tactics for learning purposes

[Martin Dvořák]

If you write

import Mathlib

def b := Cycle.ofList [1,2]

theorem nodup_b : b.Nodup := by simp [b]
#check nodup_b
#print nodup_b

the last line will give you something like

theorem b' : b.Nodup :=
of_eq_true
  (Eq.trans Mathlib.Data.List.Cycle._auxLemma.30
    (Eq.trans Mathlib.Data.List.Nodup._auxLemma.4
      (Eq.trans
        (congr
          (congrArg And
            (Eq.trans
              (congrArg Not
                (Eq.trans Init.Data.List.Lemmas._auxLemma.19 (Mathlib.Algebra.CharZero.Defs._auxLemma.10 2)))
              not_false_eq_true))
          (Eq.trans Mathlib.Data.List.Nodup._auxLemma.4
            (Eq.trans
              (congr (congrArg And (Eq.trans (congrArg Not (Init.Data.List.Lemmas._auxLemma.2 2)) not_false_eq_true))
                Mathlib.Data.List.Nodup._auxLemma.2)
              (and_self True))))
        (and_self True))))

which I have no interest in parsing or simplifying.

However, if you do

import Mathlib

def b := Cycle.ofList [1,2]

theorem nodup_b : b.Nodup := by decide
#check nodup_b
#print nodup_b

you will obtain the entire proof by computation.

PS: Do you know the difference between the following commands?

#check
#print
#eval

PPS: I have no idea why decide works on Cycle, which is Quotient. Let's wait for some experts to clarify.

[metakuntyyy]

Well check gives me the type, print I guess prints something and eval evaluates something. I guess the difference between print and eval might be vm execution but I've never looked into it.

EDIT: Actually I've tried print vs eval on def c:=3, eval just gives me the final value of 3 while print prints everything. I guess eval just reduces everything to a final value.

#eval b.next (by simp[b]) 1 (by simp[b]) works but #print b.next (by simp[b]) 1 (by simp[b]) does not.

I assume decidability is a very powerful tool in checking proofs as far as I have learned. Basically anything that you can "easily" reason about, anything that has a simple algorithm a computer can decide.
example : 10^9 < 2^30 := by decide this works and it's cool that it works. I guess when you can use the decidability you should.

Anyways back to my previous question: How do I now define parametrised permutations which are dependent on input size n? Do I just define a function and prove bijection, because I don't see how decidability will help me here.

[Martin Dvořák]

You can probably do something like:

def swap_halves_aux {n : ℕ} (a : Fin (2*n)) : Fin (2*n) :=
  if ha : a < n then
    ⟨a + n, by omega⟩
  else
    ⟨a - n, by omega⟩

lemma swap_halves_twice {n : ℕ} (x : Fin (2*n)) :
    swap_halves_aux (swap_halves_aux x) = x := by
  if hx : x < n then
    simp_all [swap_halves_aux]
  else
    sorry

def swap_halves (n : ℕ) : Equiv.Perm (Fin (2*n)) :=
  ⟨swap_halves_aux, swap_halves_aux, swap_halves_twice, swap_halves_twice⟩

I don't know what the idiomatic way is.

[metakuntyyy]

Oh wow so I've experimented a bit with it and I got the following

  if ha : a < i then
    ⟨n+a-i, by omega⟩

works but

  if ha : a < i then
    ⟨n+(a-i), by omega⟩

fails. This makes sense but it is so crazy. The fact that once you have subtraction things start to break down and that you have to worry much more about types. The first one works because apparently lean can prove that n+a-i<n because it can use the positive number i-a but the second fails because it can't use any number, as a-i gets calculated first and it can get rounded up to 0, which swallows the subtraction in some way.

Do I see that correctly?

[Ruben Van de Velde]

Pretty much

[metakuntyyy]

Wait, how would I then show for example that #check -1*-1 is a natural number. It only shows that the type is an integer. I never really understood how the coercions work. Once you have subtractions you better use Integers and once you have divisions you use Rationals.

Here is an example
example (a b : Int ) (h1: a < 0) (h2: b < 0) : ( (a*b):ℕ ) := by sorry
How could I show that a*b is a natural number?

[metakuntyyy]

As of right now this doesn't even compile, surely there is a way to assert that something has a type

[Ruben Van de Velde]

In informal mathematics, we tend to gloss over the fact that it's not really true that any natural number "is" an integer or that a nonnegative integer "is" a natural number. Lean forces you to be more explicit and say something like "there exists a natural number $n$ such that $(n \text{ seen as an integer}) = -1 \cdot -1$

[metakuntyyy]

example (a b : Int ) (ha: a < 0) (hb: b < 0) : ∃ n : ℕ ,(a*b =n )  := by
  use ( a*b).toNat
  have hc:  0< (a*b) := by exact Int.mul_pos_of_neg_of_neg ha hb
  have hd :  0≤  (a*b) := by exact Int.le_of_lt hc
  apply Int.toNat_of_nonneg at hd
  rw[hd]

Alright I have tried it. Would this suffice as a proof?

[Ruben Van de Velde]

Looks good!

[Martin Dvořák]

metakuntyyy said:

example (a b : Int ) (ha: a < 0) (hb: b < 0) : ∃ n : ℕ ,(a*b =n )  := by
  use ( a*b).toNat
  have hc:  0< (a*b) := by exact Int.mul_pos_of_neg_of_neg ha hb
  have hd :  0≤  (a*b) := by exact Int.le_of_lt hc
  apply Int.toNat_of_nonneg at hd
  rw[hd]

Alright I have tried it. Would this suffice as a proof?

Yes!

BTW, if you like terms, your proof is:

import Mathlib

example (a b : ℤ) (ha : a < 0) (hb : b < 0) : ∃ n : ℕ , a * b = n :=
  ⟨_, (Int.toNat_of_nonneg (Int.mul_pos_of_neg_of_neg ha hb).le).symm⟩

[metakuntyyy]

So let me try to recap and see if I understand correctly.
In lean types like the natural numbers and integers are a priori completely different. However in informal mathematics it is true that the natural numbers are a subset of the integers, that's why you can use a natural number where a integer is expected. Lean handles that with implicit coercions. Going in the other direction is impossible. Assuming an integer that is negative I can never show that the negative of this integer is a natural number. The only thing I can show is that the negative of this negative integer is positive, and then invoke a lemma that shows that this positive integer is equal to its projection to the natural number, proving the existence of a natural number equal to the negative of the negative integer.

As such moving from such types directly is never possible, once something has a type you need a type converting function or a coercion that embeds the smaller in the bigger set/type.

For example if we define the infinite sum from 0 to infinity of 1/2^k we could show that there exists a natural number (that is 2) which, when coerced to a real number is equal to this infinite sum. There is no way of getting the real converted back to a natural number. You can coerce to the bigger type: Like Nat->Int->Rat-> Real, and there are lemmas which make further usage of the bigger type helpful, but going back involves proofs that your number is actually of the subtype. For example 2:Int is positive, therefore (2:Nat)=(2:Int).toNat, which I can use to rewrite some lemmas.

Therefore one needs to be very mindful of the domain or the type one chooses as one can suddenly find himself in "type hell".

Is this recap good or am I missing something?

[Ruben Van de Velde]

Sounds like a good summary, yeah

[metakuntyyy]

Alright cool, now I have a follow up question before I go.
Assume I am doing an induction proof over natural numbers, where the statement is over the natural numbers, but for that proof I have to go to the rationals. Something like (a*b)<2^c where a,b,c:Nat. But the induction proof involves rationals. Can I formulate the statement over the naturals and then dip into rationals or do I directly have to type convert to rationals.

Assume I need the statement (a*b)\leq 2^c+1 eventually, which I'd be able to deduce if lhs and rhs are integers/natural numbers but not rational numbers.

How would I move forward, I need to dip into rationals to prove the first statement, but I can't use the second statement (Peano2) because I have proven the inequality for rationals. How would I resolve this issue.

Honestly this might be the most important question I have asked as I might learn more about how lean works from this one question than any other question.

It is also unfortunate albeit understandable that there are no type conversions. Coming from metamath it was really nice to just be able to use a natural number where an integer was expected. It was also possible to prove that an integer is a natural number by showing it is positive. I might have to wrap my head around it and try to find the most elegant way of popping in and out of types where needed.

[Bolton Bailey]

Seems like if you were doing induction on the naturals, then the thing to do would be to convert/dip into rationals after you had entered the inductive step of the proof.

[metakuntyyy]

So something like this?

theorem inductiveineq (x : ℕ ) (h1: 2 ≤ x) : (2^ (x+1)) < (choose (2*x+1) x) :=by
  induction' x, h1 using Nat.le_induction
  case base =>
    decide
  case succ y h1 ha =>
    have hah : (2^(x+1)) = ((2^x)*2):=by
      rw [pow_succ]
    have haf : choose (2*(x+1)+1) (x+1) = (choose (2*x+1) x)*(((2*x+2)/(x+1)):ℚ)*(((2*x+3)/(x+2)):ℚ):=by
      rw [choose_eq_factorial_div_factorial]
      simp
      sorry
    sorry

Note I am trying to prove
https://us.metamath.org/mpeuni/2ap1caineq.html
that I have successfully formalized in metamath.

[Bolton Bailey]

Likely a good example of this would be the formula for the sum 1^2 + 2^2 + ... + n^2 which I remember being in mathlib, but can't find.

[Bolton Bailey]

That code you posted doesn't compile

[Bolton Bailey]

Here

import Mathlib

open Nat

theorem inductiveineq (x : ℕ ) (h1: 2 ≤ x) : (2^ (x+1)) < (choose (2*x+1) x) :=by
  induction' x, h1 using Nat.le_induction
  case base =>
    decide
  case succ y h1 ha =>
    have hah : (2^(x+1)) = ((2^x)*2):=by
      rw [pow_succ]
    have haf : choose (2*(x+1)+1) (x+1) = (choose (2*x+1) x)*(((2*x+2)/(x+1)):ℚ)*(((2*x+3)/(x+2)):ℚ):=by
      rw [choose_eq_factorial_div_factorial]
      simp
      sorry
    sorry

[metakuntyyy]

Oh sorry, I've forgot to paste a minimal example.

[Bolton Bailey]

But yes, this strategy looks right

[metakuntyyy]

Alright so it's fine to dip into the rationals at haf?

Ah are there any helpful tactics that I can use. As of now I'd just do manual rewrites and following the proof that I have done in metamath. I am certain that this is so inefficient and that there are some powerful tactics like linarith, ring, maybe even field to convert those steps.

[Bolton Bailey]

A useful tactic might be push_cast at some point

[Bolton Bailey]

Thinking about this a bit harder, though, it should be possible to do this without any division via the use of Nat.add_choose_mul_factorial_mul_factorial, though I see why that's harder.

[Bolton Bailey]

Really, what we should have is a lemma like Nat.choose_eq_factorial_div_factorial but where the cast to rationals has already been applied to the LHS.

[Yaël Dillies]

Do you know about docs#pochhammer ?

[Yaël Dillies]

In particular, I proved docs#Nat.cast_choose_two a while ago

[Yaël Dillies]

... and I suspect docs#Nat.cast_choose_eq_ascPochhammer_div is exactly the lemma you want

[metakuntyyy]

No, I am using loogle, although that was also kinda hard to learn

[Bolton Bailey]

Yaël Dillies said:

... and I suspect docs#Nat.cast_choose_eq_ascPochhammer_div is exactly the lemma you want

Nice, I see Nat.cast_add_choose right above it is exactly the lemma I described.

[metakuntyyy]

I guess proving results by casting is important after all, am I seeing that correctly? Otherwise you aren't able to use the results for natural numbers

[metakuntyyy]

Cool, thank you guys for your help. I will try to work on it for a bit and report my progress in a few days.

[Bolton Bailey]

Hilariously, I actually think the hypothesis on Nat.cast_choose is unnecessary. If a > b then both sides are zero right?

[Yaël Dillies]

No, the LHS would be zero, but the RHS would still be b! / a!

[metakuntyyy]

Alright cool. Thank you very much. I've made some progress but I will share my attempt once I have exhausted my options. So far I am quite happy with my progress but I fail to instantiate the following

import Mathlib
open Nat
#check Nat.cast_choose ℚ (2≤3)
#check Nat.cast_factorial ℚ 2

The second one works but the first one does not. I am completely lost how to instantiate the first one. I want to have a theorem that says 2\le 3 -> ... but I fail to synthesise the instance.

[metakuntyyy]

My plan is to rewrite hypotheses and goals and lift them into the rationals.

[metakuntyyy]

import Mathlib

open Nat

#check Nat.cast_le
#check Nat.cast_choose ℚ
#check Nat.cast_factorial ℚ 2

example (h1: 2≤ 3) : a=a:=
  let h := Nat.cast_choose ℚ h1
  sorry

Actually this one works but how do I get one with the implication in a "proofless" context. It should be possible to partially apply the parameters to Nat.cast_choose

[metakuntyyy]

Nevermind, I got it. You need to construct a statement that has type 2\le 3 which means supplying it with a proof.

This one works.

import Mathlib

open Nat
#check Nat.cast_choose ℚ (Nat.zero_le 1)
#check Nat.cast_factorial ℚ 2


example :  0≤ 1 := by exact?