Zulip Chat Archive

Stream: new members

Topic: Extracting information from set comprehension


view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Johan Commelin (Jul 20 2020 at 17:06):

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

view this post on Zulip Logan Murphy (Jul 20 2020 at 17:07):

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

view this post on Zulip Johan Commelin (Jul 20 2020 at 17:08):

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

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 20 2020 at 17:44):

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

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jul 20 2020 at 17:52):

and.left H? Does that work?

view this post on Zulip Johan Commelin (Jul 20 2020 at 17:54):

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

view this post on Zulip 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

view this post on Zulip Logan Murphy (Jul 20 2020 at 17:54):

will try that

view this post on Zulip 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

view this post on Zulip 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