How to not forget definition when unpacking pair?

Stream: new members

[Jakub Nowak]

I have this weird problem. I have a function that returns Sigma, and I have a theorem that proves something about return value. The problem is, I don't know how I should use that function and the theorem.
Here's a short mwe, that demonstrates my problem, I used pair instead of Sigma, but its the same problem:

import Mathlib

def foo (n : ℕ) : ℕ × ℕ :=
  ⟨n, 2*n⟩

theorem foo_snd_even (n : ℕ) : Even (foo n).snd := by
  unfold foo
  simp_all

example := by
  let ⟨a, b⟩ := foo 3
  have : Even b := by
    unfold b
  -- Now, I can't prove `Even b`, because b "forgot" its value.

[Kyle Miller]

Options:

1. If applicable, don't return a sigma, have multiple declarations. (Maybe this is related your walk+property question?)
2. Use let v := foo 3 and work with v.1 and v.2 instead of destructuring.
3. Similar, but use let a := v.1 and let b := v.2.
4. Use let (eq := h) ⟨a, b⟩ := foo 3.

[Jakub Nowak]

Kyle Miller said:

Options:

1. If applicable, don't return a sigma, have multiple declarations. (Maybe this is related your walk+property question?)

Yes, it's the function from that other question. I don't know how to avoid Sigma there. I've made mwe with sigma, as this should better represent my problem:

import Mathlib

def foo (n : ℕ) : Σ n, Vector ℕ (n + 1) := ⟨n+42, .replicate (n + 43) n⟩

theorem foo_snd_head (n : ℕ) : (foo n).snd.head = n := by
  unfold foo
  unfold Vector.head
  simp_all

example := by
  let ⟨n, vec⟩ := foo 3
  -- I want to have this context:
  -- n : ℕ
  -- vec : Vector ℕ (n + 1)
  -- h : vec.head = 3
  have : vec.head = n := by
    unfold vec

[Jakub Nowak]

For context, the functions mentioned are:

def odd_cycle_of_odd_walk [DecidableEq V] (p : G.Walk u u) : Σ v : V, G.Walk v v

theorem odd_cycle_of_odd_walk.isCycle [DecidableEq V]
    (p : G.Walk u u) (hOdd : p.length.bodd) :
    (odd_cycle_of_odd_walk p).snd.IsCycle

Should I declare them differently to avoid Sigma?

[Kyle Miller]

No, I'd stick with that sigma type. I just didn't know if you were using "sigma" loosely in a way that also encompassed subtypes.

[Jakub Nowak]

I've tried like this, but set created a new variable named vec, while this still refers to the old variable:

import Mathlib

def foo (n : ℕ) : Σ n, Vector ℕ (n + 1) := ⟨n+42, .replicate (n + 43) n⟩

theorem foo_snd_head (n : ℕ) : (foo n).snd.head = n := by
  unfold foo
  unfold Vector.head
  simp_all

example := by
  let vec := (foo 3).snd
  have : vec.head = 3 := by
    unfold vec
    exact foo_snd_head 3
  clear_value vec
  set n := (foo 3).fst
  -- I want to have this context:
  -- n : ℕ
  -- vec : Vector ℕ (n + 1)
  -- h : vec.head = 3

[Jakub Nowak]

Kyle Miller said:

2. Use let v := foo 3 and work with v.1 and v.2 instead of destructuring.
3. Similar, but use let a := v.1 and let b := v.2.

I kinda don't like this solution, because it forces me to somehow name the pair.
Though, I guess I could do

let := foo 3
let a := this.1
let b := this.2

[Jakub Nowak]

Well, I finally got it, after like 4 different ideas failing. .-.

import Mathlib

def foo (n : ℕ) : Σ n, Vector ℕ (n + 1) := ⟨n+42, .replicate (n + 43) n⟩

theorem foo_snd_head (n : ℕ) : (foo n).snd.head = n := by
  unfold foo
  unfold Vector.head
  simp_all

example := by
  let (eq := eq) ⟨n, vec⟩ := foo 3
  have h : (foo 3).snd.head = 3 := foo_snd_head 3
  rw [eq] at h
  simp only at h
  clear eq

But that's way too convoluted for something that should be much simpler. ;_;
Isn't there something simpler?

[Kyle Miller]

Is destructuring foo 3 worth it? Do you save much by not writing foo 3?

Or, what's wrong with let loop := odd_cycle_of_odd_walk p and then working with loop?

If (eq := ...) works for you, that's pretty much the best you can do with let destructuring. I've been thinking about adding a feature to preserve the definitional equalities, but it's relatively low priority. It'd be neat though. People ask your question at least once a month. At least we have this eq syntax, which is just two months old.