Instances of functions

Stream: new members

[Andrew Carter]

I'm trying to get some instance code working but I'm running into "maximum class-instance resolution depth has been reached ...", and I'm a little bit worried that I'm using instances beyond their intended capacity. The only instances I have defined are:

instance iteration_complexity (α: Type) [α_en: has_encoding α]
  (f: α → α) [cf: has_complexity f]: has_complexity (nat.iterate f) :=
begin
  fconstructor,
  fconstructor,
  swap,
  apply iteration_complexity_le,
  apply cf.value.2,
  refl,
  { intros a b, refl },
end

instance flip_complexity (α β γ: Type) [α_en: has_encoding α] [β_en: has_encoding β] [γ_en: has_encoding γ]
  (f: α → β → γ) [cf: has_complexity f]: has_complexity (function.swap f) :=
begin
  fconstructor,
  fconstructor,
  swap,
  apply flip_complexity_le,
  apply cf.value.2,
  refl,
  { intros a b, refl },
end

instance pred_complexity: has_complexity nat.pred :=
begin
  fconstructor,
  fconstructor,
  swap,
  apply pred_complexity_le,
end

instance sub_complexity: has_complexity nat.sub :=
begin
  rw [show nat.sub = function.swap (nat.iterate nat.pred), begin
    ext1 n, ext1 m,
    induction m generalizing n,
    { simp [nat.sub, function.swap] },
    simp only [function.swap, function.iterate_succ_apply', nat.sub, nat.sub_succ, m_ih],
  end],
  apply_instance,
  -- maximum class-instance resolution depth has been reached
  -- (the limit can be increased by setting option 'class.instance_max_depth')
  -- (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')
end

The last one doesn't compile (I don't think any of the other proofs are important here, but I can provide more details if they are). With the error message in the comment. I'm wondering if this is improper use of instances because I'm matching on function names instead of types. As a human it looks pretty easy to unwrap the declaration (find an instance that matches function.swap, then find one that matches nat.iterate, then find the one for nat.pred).

[Eric Wieser]

I think the problem is that docs#function.swap is reducible and so flip_complexity forms a loop with itself

[Andrew Carter]

Ah, interesting. Wrapping a new function for flip worked, thanks @Eric Wieser .

[Eric Wieser]

Does docs#flip work for you?

[Andrew Carter]

Yes it does, not sure how I missed it, given it had the name I expected

[Andrew Carter]

A follow-up question (related mostly on the question of instance abuse).
I've defined the instance as follows

structure is_complexity {α: Type} [has_encodable_function α] (f: α):=
mk :: (cost : cost_function' α) (inv : complexity_le f cost)

class has_complexity {α: Type} [has_encodable_function α] (f: α) :=
  (value: is_complexity f)

def complexity {α: Type} [has_encodable_function α]  (f: α) [cf: has_complexity f] :=
  cf.value.1

is there a way for me to interact with the underlying cost function from an instance? Or is it quotiented away in some sense.
I.e.

def sc_cost: ℕ → ℕ → ℕ := λ n m, (2 * n + 15) * m + 5
theorem sc: (complexity nat.sub).always_le sc_cost :=
begin
  intros n m,
  simp [complexity, sc_cost],
  -- |- has_complexity.value.cost n m ≤ (2 * n + 15) * m + 5
  sorry,
end

[Reid Barton]

Sure it's possible, though it will be kind of hard to work with because you used rw to define data

[Reid Barton]

It would be better to define a function like docs#fin.cast that copies the data, and only rewrites in the proof

[Andrew Carter]

Thanks, I'll take a look