rewriting n-1+1=n

Stream: new members

[Ritwick Bhargava]

Hi everyone, I'm working on some results related to Tits' theorem in $S_n$, dealing with reduced words of permutations. If a permutation has type equiv.perm (fin n), then I find it natural for reduced words to have type list (fin (n-1)), but this back and forth from n to n-1 can sometimes get messy.
I've included below an MWE for some problems I've been having chaining results together: for some reason, I just can't use the fact that n-1+1 = n in the proof of mylemma. I've put a sorry on things where only the type is relevant.

import tactic
open equiv

def red_wrd (n: ℕ) : perm (fin n)→ list (fin (n-1)) := sorry

def perm_of_list (n: ℕ) : list (fin (n-1)) → perm (fin n) :=  sorry

lemma l_inv (n: ℕ) : ∀π, perm_of_list n (red_wrd n π) = π:= sorry

lemma comparing_lists (n: ℕ) (u v: list (fin n)):
 perm_of_list (n+1) u =perm_of_list (n+1) v → u.length =v.length := sorry

lemma mylemma (n: ℕ) (π: perm (fin n)) (l: list (fin (n-1))) (h1: n-1+1 =n) (h2: perm_of_list n l =π):
  l.length = (red_wrd n π).length :=
begin
apply comparing_lists (n-1) l  (red_wrd n π),
--WTS perm_list (n - 1 + 1) l = perm_list (n - 1 + 1) (red_wrd n π), but can't use l_inv or even h2
--rw h, gives "rewrite tactic failed, motive is not type correct"
--simp_rw h, gives "simplify tactic failed to simplify"
sorry,
end
--lemma helper  (n:ℕ)  (h:n-1+1=n) : perm_list n = perm_list (n-1+1) := sorry
-- lean complains if I try to factor this out as a sublemma

Do you have any comments or suggestions on how to deal with this?

[Alex J. Best]

Does setting it up like this to avoid the problem work for you?

import tactic
open equiv

def red_wrd (n: ℕ) : perm (fin n)→ list (fin (n-1)) := sorry

def perm_of_list (n: ℕ) : list (fin (n-1)) → perm (fin n) :=  sorry

lemma l_inv (n: ℕ) : ∀π, perm_of_list n (red_wrd n π) = π:= sorry

lemma comparing_lists (n: ℕ) (u v: list (fin (n-1))):
 perm_of_list (n) u =perm_of_list (n) v → u.length =v.length := sorry

lemma mylemma (n: ℕ) (π: perm (fin n)) (l: list (fin (n-1))) (h1: n-1+1 =n) (h2: perm_of_list n l =π):
  l.length = (red_wrd n π).length :=
begin
apply comparing_lists (n) l  (red_wrd n π),
rw h2,
rw l_inv,
end
--lemma helper  (n:ℕ)  (h:n-1+1=n) : perm_list n = perm_list (n-1+1) := sorry
-- lean complains if I try to factor this out as a sublemma

[Alex J. Best]

Here I just changed the type of comparing_lists, but seeing as I didnt think about the mathematics maybe you need to add a side condition to that

[Ritwick Bhargava]

Yeah, that does work in the MWE, and I have tried just changing the type of the lemmas, but this kind of just shifts the problem around (i.e. if I change the type of one lemma, then something else breaks/ becomes incompatible). I think at some point in the document there needs to be a full circuit n -> n-1 -> n-1+1 =n which is why I was kinda hoping for a solution with the types unchanged (part of the hypothesis in all this is that n>0 so n-1+1 =n is actually true)

[Stuart Presnell]

If you have hn : 0 < n then nat.sub_add_cancel hn : n - 1 + 1 = n

[Junyan Xu]

If you use n+1 and n instead of n and n-1 the problem probably disappear, since n+1-1=n (and obviously n+1=n+1) is defeq.

[Ritwick Bhargava]

Yep, I'm just including (h:n-1+1=n) as the hypothesis to simplify the MWE
Stuart Presnell said:

If you have hn : 0 < n then nat.sub_add_cancel hn : n - 1 + 1 = n

[Yakov Pechersky]

One of the reasons you're having trouble is that n-1+1 != n for all n < 1

[Yakov Pechersky]

In the way that nat subtraction is defined

[Ritwick Bhargava]

I guess I was just hoping that having the n-1+1=n in the environment would mean that the identification of fin (n-1+1) with fin n would be relatively easy

[Ritwick Bhargava]

Junyan Xu said:

If you use n+1 and n instead of n and n-1 the problem probably disappear, since n+1-1=n (and obviously n+1=n+1) is defeq.

This makes sense, I think I'll give this a try - thanks!

[Patrick Johnson]

Ritwick Bhargava said:

I guess I was just hoping that having the n-1+1=n in the environment would mean that the identification of fin (n-1+1) with fin n would be relatively easy

In theory, you should be able to just rw h1 and it should work, but the rw tactic is not smart enough to handle this situation. Alternatively, you can construct the eq.rec motive manually, but it may be painful.

[Violeta Hernández]

The problem here is that for l : perm (n - 1), Lean can't deduce that perm_of_list n l is well-typed, since it doesn't know that (n - 1) + 1 = n just by looking at the expression

[Violeta Hernández]

The easiest way out of this is to use types n + 1 and n instead of n and n - 1. Since (n + 1) - 1 = n is a definitional equality, you won't have these sorts of type problems

import tactic
open equiv

def red_wrd (n : ℕ) : perm (fin (n + 1)) → list (fin n) := sorry

def perm_of_list (n : ℕ) : list (fin n) → perm (fin (n + 1)) := sorry

lemma l_inv (n : ℕ) : ∀ π, perm_of_list n (red_wrd n π) = π := sorry

lemma comparing_lists (n : ℕ) (u v : list (fin n)) :
  perm_of_list n u = perm_of_list n v → u.length = v.length := sorry

lemma mylemma (n : ℕ) (π : perm (fin (n + 1))) (l : list (fin n)) (h2 : perm_of_list n l = π) :
  l.length = (red_wrd n π).length :=
begin
  apply comparing_lists n l (red_wrd n π),
  rw [l_inv, h2]
end

[Violeta Hernández]

If you insist on your current approach, you'll have to get comfortable with heterogeneous equality.

import tactic
open equiv

def red_wrd (n : ℕ) : perm (fin n) → list (fin (n - 1)) := sorry

def perm_of_list (n : ℕ) : list (fin (n - 1)) → perm (fin n) := sorry

lemma l_inv (n : ℕ) : ∀ π, perm_of_list n (red_wrd n π) = π := sorry

lemma comparing_lists (n : ℕ) (u v : list (fin n)):
  perm_of_list (n + 1) u = perm_of_list (n + 1) v → u.length = v.length := sorry

lemma mylemma (n : ℕ) (π : perm (fin n)) (l : list (fin (n - 1))) (h1 : n - 1 + 1 = n)
  (h2 : perm_of_list n l = π) : l.length = (red_wrd n π).length :=
begin
  apply comparing_lists (n - 1) l (red_wrd n π),
  convert h2,
  convert heq_of_eq (l_inv n π)
end

[Violeta Hernández]

The convert tactic makes its best effort to convert one proof into another by matching what it thinks are corresponding terms. It's able to use proofs from the context, which is why you don't have to explicitly call h1

[Ritwick Bhargava]

Thanks a lot for the detailed answer! I guess using n+1 instead of n is the simplest solution even though I prefer the latter for aesthetic reasons.

[Ritwick Bhargava]

What exactly is heterogeneous equality, and is there a reason to avoid it?

[Violeta Hernández]

n - 1 just isn't nearly as well behaved as n + 1. In fact, succ n = n + 1 is a constructor for the naturals, you can't get much better behaved than that.

[Ma, Jia-Jun]

Ritwick Bhargava said:

Thanks a lot for the detailed answer! I guess using n+1 instead of n is the simplest solution even though I prefer the latter for aesthetic reasons.

I encounter a similar problem when dealing with S_n.

[Violeta Hernández]

Heterogeneous equality is equality between terms of types Lean can't necessarily prove equal definitionally. If you're using it, as a rule of thumb, something is going wrong.

[Junyan Xu]

Another way would be to use docs#fin_congr to turn equality into bijection.

[Eric Wieser]

I had no idea fin_congr h existed, I've been using (fin.cast h).to_equiv everywhere