Converting one type to another

Stream: new members

[Jakub Nowak]

I've just learned there exists a lift tactic. Is there a simpler way to convert from one type to another, equivalent one?

import Mathlib

instance : CanLift (Array α) (List α) List.toArray (fun _ ↦ True) where
  prf xs _ := ⟨xs.toList, by simp⟩

example (xs : Array Nat) : ∀ x ∈ xs.map (· + 1), x > 0 := by
  lift xs to List Nat
  · trivial
  simp

I'm aware, that I could prove the same with just simp, without converting from Array to List, but it's only for the sake of example. Is there a simpler way to replace Array with List?

[Jakub Nowak]

Here's another example, but it's even more cumbersome:

import Mathlib

example (xs : Array Nat) : ∀ x ∈ xs.map (· + 1), x > 0 := by
  let xs' := xs.toList
  have : xs = xs'.toArray := by simp [xs']
  rw [this]
  generalize xs' = xs
  clear * -

[Peter Hansen]

I am not entirely sure if the following is what you looking for, but if you are simply looking for a bit shorter notation, you can use using:

example (xs : Array Nat) : ∀ x ∈ xs.map (· + 1), x > 0 := by
  lift xs to List Nat using trivial
  simp

Or is it something entirely different you are hoping for?

[Jakub Nowak]

That's slightly simpler I guess. But I hoped there's maybe a tactic that can be used ad-hod without creating instance,

[Ruben Van de Velde]

Does this help?

import Mathlib

lemma aux (xs : Array Nat) : ∃ xs' : List Nat, xs'.toArray = xs := ⟨xs.toList, by simp⟩

example (xs : Array Nat) : ∀ x ∈ xs.map (· + 1), x > 0 := by
  obtain ⟨xs, rfl⟩ := aux xs
  sorry

[Peter Hansen]

Maybe:

example : ∀ (xs : Array Nat), ∀ x ∈ xs.map (· + 1), x > 0 := by
  rintro ⟨xs⟩
  simp

or

example (xs : Array Nat) :∀ x ∈ xs.map (· + 1), x > 0 := by
  obtain ⟨xs⟩ := xs
  simp

[Eric Wieser]

Perhaps more generally we should have Function.Surjective.induction as one direction of docs#Function.Surjective.forall, which would work with the cases ... using tactic