# Zulip Chat Archive

## Stream: general

### Topic: equality of functions with bounded finite decideable domains

#### Gavid Liebnich (Nov 20 2018 at 11:25):

Is `eq_of_yield`

provable? Do I need to lose computability with functional extensionality?

import data.vector data.list utils variables {α : Type} def between [decidable_linear_order α] (a b : α) := {x : α // a ≤ x ∧ x < b} class c_mapper (α : Type*) := (n : α → ℕ) (h : Πm, 0 < n m) (data : Πm, between 0 (n m) → ℕ) variables [c_mapper α] def yield (m : α) := (list.range $ c_mapper.n m).attach.map $ λn, c_mapper.data m ⟨n, nat.zero_le _, list.mem_range.1 n.2⟩ theorem eq_of_yield {m₁ m₂ : α} (h : yield m₁ = yield m₂) : m₁ = m₂ := sorry

#### Kenny Lau (Nov 20 2018 at 11:35):

import data.vector data.list data.set.intervals class c_mapper (α : Type*) := (n : α → ℕ) (h : ∀ m, 0 < n m) (data : Π m, set.Ico 0 (n m) → ℕ) def yield {α : Type*} [c_mapper α] (m : α) := (list.range $ c_mapper.n m).attach.map $ λ n, c_mapper.data m ⟨n, nat.zero_le n, list.mem_range.1 n.2⟩ theorem not_yield_inj : ¬ ∀ (α : Type) [c_mapper α] {m₁ m₂ : α} (h : by resetI; exact yield m₁ = yield m₂), m₁ = m₂ := λ H, absurd (@H bool ⟨λ _, 1, λ _, dec_trivial, λ _ _, 0⟩ ff tt rfl) dec_trivial

#### Kenny Lau (Nov 20 2018 at 11:35):

@Gavid Liebnich it's false

#### Mario Carneiro (Nov 20 2018 at 11:44):

also function extensionality doesn't affect computability because it's a prop

#### Mario Carneiro (Nov 20 2018 at 11:45):

unlike some other constructive systems we have a proof irrelevant universe of propositions which are not used in computation

#### Gavid Liebnich (Nov 20 2018 at 12:23):

Oh, thanks! I think It's starting to make sense now - of course it's not an injection, the `Πm, between 0 (n m) → ℕ`

can be whatever mapping I want.

So, if I were to define one such concrete mapping, for example:

structure mapper := (n : ℕ) (h : 0 < n) (data : vector ℕ n) instance indexed_mapper_is_c_mapper : c_mapper mapper := { n := λm, m.n, h := λm, m.h, data := λm x, m.data.nth ⟨x.1, x.2.2⟩ }

I could then prove (somehow)

theorem eq_of_yield {m₁ m₂ : mapper} (h : yield m₁ = yield m₂) : m₁ = m₂

because the `data`

of `c_mapper`

would be the function `vector.data.nth`

?

#### Gavid Liebnich (Nov 20 2018 at 12:37):

So the theorem is true if I give it two extensionally equivalent functions as `data`

? For example, if I were to define a mapper that completely mirrors the `class`

, that would make the theorem true by virtue of the functions used as `data`

in `m1`

and `m2`

being equivalent? As such:

structure mapper₂ := (n : ℕ) (h : 0 < n) (data : between 0 n → ℕ) instance : c_mapper mapper₂ := { n := λm, m.n, h := λm, m.h, data := λm x, x.1 } theorem eq_of_yield {m₁ m₂ : mapper₂} (h : yield m₁ = yield m₂) : m₁ = m₂ := sorry

Now the theorem is true?

#### Kenny Lau (Nov 20 2018 at 12:58):

just because it typechecks doesn't mean it's correct... I've corrected your code:

instance c_mapper_mapper₂ : c_mapper mapper₂ := { n := λ m, m.n, h := λ m, m.h, data := λ m x, m.data x }

#### Kenny Lau (Nov 20 2018 at 12:59):

it's `m.data x`

not `x.1`

#### Kenny Lau (Nov 20 2018 at 12:59):

I think we would appreciate it if you check your questions before asking them

#### Kenny Lau (Nov 20 2018 at 12:59):

I've proved both theorems:

import data.vector data.list data.set.intervals open set class c_mapper (α : Type*) := (n : α → ℕ) (h : ∀ m, 0 < n m) (data : Π m, Ico 0 (n m) → ℕ) structure mapper := (n : ℕ) (h : 0 < n) (data : vector ℕ n) instance c_mapper_mapper : c_mapper mapper := { n := λ m, m.n, h := λ m, m.h, data := λ m x, m.data.nth ⟨x.1, x.2.2⟩ } variables {α : Type*} [c_mapper α] def yield (m : α) : list ℕ := (list.range $ c_mapper.n m).attach.map $ λ n, c_mapper.data m ⟨n, nat.zero_le n, list.mem_range.1 n.2⟩ theorem yield_inj {m₁ m₂ : mapper} (h : yield m₁ = yield m₂) : m₁ = m₂ := begin have hy1 : (yield m₁).length = m₁.n, { rw [yield, list.length_map, list.length_attach, list.length_range]; refl }, have hy2 : (yield m₂).length = m₂.n, { rw [yield, list.length_map, list.length_attach, list.length_range]; refl }, cases m₁ with n1 h1 d1, cases m₂ with n2 h2 d2, have hn : n1 = n2, { convert congr_arg list.length h, exacts [hy1.symm, hy2.symm] }, subst n2, congr' 1, cases d1 with L1 H1, cases d2 with L2 H2, congr' 1, dsimp only at hy1 hy2, refine list.ext_le (H1.trans H2.symm) (λ i hi1 hi2, _), have : ∀ h3, list.nth_le (yield ({n := n1, h := h1, data := ⟨L1, H1⟩} : mapper)) i h3 = list.nth_le (yield ({n := n1, h := h2, data := ⟨L2, H2⟩} : mapper)) i (hy2.symm ▸ H2 ▸ hi2), { rw h, intro, refl }, specialize this (hy1.symm ▸ H1 ▸ hi1), simp only [yield, list.nth_le_map', c_mapper.data, vector.nth] at this, unfold coe lift_t has_lift_t.lift coe_t has_coe_t.coe coe_b has_coe.coe at this, simpa only [list.nth_le_attach, list.nth_le_range] end structure mapper₂ := (n : ℕ) (h : 0 < n) (data : Ico 0 n → ℕ) instance c_mapper_mapper₂ : c_mapper mapper₂ := { n := λ m, m.n, h := λ m, m.h, data := λ m x, m.data x } theorem yield_inj' {m₁ m₂ : mapper₂} (h : yield m₁ = yield m₂) : m₁ = m₂ := begin have hy1 : (yield m₁).length = m₁.n, { rw [yield, list.length_map, list.length_attach, list.length_range]; refl }, have hy2 : (yield m₂).length = m₂.n, { rw [yield, list.length_map, list.length_attach, list.length_range]; refl }, cases m₁ with n1 h1 d1, cases m₂ with n2 h2 d2, have hn : n1 = n2, { convert congr_arg list.length h, exacts [hy1.symm, hy2.symm] }, subst n2, congr' 1, ext i, rcases i with ⟨i, hi1, hi2⟩, dsimp only at hy1 hy2, have : ∀ h3, list.nth_le (yield ({n := n1, h := h1, data := d1} : mapper₂)) i h3 = list.nth_le (yield ({n := n1, h := h2, data := d2} : mapper₂)) i (hy2.symm ▸ hi2), { rw h, intro, refl }, specialize this (hy1.symm ▸ hi2), simp only [yield, list.nth_le_map', c_mapper.data, vector.nth] at this, unfold coe lift_t has_lift_t.lift coe_t has_coe_t.coe coe_b has_coe.coe at this, simpa only [list.nth_le_attach, list.nth_le_range] end

#### Kenny Lau (Nov 20 2018 at 13:00):

@Gavid Liebnich

#### Gavid Liebnich (Nov 20 2018 at 13:08):

Thank you, @Kenny Lau . I appreciate your help. The transition from nondependent `range`

to the bounded mapping is a step I'm having difficulties with. There's a bit of magic in `convert`

it would appear, I'll have to take a closer look. Thanks again, I'm going to step over the proofs.

Last updated: May 08 2021 at 19:11 UTC