Construction of structures

Stream: maths

[Antoine Chambert-Loir]

The following code defines an equivalence :
fin_oplus_fin_equiv_fin {m n a : ℕ} (ham : a ≤ m): (fin m) ⊕ (fin n) ≃ fin (m + n)
that inserts the fin n after place a of the given fin m.
However, to prove the right_inv property, I was forced to define the to_fun and inv_fun parts
outside of the definition of the equiv, because otherwise, Lean wouldn't simp the inner argument.
I tried some other ways, but this is the only thing I could do…

Any advice ?

def aux_i {m n a : ℕ} (ham : a ≤ m) : (fin m) ⊕ (fin n) → fin (m + n) := λ xy,
begin
  induction xy with x y,
  { by_cases hx : (x : ℕ) < a,
    exact fin.cast_le (le_self_add) x,
    exact fin.add_nat n x, },
  { exact fin.cast_le (add_le_add_right ham n) (fin.nat_add a y), },
end

def aux_j {m n a : ℕ} (ham : a ≤ m): fin (m + n) → (fin m) ⊕ (fin n) := λ z,
begin
  by_cases hz : (z : ℕ) < a,
  exact sum.inl (fin.cast_le ham ⟨z, hz⟩),
  by_cases hz' : (z : ℕ) < a + n,
  exact sum.inr (⟨z - a,
  begin
    rw [lt_iff_not_le, nat.le_sub_iff_right (not_lt.mp hz), ← lt_iff_not_le],
    rw add_comm n a, exact hz',
  end⟩),
  exact sum.inl (⟨(z : ℕ) - n,
  begin
    rw [lt_iff_not_le, nat.le_sub_iff_right (le_trans (le_add_self) (not_lt.mp hz')), ← lt_iff_not_le],
    exact z.prop,
  end⟩),
end

def fin_oplus_fin_equiv_fin {m n a : ℕ} (ham : a ≤ m): (fin m) ⊕ (fin n) ≃ fin (m + n) := {
to_fun := aux_i ham,
inv_fun := aux_j ham,
left_inv := λ xy,
begin
  simp only [aux_j, aux_i],
  induction xy with x y,
  { simp only [not_lt, dite_eq_ite, fin.cast_le_mk],
    split_ifs with hx,
    { simp only [fin.insert_fin, hx],
      simp only [not_lt, if_true, fin.coe_cast_le, fin.eta, dite_eq_left_iff],
      intro h, exfalso, exact not_le.mpr hx h, },
    { simp only [hx, if_false, fin.coe_add_nat, add_lt_add_iff_right, not_false_iff,
      add_tsub_cancel_right, fin.eta, dif_neg, dite_eq_right_iff],
      intro h, exfalso, apply hx, apply lt_of_le_of_lt (le_self_add) h, }, },
  { simp only [fin.coe_nat_add, fin.cast_le_mk],
    split_ifs with hy hy',
    { apply not_le.mpr hy, exact le_self_add, },
    { simp only [fin.coe_cast_le, fin.coe_nat_add, add_tsub_cancel_left, fin.eta], },
    { simp only [fin.coe_cast_le, fin.coe_nat_add, add_lt_add_iff_left] at hy',
      exact hy' y.prop, }, },
end,
right_inv := λ z,
begin
  simp only [aux_j],
  by_cases hz : (z : ℕ) < a,
  { simp only [hz, fin.cast_le_mk, dif_pos],
    simp only [aux_i, hz, fin.coe_mk, fin.cast_le_mk, fin.eta, dite_eq_ite, if_true], },
  { by_cases hz' : (z : ℕ) < a + n,
    { rw ← subtype.coe_inj,
      simp only [hz, hz', aux_i, not_false_iff, fin.cast_le_mk, dif_pos, dif_neg, fin.nat_add_mk, fin.coe_mk],
      rw add_comm a _,
      refine nat.sub_add_cancel (not_lt.mp hz), },
    { rw ← subtype.coe_inj,
      simp only [hz, hz', aux_i, not_false_iff, fin.cast_le_mk, dif_neg, fin.coe_mk, fin.add_nat_mk, dite_eq_ite],
      suffices hz'' : ¬((z : ℕ) - n < a),
      simp only [hz'', if_false, fin.coe_mk],
      apply nat.sub_add_cancel,
      exact le_trans (le_add_self) (not_lt.mp hz'),
      intro hz'', apply hz', exact lt_add_of_tsub_lt_right hz'', }, },
end }

[Antoine Chambert-Loir]

(A related question would be how, in the definition of a structure, to access some already defined fields.)

[Bob Bass]

(deleted)

[Kyle Miller]

Found the mathlib definition, if you want to take a look how it was done: docs#fin_sum_fin_equiv

[Junyan Xu]

docs#fin_sum_fin_equiv doesn't have the flexibility of inserting at any place though. If you inline aux_i and aux_j, you just need a dsimp only to achieve (almost) the same effect as simp only [aux_i, aux_j]. I think you may also consider using docs#list.split_at, docs#list.append, docs#list.nth_le to construct the backward direction.

[Eric Wieser]

Inserting at any place can be achieved by composing docs#equiv.add_left on the input and output appropriately, right?

[Junyan Xu]

rather, docs#fin_rotate should work better (no need of abusing defeq between zmod and fin, and works for n=0)

[Kyle Miller]

Ah, I didn't read what the description of the needed equivalence well enough.

[Kyle Miller]

There are enough equivalences in mathlib to create this equivalence without needing to descend to terms:

import logic.equiv.fin
import tactic.zify
import tactic.ring

def fin_oplus_fin_equiv_fin {m n a : ℕ} (ham : a ≤ m) :
  fin m ⊕ fin n ≃ fin (m + n) :=
calc fin m ⊕ fin n ≃ fin (a + (m - a)) ⊕ fin n :
    equiv.sum_congr (fin.cast (by { zify [ham], ring})).to_equiv (equiv.refl _)
  ... ≃ (fin a ⊕ fin (m - a)) ⊕ fin n :
    equiv.sum_congr fin_sum_fin_equiv.symm (equiv.refl _)
  ... ≃ fin a ⊕ (fin (m - a) ⊕ fin n) : equiv.sum_assoc _ _ _
  ... ≃ fin a ⊕ (fin n ⊕ fin (m - a)) : equiv.sum_congr (equiv.refl _) (equiv.sum_comm _ _)
  ... ≃ fin a ⊕ fin (n + (m - a)) :
    equiv.sum_congr (equiv.refl _) fin_sum_fin_equiv
  ... ≃ fin (a + (n + (m - a))) : fin_sum_fin_equiv
  ... ≃ fin (m + n) : (fin.cast (by { zify [ham], ring })).to_equiv

[Ruben Van de Velde]

Neat. Do you also have a proof that it is the equivalence Antoine was looking for? :)

[Antoine Chambert-Loir]

I am impressed by Kyle's alternative definition (in fact, calc is a tactic I'm not enough used to),.

But this does not really answer my question which was that without an external definition of aux_i, everything was expanded too soon and the compiler wasn't able to rewrite something at the required depth.
Something I would like to be able to do is to rewrite right_inv as having to proveλ z, to_fun (inv_fun z) = z, and then expanding inv_fun, etc.

[Floris van Doorn]

You can do something like this:

import logic.equiv.fin

def fin_oplus_fin_equiv_fin {m n a : ℕ} (ham : a ≤ m): (fin m) ⊕ (fin n) ≃ fin (m + n) :=
let to_fun : (fin m) ⊕ (fin n) → fin (m + n) := λ xy,
begin
  sorry
end in
let inv_fun : fin (m + n) → (fin m) ⊕ (fin n) := λ z,
begin
  sorry
end in
{
to_fun := to_fun,
inv_fun := inv_fun,
left_inv := λ xy,
begin
  sorry -- inv_fun (to_fun xy) = xy
end,
right_inv := λ z,
begin
  -- to_fun (inv_fun z) = z
  simp only [inv_fun],
  -- to_fun (expanded version) = z
  sorry
end }

[Ruben Van de Velde]

I nerd-sniped myself and got lost in a maze of fin casting functions, but came out with a proof that Kyle's construction works: https://gist.github.com/Ruben-VandeVelde/9af0d23e0909719f7247e740bf3efbdf