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

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

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