Dependent mapping of vector

Stream: new members

[Yakov Pechersky]

I'm trying to work on some vector API that should parallel list. I'm trying to come up with a dependent-map that can use a hypothesis about all of the elements of a vector. Below, I have an example. Does anyone have tips on how to do this or express this better? Avoid this entirely?

import data.vector2

variables {α : Type*} {n : ℕ} (v : vector α n)

open vector

namespace vector

def enum : vector (fin n × α) n :=
vector.of_fn (λ i, (i, v.nth i))

def enum' : vector (ℕ × α) n :=
⟨v.to_list.enum, by rw [list.length_enum, vector.to_list_length]⟩

lemma to_list_enum' : v.enum'.to_list = v.to_list.enum := rfl

@[simp] lemma nth_enum' (i : fin n) : v.enum'.nth i = (i, v.nth i) :=
begin
  rw [←option.some.inj_eq, nth_eq_nth_le, nth_eq_nth_le, ←list.nth_le_nth,
      to_list_enum', list.enum_nth, list.nth_le_nth],
  simp only [fin.val_eq_coe, option.map_some],
end

lemma enum_bdd_above' (i : fin n) : prod.fst (v.enum'.nth i) < n :=
by simpa only [nth_enum'] using i.property

-- I want to express `enum` as a dependent map of `enum'` using
-- `enum_bdd_above'` as the proof that I can construct a `fin n`.

def dmap' {α β : Type*} (m : ℕ) (p : β → Prop) (γ : ℕ → Type* → Type* → Type*)
          (g : Π {k : ℕ}, vector α k → vector β k) :
  Π {n : ℕ} (hl : n ≤ m) (v : vector α n)
  (h : Π {k : ℕ}, ∀ (v' : vector α k), k ≤ n → ∀ i, p ((g v').nth i))
  (f : Π (b : β), n ≤ m → p b → γ m α β),
  vector (γ m α β) n
| 0       hl v h f := nil
| 1       hl v h f := f ((g v).nth 0) hl (h _ (le_refl _) _) ::ᵥ nil
| (n + 2) hl v h f := f ((g v).nth 0) hl (h _ (le_refl _) 0) ::ᵥ dmap'
  (le_trans (nat.sub_le (n + 2) 1) hl)
  v.tail
  (λ k v' H, h v' (le_trans H (nat.sub_le (n + 2) 1)))
  (λ b _, f b hl)

-- is there a better way to do this?

#check @dmap' α (ℕ × α) n (λ i, i.fst < n) (λ k x px', fin k × x) (@enum' α)
        n (le_refl _) v
          (λ k v' h i, lt_of_lt_of_le (@enum_bdd_above' _ k v' i) h)
          (λ ⟨i, x⟩ h H, ⟨⟨i, H⟩, x⟩)

end vector

[Yakov Pechersky]

Ah, turns out there was a list.pmap I could port over. Thanks Julian and Mario for hints. Here's the proof I was trying to develop, at the bottom:

import data.vector2

variables {α β γ : Type*} {n : ℕ} (v : vector α n) (vn : vector α 0) (vs : vector α (n + 1)) (x : α)

open vector

namespace vector

section pmap

variables {v vn vs x}
variables {p q : α → Prop}

lemma prop_distribute :
  p x ∧ (∀ i, p (v.nth i)) ↔ ∀ i, p ((x ::ᵥ v).nth i) :=
begin
  split,
    { rintro ⟨hx, ht⟩ i,
      refine fin.cases _ _ i,
      { simpa only [nth_cons_zero] using hx },
      { simpa only [nth_cons_succ] using ht } },
    { intro h,
      split,
      { simpa only [nth_cons_zero] using h 0 },
      { intro i,
        simpa only [nth_cons_succ] using h i.succ } }
end

lemma prop_distribute' :
  (∀ i, p (vs.nth i)) ↔ p vs.head ∧ (∀ i', p (vs.tail.nth i')) :=
begin
  split,
  { intro h,
    split,
    { simpa only [nth_zero] using h 0 },
    { intro i,
      simpa only [nth_tail] using h i.succ } },
  { rintro ⟨hx, ht⟩ i,
    refine fin.cases _ _ i,
    { simpa only [nth_zero] using hx },
    { simpa only [nth_tail] using ht} },
end

lemma nth_of_mem (h : x ∈ v.to_list) : ∃ i, v.nth i = x :=
mem_iff_nth.mp h

lemma forall_mem_to_list_iff : (∀ x ∈ v.to_list, p x) ↔ ∀ (i : fin n), p (v.nth i) :=
⟨ λ h i, h _ (mem_iff_nth.mpr ⟨i, rfl⟩), λ h _ hx, exists.elim (nth_of_mem hx) (λ _ H, H ▸ h _)⟩

variables (v)

def pmap (f : Π (x : α), p x → β)
  (h : ∀ i : fin n, p (v.nth i)) : vector β n :=
⟨list.pmap f v.to_list (forall_mem_to_list_iff.mpr h), by rw [list.length_pmap, to_list_length]⟩

lemma pmap_def (f : Π (x : α), p x → β) (h : ∀ i : fin n, p (v.nth i)) :
  v.pmap f h = ⟨list.pmap f v.to_list (forall_mem_to_list_iff.mpr h),
                by rw [list.length_pmap, to_list_length]⟩ := rfl

lemma to_list_pmap (f : Π (x : α), p x → β)
  (h : ∀ i : fin n, p (v.nth i)) : (v.pmap f h).to_list = v.to_list.pmap f (forall_mem_to_list_iff.mpr h) := rfl

variable (p)

lemma pmap_eq_map (f : α → β) (h) : @pmap _ _ _ v p (λ x _, f x) h = v.map f :=
vector.eq _ _ (by simp only [to_list_map, to_list_pmap, list.pmap_eq_map])

variable {p}

lemma pmap_congr {f : Π (x : α), p x → β} {g : Π (x : α), q x → β} {H₁ H₂}
  (h : ∀ x h₁ h₂, f x h₁ = g x h₂) :
  v.pmap f H₁ = v.pmap g H₂ :=
vector.eq _ _ (v.to_list.pmap_congr h)

lemma map_pmap (g : β → γ) (f : Π (x : α), p x → β) (H) :
  (v.pmap f H).map g = v.pmap (λ a h, g (f a h)) H :=
vector.eq _ _ (list.map_pmap g f v.to_list (forall_mem_to_list_iff.mpr H))

@[simp] lemma pmap_nil {f : Π (x : α), p x → β} {h} :
  nil.pmap f h = nil := rfl

lemma pmap_nil' {f : Π (x : α), p x → β} {h} :
  vn.pmap f h = nil := by simp only [eq_iff_true_of_subsingleton]

@[simp] lemma pmap_singleton {f : Π (x : α), p x → β} {h} :
  (x ::ᵥ nil).pmap f h = f x (h 0) ::ᵥ nil := rfl

@[simp] lemma pmap_cons {f : Π (x : α), p x → β} {h} (hx : p x) :
  (x ::ᵥ v).pmap f h = f x hx ::ᵥ v.pmap f (prop_distribute.mpr h).right :=
by simpa only [pmap_def, to_list_cons]

@[simp] lemma pmap_head {f : Π (x : α), p x → β} : Π {vs : vector α (n + 1)} {h},
  (vs.pmap f h).head = f vs.head (prop_distribute'.mp h).left
| ⟨[],     hl⟩ _ := by contradiction
| ⟨x :: l, hl⟩ _ := rfl

@[simp] lemma nth_pmap_cons {f : Π (x : α), p x → β} {H i} :
  (v.pmap f H).nth i = f (v.nth i) (H i) :=
begin
  induction n with n hn generalizing f H i,
  { exact fin_zero_elim i },
  { have : ∃ h t, h ::ᵥ t = v := ⟨v.head, v.tail, cons_head_tail v⟩,
    rcases this with ⟨x, t, hv⟩,
    simp_rw ←hv at H ⊢,
    have hx : p x := (prop_distribute.mpr H).left,
    refine fin.cases _ _ i,
    { simp only [nth_zero, pmap_head] },
    { rw pmap_cons _ hx,
      simp_rw nth_cons_succ,
      apply hn } }
end

end pmap

section enum

def enum : vector (fin n × α) n :=
of_fn (λ i, (i, v.nth i))

lemma enum_def : v.enum = of_fn (λ i, (i, v.nth i)) := rfl

lemma to_list_enum : v.enum.to_list = list.of_fn (λ i, (i, v.nth i)) :=
by simp only [enum_def, to_list_of_fn]

@[simp] lemma nth_enum (i : fin n) : v.enum.nth i = (i, v.nth i) :=
by simp only [enum_def, nth_of_fn]

def enum' : vector (ℕ × α) n :=
⟨v.to_list.enum, by rw [list.length_enum, vector.to_list_length]⟩

lemma to_list_enum' : v.enum'.to_list = v.to_list.enum := rfl

@[simp] lemma nth_enum' (i : fin n) : v.enum'.nth i = (i, v.nth i) :=
begin
  rw [←option.some.inj_eq, nth_eq_nth_le, nth_eq_nth_le, ←list.nth_le_nth,
      to_list_enum', list.enum_nth, list.nth_le_nth],
  simp only [fin.val_eq_coe, option.map_some],
end

lemma enum_bdd_above' (i : fin n) : prod.fst (v.enum'.nth i) < n :=
by simpa only [nth_enum'] using i.property

def enum_p : vector (fin n × α) n :=
pmap v.enum' (λ xpair h, ((⟨xpair.fst, h⟩), xpair.snd)) v.enum_bdd_above'

lemma enum_p_def :
  v.enum_p = v.enum'.pmap (λ xpair h, ((⟨xpair.fst, h⟩), xpair.snd)) v.enum_bdd_above' := rfl

lemma enum_eq_enum_p : v.enum = v.enum_p :=
begin
  apply ext,
  intro i,
  simp only [enum_p_def, nth_enum, nth_pmap_cons, nth_enum', fin.eta],
end

end enum

end vector

[Shreyas Srinivas]

Hello folks. I am very new to lean and dependently typed programming. Unfortunately I have hit what seems to be a beginner's snag. I have worked through the lean theorem proving tutorial and attempted the most basic example that dependently typed languages advertise, namely Vec a n. A snippet below:

inductive Vec (α : Type) : Nat → Type where
  | Nil : Vec α 0
  | Cons : {x : Nat} → α → Vec α x → Vec α (1+x)


open Vec

def commute {α : Type} {m n : Nat} : Vec α (m + n) = Vec α (n + m) := congrArg (Vec α) (Nat.add_comm m n)

def concat {α : Type} {n m : Nat} (v : Vec α n) (w : Vec α m) : Vec α (n+m) :=
  match v with
    | Vec.Nil => concat Nil w
    | Vec.Cons x xs => Cons x (concat xs w)

Unfortunately the Cons arm of the match protests that

type mismatch
  Cons x (concat xs w)
has type
  Vec α (1 + (x✝ + m)) : Type
but is expected to have type
  Vec α (1 + x✝ + m) : Type

I have read the chapter on Quantifiers and Equality. However, the functions/theorems there only allow one to derive new Propositions or Types. How do I derive a vector of type Vec α (1 + x✝ + m) from Vec α (1 + x✝ + m)

More concisely, is there is a function that does the following: def transform_equiv (α β : Type) (f : Type → Type) (hab : α = β) (a : f α) : f β := _ # Same value for type \beta

[Kyle Miller]

Associativity of addition in the index of a type is a perennial dependent type problem.

To answer your last question first, that function is easy to define with tactics:

def cast_idx {α β : Type} (f : Type → Type) (hab : α = β) (a : f α) : f β :=
by { cases hab, exact a }

/-- Likely useful when trying to work with `cast_idx`. -/
lemma cast_idx_rfl {α β : Type} (f : Type → Type) (a : f α) : cast_idx f rfl a = a := rfl

[Kyle Miller]

It's also easy to define without tactics:

def cast_idx {α β : Type} (f : Type → Type) (hab : α = β) (a : f α) : f β := eq.rec a hab

[Kyle Miller]

Oh, you're using Lean 4, that was Lean 3.

[Kyle Miller]

Lean 4:

def cast_idx {α β : Type} (f : Type → Type) (hab : α = β) (a : f α) : f β :=
by { cases hab; exact a }

-- Or, using the recursor:
def cast_idx {α β : Type} (f : Type → Type) (hab : α = β) (a : f α) : f β :=
Eq.rec (motive := λ γ _ => f γ) a hab

-- Or, using the recursor's notation:
def cast_idx {α β : Type} (f : Type → Type) (hab : α = β) (a : f α) : f β :=
hab ▸ a

/-- Likely useful when trying to work with `cast_idx`. -/
theorem cast_idx_rfl {α β : Type} (f : Type → Type) (a : f α) : cast_idx f rfl a = a := rfl

[Kyle Miller]

Anyway, this is a potential way to write concat:

def concat {α : Type} {n m : Nat} (v : Vec α n) (w : Vec α m) : Vec α (n+m) :=
  match v with
    | Vec.Nil => Nat.zero_add _ ▸ w
    | Vec.Cons x xs => Nat.add_assoc _ _ _ ▸ Cons x (concat xs w)

[Mario Carneiro]

A warning: You used 1+x in the definition of Vec, which is common in Coq because addition is defined by recursion on the left. In Lean, addition is defined by recursion on the right, so you should prefer x+1, it will unfold definitionally in more contexts that way (which is important for dependent type families)

[Mario Carneiro]

In fact, with just a bit of commutation, you can make the definition of concat go through without any casts:

inductive Vec (α : Type) : Nat → Type where
  | Nil : Vec α 0
  | Cons : {x : Nat} → α → Vec α x → Vec α (x+1)


open Vec

def concat {α : Type} {n m : Nat} (v : Vec α n) (w : Vec α m) : Vec α (m + n) :=
  match v with
  | Vec.Nil => w
  | Vec.Cons x xs => Cons x (concat xs w)

[Shreyas Srinivas]

Kyle Miller said:

Associativity of addition in the index of a type is a perennial dependent type problem.

To answer your last question first, that function is easy to define with tactics:

def cast_idx {α β : Type} (f : Type → Type) (hab : α = β) (a : f α) : f β :=
by { cases hab, exact a }

/-- Likely useful when trying to work with `cast_idx`. -/
lemma cast_idx_rfl {α β : Type} (f : Type → Type) (a : f α) : cast_idx f rfl a = a := rfl

Thanks a lot. This helps immensely.