# Zulip Chat Archive

## Stream: new members

### Topic: Extracting information from set comprehension

#### Logan Murphy (Jul 20 2020 at 16:53):

I'm formalizing some proofs about labelled transition systems, so I've built some rather hairy structures to try and express them. I hope I can get my question across with the particular proof I'm working with, even though it isn't exactly a MWE of the phenomenon.

In the definition of pre_images below, I return the set of x ∈ CM.X satisfying the property indicated. In the following proof, when I assume I have an element of the set returned by pre_images, how can I get back to the original stipulation that x ∈ CM.X ?

```
structure LTS_Claim (M : LTS) (α : Type) extends LTS :=
(X : set (execution M))
(E : ∀ x ∈ X, valid x)
(P : execution M → Prop)
(C : ∀ x ∈ X, P x)
(f : execution M → α)
(n : ℕ)
(D : set α)
(sets_D : fin n → (set α))
(subs_D : ∀ (i : fin n), sets_D i ⊆ D)
/-
Given an LTS_Claim for an LTS M, pre_images returns an indexed family of sets of
executions of Xs = {X₁, X₂, ... Xₙ} where Xᵢ = {x | f(x) ∈ Dᵢ}
or at least, that's what I'm trying to accomplish.
-/
def preimages {M : LTS} {α : Type} (CM : LTS_Claim M α) : fin CM.n → set (execution M) :=
λ (i : fin CM.n), {x ∈ CM.X | CM.f x ∈ CM.sets_D i}
---------------------^^^^^^---------
---trying to pull out this information
---for the part of the proof indicated by ??
def domain_decomp {M : LTS} {α : Type} (CM : LTS_Claim M α ) : fin CM.n → LTS_Claim M α :=
begin
intro i,
have Xᵢ : set (execution M), from preimages CM i,
have H₀ : ∀ x ∈ CM.X, valid x, from CM.E,
have Eᵢ : ∀ (x ∈ Xᵢ), valid x, from
assume x ∈ Xᵢ,
show valid x, from
have H₁ : x ∈ CM.X, from ??
end
```

I hope this question makes sense, if not I can try to come up with a clearer example. Also, I'm still quite new to building arbitrary data structures and to lean in general so I assume the way I've set up my structure here is not the best way to do what I'm trying to do.

#### Johan Commelin (Jul 20 2020 at 17:05):

`{x ∈ CM.X | CM.f x ∈ CM.sets_D i}`

is this even legal syntax? I didn't know that!

#### Johan Commelin (Jul 20 2020 at 17:06):

My guess is, if you `#print preimages`

you'll get an answer to your question

#### Logan Murphy (Jul 20 2020 at 17:07):

I guess it is, although I should check that it means what I think it means.

#### Johan Commelin (Jul 20 2020 at 17:08):

`assume x ∈ Xᵢ`

, it's probably the `.1`

of this hypothesis that you are looking for

#### Logan Murphy (Jul 20 2020 at 17:09):

Yep, since

#reduce {x ∈ S | x ∈ T}

prints

λ (a : α), S a ∧ T a . Thanks for the tip!

#### Logan Murphy (Jul 20 2020 at 17:39):

Hmm, having trouble moving from

```
variable M : LTS
variable CM : LTS_Claim M α
variable i : fin CM.n
variable x : execution M
#reduce (preimages CM i x)
==> CM.X x ∧ CM.sets_D i (CM.f x)
```

to

```
have H₁ : (CM.X x ∧ CM.sets_D i (CM.f x)), from (preimages CM i x),
```

invalid type ascription, term has type

Prop : Type

but is expected to have type

CM.X x ∧ CM.sets_D i (CM.f x) : Prop

I think I'm confusing the proposition/type with the proof term itself

#### Johan Commelin (Jul 20 2020 at 17:44):

Look for something with type `x ∈ Xᵢ`

in your goal state, in the original context.

#### Johan Commelin (Jul 20 2020 at 17:45):

Logan Murphy said:

I think I'm confusing the proposition/type with the proof term itself

Yup...

#### Logan Murphy (Jul 20 2020 at 17:52):

still struggling with

```
assume x ∈ Xᵢ, -- gives assumption the name H
have H₁ : x ∈ CM.X, from H.1
```

invalid field notation, type is not of the form (C ...) where C is a constant

H

has type

Xᵢ x

Appreciate your help.

#### Johan Commelin (Jul 20 2020 at 17:52):

`and.left H`

? Does that work?

#### Johan Commelin (Jul 20 2020 at 17:54):

Alternatively, write `assume H : x ∈ CM.X \and _,`

instead of `assume x ∈ Xᵢ,`

#### Logan Murphy (Jul 20 2020 at 17:54):

term

H

has type

x ∈ Xᵢ

but is expected to have type

x ∈ CM.X ∧ ?m_1

#### Logan Murphy (Jul 20 2020 at 17:54):

will try that

#### Logan Murphy (Jul 20 2020 at 18:00):

I was able to write this lemma, which should be good enough.

```
lemma silly {M : LTS} {α : Type} (CM : LTS_Claim M α ) (x : execution M) (i : fin CM.n) : x ∈ preimages CM i → x ∈ CM.X := λ h, h.1
```

#### Logan Murphy (Jul 20 2020 at 18:01):

I guess renaming x \in preimage _ _ to x \in X\_1 obfuscates the conjunction somehow

Last updated: May 10 2021 at 00:31 UTC