# 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',
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