cons is to snoc as Fin.eq_zero_or_eq_succ is to

Stream: Is there code for X?

[Bolton Bailey]

Do we have

theorem Fin.eq_castSucc_or_eq_last {n : Nat} : ∀ i : Fin (n + 1),
    (∃ j : Fin n, i = j.castSucc) ∨ i = n

anywhere?

[Bolton Bailey]

theorem Fin.eq_castSucc_or_eq_last {n : Nat} : ∀ i : Fin (n + 1),
    (∃ j : Fin n, i = j.castSucc) ∨ i = n := by
  intro ⟨i, hi⟩
  by_cases h : i < n
  · left
    use ⟨i, by assumption⟩
    simp only [castSucc_mk]
  · right
    apply Fin.eq_of_val_eq
    simp only [coe_ofNat_eq_mod]
    rw [Nat.mod_eq_of_lt (Nat.lt.base n), Nat.eq_of_lt_succ_of_not_lt hi h]

[Eric Wieser]

docs#Fin.snocInduction maybe?

[Eric Wieser]

docs#Fin.consCases is the lemma that I think we should actually have a snoc version of

[Bolton Bailey]

I'm starting to think we should have a to_snoc modifier like to_additive for some of these, seems like a bunch of totally analogous lemmas.

cons <-> snoc
tail <-> init
succ <-> castSucc
zero <-> last
pred <-> ???

[Bolton Bailey]

Or more simply a reverse function, some lemmas about it, and then use that to prove things about snoc type functions

[Bolton Bailey]

(In fact, docs#Fin.rev exists)

[Bolton Bailey]

Is there any hope of this? I can define

def reverse {α : Fin n → Type u} (q : ∀ i, α i) : ∀ i : Fin n, α (rev i) :=
  fun i => q (rev i)

and

theorem init_eq_reverse_tail_reverse (q : ∀ i, α i) (k) : init q k = reverse (tail (reverse q)) k := by sorry

but then I get

type mismatch
  reverse (tail (reverse q)) k
has type
  α (rev (succ (rev k))) : Type u
but is expected to have type
  α (castSucc k) : Type u

Is there some way of getting lean to know these types are the same?

[Bolton Bailey]

Is this a use case for heterogenous equality?

[Eric Wieser]

I would recommend composing with Fin.cast on one side

[Bolton Bailey]

Sweet, that's exactly what I'm looking for, thanks.

[Bolton Bailey]

Hmm, maybe I spoke too soon. It seems docs#Fin.cast casts Fin n to Fin m when n = m. But what I need is to cast alpha i to alpha j where i = j are equal elements, both of Fin (n + 1)

[Bolton Bailey]

I think I want docs#cast

[Timo Carlin-Burns]

I'm not sure if there's a reason to prefer Eq.cast or ▸ (\t), but here's a starting place using the latter

open Fin

def reverse {n : ℕ} {α : Fin n → Type u} (q : ∀ i, α i) : ∀ i : Fin n, α (rev i) :=
  fun i => q (rev i)

theorem castSucc_eq_rev_succ_rev {n : ℕ} (k : Fin n) : castSucc k = rev (succ (rev k)) := by
  sorry

theorem init_eq_reverse_tail_reverse {n : ℕ} {α : Fin (n + 1) → Type u} (q : ∀ i, α i) (k : Fin n) : init q k = castSucc_eq_rev_succ_rev k ▸ reverse (tail (reverse q)) k := by
  sorry

[Timo Carlin-Burns]

You could also change your goal to HEq (init q k) (reverse (tail (reverse q)) k)

[Bolton Bailey]

It works!

theorem init_eq_reverse_tail_reverse (q : ∀ i, α i) (i) :
    init q i = _root_.cast (by rw [castSucc_eq_rev_succ_rev]) (reverse (tail (reverse (q))) i) := by
  rw [init, reverse, tail, eq_comm, cast_eq_iff_heq, castSucc_eq_rev_succ_rev]
  exact congr_arg_heq q (Eq.refl (rev (succ (rev i))))

[Bolton Bailey]

snoc_eq_reverse_cons_reverse being tricky though

[Timo Carlin-Burns]

@Bolton Bailey I'm a beginner and I'm curious, does your proof of castSucc_eq_rev_succ_rev look much different from mine?

import Mathlib

namespace Fin

@[simp]
theorem succ_rev {n : ℕ} (k : Fin n) : succ (rev k) = rev (castSucc k) := by
  ext
  simp only [val_succ, val_rev, coe_castSucc, Nat.succ_sub_succ_eq_sub]
  zify [show k + 1 ≤ n from k.is_lt, show k ≤ n from is_le']
  ring

theorem rev_succ_rev {n : ℕ} (k : Fin n) : rev (succ (rev k)) = castSucc k := by
  simp

end Fin

[Bolton Bailey]

I have been using this software for years now and I still do not know how to prove lemmas about tsub, I had just sorried it

[Bolton Bailey]

There should be a zify! tactic which just assumes every tsub it sees is nondegenerate and then throws off the proofs it needs to throw off.

[Bolton Bailey]

Can I steal this? (also I think the one with succ should be the one it simplifies to).

[Timo Carlin-Burns]

Sure!

[Timo Carlin-Burns]

I was thinking that the simp normal form should push revs to the outside like how there's a simp lemma for -(a + b) = -b - a

[Bolton Bailey]

Maybe. My sort of goal with all of this is to make all the things on the right hand side of the comment above simplify to their right hand counterparts so we can easily reduce to one bigger API.

[Timo Carlin-Burns]

I think I mixed myself up. You're right. We push negs to the inside, so we should do the same with revs.

[Timo Carlin-Burns]

Playing around with this, after I proved that _ ▸ (reverse (reverse q)) = q, I realized I would really want to be able to float these casts in and out of expressions, so I tried to prove _ ▸ (reverse q) = reverse (_ ▸ q) Unfortunately, I think it's impossible. It's similar to the following statement:

import Mathlib.Logic.Basic

universe u
theorem cast_behaves {ι : Type u} {α β : ι → Type u}
    (h : ∀ i, α i = β i) (f : ∀ i, α i) (i : ι) :
  cast (h i) (f i) = cast (pi_congr (congrFun (funext h))) f i :=
  sorry -- unprovable, right? we can't prove anything about the result of applying casted functions.

[Timo Carlin-Burns]

I PRed some of the above lemmas: std4#277

[Eric Wieser]

I think you can prove that with revert h, rw [<-funext_iff], rintro rfl or similar

[Eric Wieser]

If rw doesn't work then applying docs#forall_prop_congr or similar might

[Alex J. Best]

Bolton Bailey said:

There should be a zify! tactic which just assumes every tsub it sees is nondegenerate and then throws off the proofs it needs to throw off.

Can you open an issue for this? It sounds like a nice idea and it would be great if it wasn't forgotten. There are definitely people out there (myself included) that look at the tactics issues when bored and want a small project to implement.

[Bolton Bailey]

Alex J. Best said:

Bolton Bailey said:

There should be a zify! tactic which just assumes every tsub it sees is nondegenerate and then throws off the proofs it needs to throw off.

Can you open an issue for this? It sounds like a nice idea and it would be great if it wasn't forgotten. There are definitely people out there (myself included) that look at the tactics issues when bored and want a small project to implement.

Done! #7450

[Timo Carlin-Burns]

Eric Wieser said:

I think you can prove that with revert h, rw [<-funext_iff], rintro rfl or similar

That approach doesn't work

import Mathlib

universe u

theorem cast_behaves {ι : Type u} {α β : ι → Type u}
    (h : ∀ i, α i = β i) (f : ∀ i, α i) (i : ι) :
  cast (h i) (f i) = cast (pi_congr (congrFun (funext h))) f i := by
  revert h
  rw [← Function.funext_iff]
  -- ⊢ (fun h ↦ cast _ (f i)) = fun h ↦ cast _ f i
  rintro rfl -- error: our goal is not an implication

[Eric Wieser]

import Mathlib

universe u

theorem cast_behaves {ι : Type u} {α β : ι → Type u}
    (h : ∀ i, α i = β i) (f : ∀ i, α i) (i : ι) :
  cast (h i) (f i) = cast (pi_congr (congrFun (funext h))) f i := by
  revert h
  refine (forall_prop_congr (fun x => Iff.rfl) (Function.funext_iff).symm).mpr ?_
  rintro (rfl : α = β)
  rfl