BEq and LawfulBeq of Sequences (Fin n -> a)

Stream: lean4

[Martin Ceresa]

Hello everyone!
I am kinda stuck, maybe I am not seeing something trivial here.
Let me know if this channel is not the correct one.

So, I want to define BEq and LawfulBEq for finite Sequences.

abbrev Sequence (n : Nat) (α : Type) := Fin n -> α

So, I would like to define a simple BEq as there are several ways to do it I
guess:

instance beq_sequences {α : Type}[BEq α]{n : Nat} : BEq (Sequence n α) where
  beq sl sr :=
    match n with
   | .zero => true
   | .succ _pn => headSeq sl == headSeq sr
                  && beq_sequences.beq (Fin.tail sl) (Fin.tail sr)

And finally, I would like to show something on the lines of

instance law_full_beq_seq {α : Type}[BEq α][LawfulBEq α]{n : Nat}
  : LawfulBEq (Sequence n α) where
  eq_of_beq := _
  rfl := _

The problem is that when proving 'eq_of_beq' I have no way of getting
information from the statement '(a == b) = true'. I gave one definition of
'(==)' before at 'beq_sequences', but here '==' may be something else.

Does that make sense? What do you recomend?

I am using these Sequences for something else and it should be rudimentary.
The 'main' proof of this section is about a transformation from sequences to
trees and back. Something on the lines of:

theorem split_seq_eq {α : Type}{n m : Nat}{ mLTn : m ≤ n }( seq : Sequence n α ):
  have ⟨ seql , seqr ⟩ := splitSeq seq m mLTn
  HEq seq (concatSeq seql seqr)

theorem concat_perfect_split {α : Type}[BEq α]{n : Nat}(seq : Sequence ((2^n.succ.succ) - 1) α)
  : let ⟨ seql, m , seqr ⟩ := seqPerfectSplit seq
  seq = (concatSeq seql (Fin.cons m seqr))

Thank you very much for your time!

[Edward van de Meent]

it seems that the BEq and LawfulBEq variants of docs#Fintype.decidablePiFintype are missing (and exactly what you need)

[Edward van de Meent]

(although that will result in slightly different defeq for you)

[Martin Ceresa]

True! Maybe I can take some inspiration from the ones already defined!
Thanks!!

[Martin Ceresa]

Well, I ended up doing something not so very nice, just to be sure that I am in the good (?) path:

theorem split_seq_eq {α : Type}{n m : Nat}{ mLTn : m ≤ n }( seq : Sequence n α ):
  have ⟨ seql , seqr ⟩ := splitSeq seq m mLTn
  seq = sequence_coerce (by omega) (concatSeq seql seqr)

The function sequencu_coerce simply enable me to match sequence lenghts:

def sequence_coerce {α : Type} {n m : Nat}( hEq : n = m )(s : Sequence n α) : Sequence m α

With that and some funext, it is easy to prove.
I will take a look to see if I can define some more generic notions and maybe suggest something nice :D!
It is a way of having a notion of hidden HEq, but it is working fine :D

Cheers!!

[Kyle Miller]

Just to check, are you defining BEq for programming purposes? Will you ever be wanting to use Sequence with an underlying type that doesn't satisfy LawfulBEq?

If the answer to the first question is "no", then you may as well use plain old = instead. Otherwise, if the answer to the second question is "no", it might be better to define a DecidableEq instance instead of defining BEq.

[Kyle Miller]

Side note: you likely don't want the definition of Sequence to be abbrev, given that you are putting instances on it. The effect is actually that you're putting an instance on Fin n -> α itself, since the typeclass system unfolds abbrevs.

[Kyle Miller]

Here's a DecidableEq instance in case it's helpful (I have mathlib imported, and I haven't checked that the simps are not making use of mathlib or batteries theorems). You might like the Sequence.beq definition. I found that rewriting with Nat.all_eq_finRange_all enables a reduction to a forall, and then simp handles the rest.

def Sequence (n : Nat) (α : Type) := Fin n -> α

def Sequence.beq {n : Nat} {α : Type} [BEq α] (sl sr : Sequence n α) : Bool :=
  Nat.all n fun i h => sl ⟨i, h⟩ == sr ⟨i, h⟩

instance {α : Type} [DecidableEq α] (n : Nat) : DecidableEq (Sequence n α) :=
  fun sl sr =>
    decidable_of_iff (Sequence.beq sl sr) <| by
      constructor
      · intro h
        apply funext
        simpa [Sequence.beq, Nat.all_eq_finRange_all] using h
      · rintro rfl
        simp [Sequence.beq, Nat.all_eq_finRange_all]

[Martin Ceresa]

Hello! What I am implementing in Lean is not purely mathematical, but a mix between programming and proving. If that anwsers the your questions.
I thought the usual steps were to define BEq and then LawfulBEq, but it seems I am wrong.

I developed almost everything without instances so far and abbrev was working just fine. Although defining Sequences as it's own "type" may be a good idea in a final version.

The endgoal here is to have something close to HEq actually. "Heterogeous" in the length of the Sequence. When you start working with sequences, some operations may modify the length of the sequences, and thus, we need to have a notion that enable us to prove equivalence while computing at the length parameter.
I called that sequence_coerce and just used = as you suggested :muscle: . The problem here is that I need to explictly use this coerce function when I am manipulating the length and make some extra annotations.

I was worried because I was not understanding how to prove it. But I think I was wrong about instances, DecidableEq seems to be what I wanted.

[Martin Ceresa]

Also, funny thing. My Nat.all is different from yours.
The documentation here says it has the type you have, but the use part all f n = true is wrong.
Maybe I need to update my system.

[Martin Ceresa]

Okay, last notes.

• Mathlib is required, in particularList.mem_finRange mapping elements from Fin n to finRange (basically).
• So, my original question was how to get something to work with, because when defining a definition of BEq I am just giving one but when proving LawfulEq I did no have it in my context. I think this is what @Kyle Miller showed me how to do it properly through decidable_of_iff (plus some useful questions and insights). Thanks a lot!!

[Kyle Miller]

If you want to work with finite sequences of varying lengths, it's hard to beat List α. You can restrict to particular lengths like so:

def Sequence (n : Nat) (α : Type) := { xs : List α // xs.length = n }

(In mathlib this is docs#Mathlib.Vector, though it's not particularly well developed.)

[Kyle Miller]

Martin Ceresa said:

I thought the usual steps were to define BEq and then LawfulBEq

= is the true mathematical equality that every type comes with, and BEq is a user-implemented operation that happens to be equivalent to = if you prove LawfulBEq. Generally = is easier to work with, since to work with == in proofs you usually have to convert it to = first anyway.

I think this tends to trip up people who come from languages like Haskell, where you need to implement a typeclass to get access to = at all. In programming there's usually not a concept of true mathematical equality, since it's not something you can necessarily compute with. But Lean does come with such an equality. Lean has this decidability system to synthesize decision procedures for mathematical concepts; the DecidableEq instance for example lets an = that appears in an if condition to be evaluated.

[Kim Morrison]

(Mathlib.Vector was just renamed to docs#List.Vector)

[Martin Ceresa]

I am checking List.Vector and it has kinda the same operations that I defined. That's cool, I am going to port it (one of these days).
Thank you!!