Zulip Chat Archive

Stream: general

Topic: Proving things on rewritten terms

Artem Yurchenko (Mar 15 2022 at 14:13):

Hi! I may try to explain the problem, but it's probably more clear for you to see for yourself what it is.

I'm trying to finish the following proof in Lean 3:

import data.finset

structure matset (α : Type*)
:= (set : finset α)
   (mat : array set.card α)
   (equiv :  x, x  set  x  mat)

def insert {α} [decidable_eq α] : matset α  α  matset α
| s el := by {
  by_cases h : el  s.set,
    exact s,
  let set' := s.set.cons el h,
  let mat' := s.mat.push_back el,
  refine set', _, _⟩,
    rw finset.card_cons h,
    exact mat',

Here's the goal and the context:

α : Type ?,
_inst_1 : decidable_eq α,
insert : matset α  α  matset α,
s : matset α,
el : α,
h : el  s.set,
set' : finset α := finset.cons el s.set h,
mat' : array (s.set.card + 1) α := s.mat.push_back el
  (x : α), x  set'  x  _.mpr mat'

It would be trivial, if not for mpr , caused by rewrite. I wonder what is the best way to approach it without changing the matset type?

Thanks a lot for any help.

Logan Murphy (Mar 15 2022 at 14:51):

I'm not sure if it makes things any easier, but you can swap the .mpr for a cast :

def insert {α} [decidable_eq α] : matset α  α  matset α :=
λ s a,
if h : a  s.set then s else
   set := s.set.cons a h,
   mat :=
         let mat' := s.mat.push_back a in
         let h' : (array ((finset.card s.set) + 1) α) = (array (finset.cons a s.set h).card α) :=
            by {rw finset.card_cons,} in
         cast h' mat',
   equiv := by { simp, sorry,}
  -- ⊢ ∀ (x : α), x = a ∨ x ∈ s.set ↔ x ∈ cast _ (s.mat.push_back a)

Artem Yurchenko (Mar 15 2022 at 14:54):

Thanks @Logan Murphy! I also tried to solve for this goal, but wasn't successful

Alex J. Best (Mar 15 2022 at 15:12):

Do you really need to use array for what you are doing? As you are seeing its quite awkward as it is a dependent type. If you can use list instead I think things will be a lot easier.

Artem Yurchenko (Mar 15 2022 at 17:52):

@Alex J. Best Some other operations that I define on it seem to be _much_ less awkward and more efficient to define in terms of indices.
One operation is fold: def fold (s : matset β) : α → (α → s → α) → α. The other is random: def element_random (s : matset α) (s_nonempty : s.nonempty): rand s.
Just iterating over a list doesn't help, because it doesn't carry a proof of "belonging" to the matset, which is trivial to get for arrays with array.read_mem.

Yaël Dillies (Mar 15 2022 at 17:53):

Why do you even carry around the finset? You can reconstruct it from the array.

Artem Yurchenko (Mar 15 2022 at 17:55):

I often need to recreate a set from the array, so I carry it around, kind of "cached"

Alex J. Best (Mar 15 2022 at 17:58):

Mathlib has a docs#finset.fold, is that helpful? Also to get a proof of belonging you can use docs#finset.attach (or docs#list.attach).

Last updated: Aug 03 2023 at 10:10 UTC