Zulip Chat Archive

Stream: new members

Topic: Match statement in type in structure


Josiah Eldon Bills (Sep 23 2022 at 23:08):

I am trying to define the type of potentially countably infinite binary strings. I have the following:

import order.bounded_order
import algebra.order.module

@[derive [
  has_zero, add_comm_monoid_with_one,
  canonically_ordered_comm_semiring, complete_linear_order, nontrivial,
  canonically_linear_ordered_add_monoid, has_sub, has_ordered_sub,
  linear_ordered_add_comm_monoid_with_top, decidable_eq]]
def extnat := with_top 

namespace extnat

instance : inhabited extnat := 0

end extnat

notation (name := extnat.top) `∞` := ( : extnat)


structure binstring :=
  (seq:   bool) (len: extnat) (proof: (match len with
                                        | none := true
                                        | some l := n  l, seq n = false
                                        end: Prop) )

Basically, finstring should be a sequence with a length, together with a proof that the sequence is 0 after the end of the length. I could probably also do this with a quotient instead, but this is the route I am trying first.

However this gives me the error "failed to register private name '_match_1', prefix has not been registered". What causes this error? What would the idiomatic way of writing the type of such a proof be? An alternative I am considering is (proof: len = ∞ ∨ (∃l: ℕ, len = l ∧ ∀n ≥ l, seq n = false))

Kyle Miller (Sep 23 2022 at 23:12):

FYI, your extnat is docs#enat

Kyle Miller (Sep 23 2022 at 23:13):

For the match expression, this seems to be a bug, but in any case I think it would be easier to work with proof: ∀n ≥ len, seq n = ff.

Kyle Miller (Sep 23 2022 at 23:14):

There's a coercion from nat to enat, so the statement will be vacuously true if len = ∞

Kyle Miller (Sep 23 2022 at 23:15):

You'll have to write it as ∀(n : ℕ), n ≥ len ∧ seq n = ff I believe (sorry, I haven't checked it in Lean)

Josiah Eldon Bills (Sep 23 2022 at 23:15):

All right, that makes sense


Last updated: Dec 20 2023 at 11:08 UTC