Proving things on rewritten terms

Stream: general

[Artem Yurchenko]

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',
  sorry,
}

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]

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]

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

[Alex J. Best]

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]

@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]

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

[Artem Yurchenko]

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

[Alex J. Best]

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).