How to evaluate ite?

Stream: new members

[Ma, Jia-Jun]

I am new to Lean and trying to formalize some proofs in my paper (starting from some very basic stuffs)
In the tactic mode, I get the goal as the following:
image.png

Then I got no idea how to proceed. There are at least two obstructions to me.

1. how to treat "ite" ? (clearly one must use -1 \neq 1)
2. how to treat _match_2 ?

It seems there are no documents on these two points.

Thanks.

[Eric Wieser]

Can you share a #mwe that includes your definition of mat_mul?

[Eric Wieser]

docs#if_neg will let you eliminate the third ite

[Ma, Jia-Jun]

Eric Wieser said:

Can you share a #mwe that includes your definition of mat_mul?

image.png
I am trying to define the structure of monomial_matrix (over the coefficient ring int, for simplicity), mat_mul is the multiplication of two monomail_matrix.

The code is attached. Thanks.
test.lean

[Eric Wieser]

Can you paste the code here in #backticks rather than attaching it?

[Ma, Jia-Jun]

Eric Wieser said:

Can you paste the code here in #backticks rather than attaching it?

-- basis of V_l are {v_i} R=integer
-- a scalar of a basis vector c_i v_i is identified with (c_i, i)R × int

-- A lifting of simple refelection is a map int -> R × int
structure monomial_matrix  :=
mk  ::  (mat: int -> int × int)

def mat_mul (w : monomial_matrix) (wp : monomial_matrix) : monomial_matrix :=
  monomial_matrix.mk
    (λ j,
        let (cwp_j, wp_j) := (wp.mat j) in
        let (cw_wp_j, w_wp_j) := (w.mat wp_j)
          in (cw_wp_j * cwp_j, w_wp_j))

def t (i : nat) : monomial_matrix :=
  monomial_matrix.mk
  (λ (j: int),
    if j = i then (-1, -i) else
    if j = -i then (-eps, i)
    else (1,j))

-- The idenetity map
def id_mat : monomial_matrix :=
  monomial_matrix.mk (λ j, (1,j))

infixl ` * `:75 := mat_mul

example : (mat_mul (t 1) (t 1)).mat (-1) = (eps, -1) := begin
  rw mat_mul,
  rw t,
  simp,

end

[Eric Wieser]

Make sure to read #backticks (that's a link)

Edit: ah, you need a second set of backticks because the first set is part of the ```quote ``` syntax; you used the ``` that was inserted automatically by the quotation, and didn't actually type new ones for the code.

[Eric Wieser]

The _match terms are being generated by your use of let (cw_wp_j, w_wp_j) := (w.mat wp_j)

[Eric Wieser]

If you use let w_wp := (w.mat wp_j) and w_wp.1, w_wp.2 instead, then they will go away

[Ma, Jia-Jun]

Eric Wieser said:

If you use let w_wp := (w.mat wp_j) and w_wp.1, w_wp.2 instead, then they will go away

Just updated the code.

[Kevin Buzzard]

If you import tactic then you can use split_ifs which does all the dirty work for you:

example : (mat_mul (t 1) (t 1)).mat (-1) = (eps, -1) := begin
  simp [mat_mul, t],
  split_ifs;
  simp,
  cases h,
end

[Ma, Jia-Jun]

Kevin Buzzard said:

If you import tactic then you can use split_ifs which does all the dirty work for you:

example : (mat_mul (t 1) (t 1)).mat (-1) = (eps, -1) := begin
  simp [mat_mul, t],
  split_ifs;
  simp,
  cases h,
end

Thanks. Like magic :tada: .
Why split_ifs ends with ";" instead of ", " ?

[Anne Baanen]

; means "apply the following tactic to all goals created by the previous"

[Anne Baanen]

So I assume in this case we want to simplify both the positive and negative outcome of the if statement.

[Kevin Buzzard]

Maybe this is a clearer proof:

example : (mat_mul (t 1) (t 1)).mat (-1) = (eps, -1) := begin
  simp [mat_mul, t],
  split_ifs with h,
  { cases h, },
  { simp, },
end

[Eric Wieser]

Or an even clearer proof:

example : (mat_mul (t 1) (t 1)).mat (-1) = (eps, -1) := begin
  have : (-1 : ℤ) ≠ 1 := dec_trivial,
  simp [mat_mul, t, this],
end

[Ma, Jia-Jun]

Now I am trying to prove something more complex.
Basically, I want to verify certain listings in GL_n of simple reflections of a Weyl satisfy the braid relation.

I have edited my original question to include the codes.
Here is the relevant part.

-- The definition of s_i
def s (i : nat) : monomial_matrix :=
  monomial_matrix.mk
  (λ (j: int),
    if j = i then (- eps , i+1) else
    if j = i+1 then (eps, i) else
    if j = -(i+1) then (eps,-i) else
    if j = -i then (- eps, -(i+1)) else
    (1,j))

-- s_i s_{i+1} s_i = s_{i+1} s_i s_{i+1}
-- i≠ 0, j≠ 0
lemma s_i_s_ip_s_i_eq_s_ip_s_i_s_ip
  (i : nat) (j : int) (hi : -(i:int) ≠ (i:int)) (hj : -j≠ j)
  :
  ((s i) * (s (i+1)) * (s i)).mat j = ((s (i+1) ) * (s i) * (s (i+1))).mat j
  :=
begin
  simp [mat_mul, s, hi, hj],
  split_ifs,

end

Here are the problems:

1. split_ifs runs timeout by default (and my VS code go crush :sweat_smile: ) , and I removed the time limitation.
2. after split_ifs, it give 859 goals to solve but most goals include a hypothesis such as

h: i+1 +1 = i

which is clearly false.
So my question is:

1. Is there a better way to rewrite the definition of s_i so that number of cases can be reduced.
2. Is there some way to automatically eliminate the goal containing false assumptions.
3. Although I known how to disprove i+1+1 =1 in the natural number game, I still don't know how to solve it effectively using lean/mathlib.

Thanks.

[Ruben Van de Velde]

Ouch, that looks like a pretty extreme case. Is there a lemma called something like lt_succ_succ that you could use with ne_of_gt?

[Eric Wieser]

I think probably the way to do this is handle the cases when j is (i+2), (i+1), i, -i, -(i+1), -(i+2) separately

[Eric Wieser]

Which will give you only 7 cases to handle

[Eric Wieser]

Based on your comment:

-- A lifting of simple refelection is a map int -> R × int
structure monomial_matrix  :=
mk  ::  (mat: int -> int × int)

you probably actually want

structure monomial_matrix (ι R : Type*) :=
(mat : ι → R × ι)  -- lean does `mk :: ` automatically
-- is `(mat j).2` the column number containing `(mat j).1` in row `j`,
-- or the row number containing ... in column `j`?

where I would guess def s [ring R] (i : nat) : monomial_matrix ℤ R

[Ma, Jia-Jun]

Eric Wieser said:

I think probably the way to do this is handle the cases when j is (i+2), (i+1), i, -i, -(i+1), -(i+2) separately

Mathematically yes, and the claim is easy to check by hand. However, is there a more automated way?

[Ma, Jia-Jun]

Eric Wieser said:

Based on your comment:

-- A lifting of simple refelection is a map int -> R × int
structure monomial_matrix  :=
mk  ::  (mat: int -> int × int)

you probably actually want

structure monomial_matrix (ι R : Type*) :=
(mat : ι → R × ι)  -- lean does `mk :: ` automatically
-- is `(mat j).2` the column number containing `(mat j).1` in row `j`,
-- or the row number containing ... in column `j`?

where I would guess def s [ring R] (i : nat) : monomial_matrix ℤ R

Thanks for the improvement. (mat j).2 is the row number containing (mat j).1 in column j (by viewing a vector as a column vector).

[Eric Wieser]

However, is there a more automated way?

I recommend first writing the five lemmas:

example : (s i).mat i = (- eps , i+1) := sorry
example : (s i).mat (i+1)= (eps , i) := sorry
example : (s i).mat -(i+1)= (eps , i) := sorry
example (h : i ≠ 0) : (s i).mat (-i) = (- eps , i+1) := sorry
example (h1 : j ≠ i) (h2 : j ≠ i+1) (h3 : j ≠ -(i+1)) (h4 : j ≠ -i) : (s i).mat j= (eps , i) := sorry

[Ma, Jia-Jun]

Eric Wieser said:

However, is there a more automated way?

I recommend first writing the five lemmas:

example : (s i).mat i = (- eps , i+1) := sorry
example : (s i).mat (i+1)= (eps , i) := sorry
example : (s i).mat -(i+1)= (eps , i) := sorry
example (h : i ≠ 0) : (s i).mat (-i) = (- eps , i+1) := sorry
example (h1 : j ≠ i) (h2 : j ≠ i+1) (h3 : j ≠ -(i+1)) (h4 : j ≠ -i) : (s i).mat j= (eps , i) := sorry

First two are simple:

example (i:nat): (s i).mat i = (- eps , i+1) := begin
  simp [s, ip_ne_i],
end

example (i:nat) : (s i).mat (i+1)= (eps , i) := begin
  simp [s],
  simp,
end

The third one is not easy already, I am run into the trouble to prove that

lemma neq_ii (i: nat ): -1 + -(i:int) ≠  (i:int) :=
begin
sorry
end

The whole thing is not difficult mathematically. My feeling is that the definition of s and monomial_matrix is not good.

[Eric Wieser]

tactic#linarith can solve that

[Eric Wieser]

If you want to know how to do it manually,

lemma neq_ii (i: nat ): -1 + -(i:int) ≠  (i:int) :=
begin
  intro h,
  rw [←neg_add, neg_eq_iff_add_eq_zero, add_assoc, add_comm] at h,
  cases h,
end

[Ma, Jia-Jun]

Eric Wieser said:

If you want to know how to do it manually,

lemma neq_ii (i: nat ): -1 + -(i:int) ≠  (i:int) :=
begin
  intro h,
  rw [←neg_add, neg_eq_iff_add_eq_zero, add_assoc, add_comm] at h,
  cases h,
end

Thanks.
linarith works perfectly.
But it seems I have to supply a big set of all such kinds of inequalities to simp. Is it possible to automate the process? For example, apply linarith on all the hypothesis?

[Damiano Testa]

Is any_goals { linarith } what you are looking for?

[Damiano Testa]

If you want to use a tactic on all side-goals generated by the application of one tactic, you can also use ;. For instance,

tactic1;
tactic2

means "use tactic2 on all goals that tactic1 produces".

[Ma, Jia-Jun]

Damiano Testa said:

Is any_goals { linarith } what you are looking for?

Is it possible to make Lean to reduce the expression of the both sides of the equation? just like #reduce can do ?

For example using #reduce I got

#reduce ((t 1) * (t 1)).mat (v.p 1)      -- (eps.neg.mul -[1+ 0], v.p 1)

But is I would like to proof the statement ((t 1) * (t 1)).mat (v.p 1) = (eps, v.p 1):

example  : ((t 1) * (t 1)).mat (v.p 1)  = (eps, v.p 1)
:= begin
  simp [t],

end

What I can get is the following big chunk of unsolved goal:

tactic failed, there are unsolved goals
state:
eps : ℤ
⊢ ({mat := λ (bb : v),
                 v.rec (λ (i : ℕ), ite (i = 1) (-1, v.n 1) (1, bb)) (λ (i : ℕ), ite (i = 1) (-eps, v.p 1) (1, bb))
                   bb} *
       {mat := λ (bb : v),
                 v.rec (λ (i : ℕ), ite (i = 1) (-1, v.n 1) (1, bb)) (λ (i : ℕ), ite (i = 1) (-eps, v.p 1) (1, bb))
                   bb}).mat
      (v.p 1) =
    (eps, v.p 1)

[Alex J. Best]

Can you post an updated MWE so people can try things out?

[Alex J. Best]

Does refl work to prove the equality with the output of reduce?

[Ma, Jia-Jun]

Alex J. Best said:

Can you post an updated MWE so people can try things out?

I rewrote the code so it is different from the original one.
The last example is where I got stuck. Thanks.

import tactic

universe u

-- Basis of the vector space V_l
-- The basis is v^±_0 , v^±_1 , ⋯, v^\pm_l
inductive v
| p  (i : nat) : v
| n  (i : nat) : v

#check v.p 1
def bb : v := v.p 1
#reduce bb

example : (v.p 1) = (v.p 1) := by refl
example (i : nat ) : (v.p i) ≠ (v.p (i+1)) :=
begin
  intro h,
  simp at h,
  exact h,
end

example (i : nat ) : (v.p i) ≠ (v.n (i+1)) :=
begin
  intro h,
  simp at h,
  exact h,
end

-- Monomail matrix by specify the value at the basis vector
structure monomial_matrix  :=  (mat: v -> int × v)

-- indentity matrix
def id_mat : monomial_matrix :=
  { mat := (λ j, (1,j))}


def mat_mul (w : monomial_matrix) (wp : monomial_matrix) :
  monomial_matrix :=  monomial_matrix.mk
    (λ j,
        let wp_j := (wp.mat j) in
        let w_wp_j:= (w.mat wp_j.2)
          in (w_wp_j.1 * wp_j.1, w_wp_j.2))

infixl ` * `:75 := mat_mul

section

parameter (eps : int)
-- def eps := 1

-- attribute [reducible]
-- def t_map (i : nat) (bb : v) : int × v :=
--  v.cases_on bb (λ j, if   j= i then (-1, v.n i) else (1, bb))
--   (λ j, if j = i then (-eps, v.p i) else (1, bb))

attribute [reducible]
def t (i : nat) : monomial_matrix := {
  mat :=
  (λ bb, v.cases_on bb
    (λ j, if   j= i then (-1, v.n i) else (1, bb))
    (λ j, if j = i then (-eps, v.p i) else (1, bb))
    )
    }


def eps_map (i : nat) (bb : v) : int × v :=
  v.cases_on bb
    (λ j, if j = i then (eps, bb) else (1, bb))
    (λ j, if j = i then (eps, bb) else (1, bb))


attribute [reducible]
def eps_mat (i : nat) : monomial_matrix := {
  mat :=   (λ bb, v.cases_on bb
    (λ j, if j = i then (eps, bb) else (1, bb))
    (λ j, if j = i then (eps, bb) else (1, bb))
    )
  }

#reduce  (t 1).mat (v.p 1)

example : (t 1).mat (v.p 1) = (-1, v.n 1) := begin
 simp [t],
end

example : (t 1).mat (v.n 1) = (- eps, v.p 1) := begin
 simp [t],
end

#reduce ((t 1) * (t 1)).mat (v.p 1)


-- example (l: nat) (hl: l=1 ): ((t l) * (t l)).mat (v.p l)  = (eps_mat l).mat (v.p l)
example  : ((t 1) * (t 1)).mat (v.p 1)  = (eps, v.p 1)
:= begin
  simp [t],
  refl,

end

end

[Ma, Jia-Jun]

Alex J. Best said:

Does refl work to prove the equality with the output of reduce?

no. :sweat_smile:

[Eric Wieser]

You should be adding lemmas in the style of the ones I suggested before

[Eric Wieser]

Don't start writing lemmas about multiplication until you've written the basic lemmas about t

[Eric Wieser]

@[simp] lemma t_mat_p_eq (i : ℕ) : (t i).mat (v.p i) = (-1, v.n i) := if_pos rfl
@[simp] lemma t_mat_n_eq (i : ℕ) : (t i).mat (v.n i) = (-eps, v.p i) := if_pos rfl
@[simp] lemma t_mat_p_ne {i j : ℕ} (h : j ≠ i) : (t i).mat (v.p j) = (1, v.p j) := if_neg h
@[simp] lemma t_mat_n_ne {i j : ℕ} (h : j ≠ i) : (t i).mat (v.n j) = (1, v.n j) := if_neg h