Zulip Chat Archive

Stream: new members

Topic: resetting instance cache in term mode?

Matt Diamond (Aug 14 2022 at 00:28):

Is there a way to reset the instance cache when writing definitions in term mode? I'm wondering if there's a cleaner way to write this:

def comp_dec {α : Type*} {p : α  Prop} (d : decidable_pred p) (f : α  α) : decidable_pred (p  f) :=
λ a, dite (p (f a)) is_true is_false

def ε : Π (n : ) (p : cantor  Prop) [decidable_pred p], cantor
| 0 _ _         := λ _, zero
| (n+1) p p_dec :=
  let p_zero := p  cons zero,
      p_one := p  cons one,
      p_zero_dec := comp_dec p_dec (cons zero),
      p_one_dec := comp_dec p_dec (cons one),
      ite_prop_dec := p_zero_dec (@ε n p_zero _›) in
  @ite _ (p_zero (@ε n p_zero _›)) _
    (zero :: @ε n p_zero _›)
    (one :: @ε n p_one _›)

(The type cantor is an alias for stream bit, where bit is an enumerated type with values of zero or one.)

This function performs a limited search of the Cantor space, and you can see that it involves a lot of passing around decidable and decidable_pred instances. I'm wondering if there's a way to avoid that... like an equvalent of resetI but for term mode. This would allow me to get rid of comp_dec, which I think is only necessary because Lean doesn't know that the function being composed is decidable.

Last updated: Dec 20 2023 at 11:08 UTC