Extracting information from set comprehension

Stream: new members

[Logan Murphy]

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]

{x ∈ CM.X | CM.f x ∈ CM.sets_D i} is this even legal syntax? I didn't know that!

[Johan Commelin]

My guess is, if you #print preimages you'll get an answer to your question

[Logan Murphy]

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

[Johan Commelin]

assume x ∈ Xᵢ, it's probably the .1 of this hypothesis that you are looking for

[Logan Murphy]

Yep, since
#reduce {x ∈ S | x ∈ T}
prints
λ (a : α), S a ∧ T a . Thanks for the tip!

[Logan Murphy]

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]

Look for something with type x ∈ Xᵢ in your goal state, in the original context.

[Johan Commelin]

Logan Murphy said:

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

Yup...

[Logan Murphy]

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]

and.left H? Does that work?

[Johan Commelin]

Alternatively, write assume H : x ∈ CM.X \and _, instead of assume x ∈ Xᵢ,

[Logan Murphy]

term
H
has type
x ∈ Xᵢ
but is expected to have type
x ∈ CM.X ∧ ?m_1

[Logan Murphy]

will try that

[Logan Murphy]

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]

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