Zulip Chat Archive
Stream: new members
Topic: Symmetric group
metakuntyyy (Jun 17 2024 at 17:38):
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 (Jun 17 2024 at 17:45):
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 (Jun 17 2024 at 17:47):
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 (Jun 17 2024 at 17:48):
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 (Jun 17 2024 at 17:48):
However it shows the correct result
Martin Dvořák (Jun 17 2024 at 17:50):
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 (Jun 17 2024 at 17:52):
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 (Jun 17 2024 at 17:53):
You can also use by decide
in place of either proof.
metakuntyyy (Jun 17 2024 at 17:55):
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 (Jun 17 2024 at 18:00):
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 (Jun 17 2024 at 18:14):
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 (Jun 17 2024 at 18:35):
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 (Jun 17 2024 at 18:58):
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 (Jun 17 2024 at 19:04):
Pretty much
metakuntyyy (Jun 17 2024 at 19:18):
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 (Jun 17 2024 at 19:18):
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 (Jun 17 2024 at 19:34):
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 such that
metakuntyyy (Jun 17 2024 at 20:55):
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 (Jun 17 2024 at 20:56):
Looks good!
Martin Dvořák (Jun 17 2024 at 21:03):
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 (Jun 17 2024 at 21:11):
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 (Jun 17 2024 at 21:16):
Sounds like a good summary, yeah
metakuntyyy (Jun 17 2024 at 21:32):
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 (Jun 17 2024 at 21:48):
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 (Jun 17 2024 at 21:51):
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 (Jun 17 2024 at 21:52):
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 (Jun 17 2024 at 21:52):
That code you posted doesn't compile
Bolton Bailey (Jun 17 2024 at 21:53):
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 (Jun 17 2024 at 21:53):
Oh sorry, I've forgot to paste a minimal example.
Bolton Bailey (Jun 17 2024 at 21:54):
But yes, this strategy looks right
metakuntyyy (Jun 17 2024 at 21:55):
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 (Jun 17 2024 at 22:02):
A useful tactic might be push_cast at some point
Bolton Bailey (Jun 17 2024 at 22:04):
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 (Jun 17 2024 at 22:05):
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 (Jun 17 2024 at 22:07):
Do you know about docs#pochhammer ?
Yaël Dillies (Jun 17 2024 at 22:07):
In particular, I proved docs#Nat.cast_choose_two a while ago
Yaël Dillies (Jun 17 2024 at 22:08):
... and I suspect docs#Nat.cast_choose_eq_ascPochhammer_div is exactly the lemma you want
metakuntyyy (Jun 17 2024 at 22:08):
No, I am using loogle, although that was also kinda hard to learn
Bolton Bailey (Jun 17 2024 at 22:14):
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 (Jun 17 2024 at 22:16):
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 (Jun 17 2024 at 22:17):
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 (Jun 17 2024 at 22:21):
Hilariously, I actually think the hypothesis on Nat.cast_choose
is unnecessary. If a > b then both sides are zero right?
Yaël Dillies (Jun 17 2024 at 22:22):
No, the LHS would be zero, but the RHS would still be b! / a!
metakuntyyy (Jun 19 2024 at 18:11):
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 (Jun 19 2024 at 18:11):
My plan is to rewrite hypotheses and goals and lift them into the rationals.
metakuntyyy (Jun 19 2024 at 18:31):
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 (Jun 19 2024 at 19:08):
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?
Last updated: May 02 2025 at 03:31 UTC