dependent structures

Stream: new members

[Jake Levinson]

What's the right way to work with dependent / parametrized structures like structure foo (a : α) : ... where α : Type? I have something like that, and sometimes I end up with two foo's using different but equal a's, and I'd like to compare them or work with them.

Here's the sort of thing I mean:

import tactic

variable {α : Type}

def p : α → Prop := sorry
def f : α → α := sorry
lemma fp {a : α} : p a → p (f a) := sorry

structure foo (a : α) :=
  (seq : ℕ → ℕ)
  (bar : p a)

def new_foo {a : α} (t : foo a) : foo (f a) :=
{ seq := λ n, t.seq (n + 1),
  bar := fp t.bar }

def new_foo' {a : α} (t : foo a) (h : f a = a) : foo a :=
  (congr_arg foo h).mp (new_foo t)

lemma new_foo'_def {a : α} (t : foo a) (h : f a = a) (n : ℕ):
  (new_foo' t h).seq n = t.seq (n+1) := sorry

So by default new_foo produces something of type foo (f a), but occasionally I can get a foo a instead. In the situation I'm in, the new_foo definition is actually quite involved -- that's why I wanted new_foo' to "piggyback" off of it rather than redoing the proof. The situation is loosely along the lines of a : set X and an operation like new_foo ... : foo (insert x a), where sometimes it can be shown that x ∈ a and so this operation should stay in foo a.

But, the congr_arg definition seems... awkward, in particular I don't know how to prove the last sorry as (new_foo' t h).seq is not defeq to (new_foo a).seq. If I do rw [new_foo', new_foo] I get stuck with a goal like

⊢ (_.mp {seq := λ (n : ℕ), t.seq (n + 1), bar := _}).seq n = t.seq (n + 1)

So the eq.mp is in the way of the pattern matching. I suspect I shouldn't be trying to modify the a parameter. Should I be defining

structure foo' :
  (a : α)
  (seq : ℕ → ℕ)
  (bar : p a)

instead?

[Kyle Miller]

One way around this is to use a copy pattern (that's a link to one instance of it). You create a copy function that rewrites the relevant parts to make things definitionally convenient.

For your case, we can re-use seq when we copy it, and then that last sorry can be a mere rfl:

variable {α : Type}

def p : α → Prop := sorry
def f : α → α := sorry
lemma fp {a : α} : p a → p (f a) := sorry

structure foo (a : α) :=
  (seq : ℕ → ℕ)
  (bar : p a)

def new_foo {a : α} (t : foo a) : foo (f a) :=
{ seq := λ n, t.seq (n + 1),
  bar := fp t.bar }

def foo.copy {a a' : α} (t : foo a) (h : a = a') : foo a' :=
{ seq := t.seq,
  bar := h ▸ t.bar }

def new_foo' {a : α} (t : foo a) (h : f a = a) : foo a :=
(new_foo t).copy h

lemma new_foo'_def {a : α} (t : foo a) (h : f a = a) (n : ℕ):
  (new_foo' t h).seq n = t.seq (n+1) := rfl

[Jake Levinson]

Neato, I'll try that in my larger context.

[Jake Levinson]

yesssss

[Jake Levinson]

That works. Thanks!