## 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',
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 (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: Dec 20 2023 at 11:08 UTC