Restricting structure instantiation

Stream: lean4

[Arthur Paulino]

I am refining my definition of DataFrame and I've realized that one can instantiate a DataFrame with rows of arbitrary size, not necessarily consistent with the header size:

structure DataFrame where -- will just use strings for the sake of MWE simplification
  header : List (String × String)
  rows : List (List String)

Can I attach some piece of code to my structure that runs on instantiation and makes Lean panic if there's an inconsistency between the dimensions?

[Marcus Rossel]

I'm not sure what exact restriction you're looking for, but you can add fields to the structure that enforce properties:

structure DataFrame where
  header : List (String × String)
  rows : List String
  eqDim : header.length = rows.length

[Arthur Paulino]

It's definitely something like that, but I want every item of rows to have the same length as header

[Arthur Paulino]

(That is, the data is in fact as wide as the header says)

[Arthur Paulino]

I will try to apply your idea with a reduce

[Arthur Paulino]

Hm, we don't seem to have a native reduce for lists yet. I will try to make one

[Marcus Rossel]

I'm not familiar with database stuff, so I'm not sure what "same length as header" means.
Do you mean that the length of every string in rows should be equal to the length of the header list?

[Arthur Paulino]

Oops, there's a mistake in my definition. let me fix it

[Arthur Paulino]

There, now I think it will make more sense

[Marcus Rossel]

Then:

...
  eqDim : ∀ r ∈ rows, r.length = header.length

should do it.

[Arthur Paulino]

Oh, I thought \forall was a mathlib (Lean 3) thing :smiley:

[Arthur Paulino]

Thanks!!

[Notification Bot]

Arthur Paulino has marked this topic as resolved.

[Marcus Rossel]

No, ∀ is very much a part of Lean.

[Arthur Paulino]

I guess I should have tried first :sweat_smile:

[Notification Bot]

Arthur Paulino has marked this topic as unresolved.

[Arthur Paulino]

Hm, actually this is not exactly what I need. This solution forces the user to provide a proof that the constraint is true everytime they want to instantiate a DataFrame. I was thinking more of a code that runs pre (or post) instantiation and throws an exception when the restriction is not satisfied

[Arthur Paulino]

(Also Lean didn't recognize ∈ :thinking:)

[Arthur Paulino]

(deleted)

[Henrik Böving]

Arthur Paulino said:

Hm, actually this is not exactly what I need. This solution forces the user to provide a proof that the constraint is true everytime they want to instantiate a DataFrame. I was thinking more of a code that runs pre (or post) instantiation and throws an exception when the restriction is not satisfied

you could try to use default values and apply a tactic like simp per default I guess? I'm not sure how good that would work in the general case though.

[Arthur Paulino]

Henrik Böving said:

you could try to use default values and apply a tactic like simp per default I guess? I'm not sure how good that would work in the general case though.

I tried it (but using rfl instead). It works for manual instantiations but is a bit of a pain when inside other functions (using generic variables)

[Yakov Pechersky]

Well you have to prove that those functions retain your invariant

[Yakov Pechersky]

Otherwise they can make dataframes exactly breaking your invariant

[Yakov Pechersky]

In mathlib3, you can use something like . tactic.exact_dec_trivial to do default computation:
https://github.com/Julian/lean-across-the-board/blob/main/src/chess/board.lean#L67-L77

[Arthur Paulino]

Yeah I am starting to understand the beauty of Lean to build correct software

[Arthur Paulino]

It's sinking in slowly