equality of functions with bounded finite decideable domains

Stream: general

[Gavid Liebnich]

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]

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]

@Gavid Liebnich it's false

[Mario Carneiro]

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

[Mario Carneiro]

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

[Gavid Liebnich]

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]

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]

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]

it's m.data x not x.1

[Kenny Lau]

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

[Kenny Lau]

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]

@Gavid Liebnich

[Gavid Liebnich]

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.