Zulip Chat Archive

Stream: new members

Topic: Proofs as structure fields


view this post on Zulip Logan Murphy (Jul 20 2020 at 19:23):

I hope it's okay that I start a new topic, even though I'm working with the same structure. I'm hoping someone might be able to suggest a possible strategy and that I haven't set myself up for failure.

So I've got my base structure, one of which's fields is evidence that a predicate on executions holds for every execution in the structure.

structure LTS_Claim (M : LTS) (α : Type) extends LTS :=
(X : set (execution M))
...
(P : execution M  Prop)
(C :  x  X, P x)                 -- C is for Claim
...

I've also built a function which takes an LTS_Claim and turns it into an indexed family of LTS_Claims partitioned according to the pre-images of some evaluation function.

def domain_decomp {M : LTS} {α : Type} (CM : LTS_Claim M α ) : fin CM.n  LTS_Claim M α :=
begin
intro i,
let X := preimages CM i,
have HX : set (execution M), from preimages CM i,
...
have C :  x  X, CM.P x, from
...
exact LTS_Claim.mk M X E CM.P C CM.f CM.n CM.D CM.sets_D CM.subs_D
end

I want to try to express a relation between and LTS_Claim and an indexed family of LTS_Claims which says that the conjunction of every claim C in the indexed family implies the original structure's claim.

def foo {M : LTS} {α : Type} (Original_CM : LTS_Claim M α) (CMs : fin Original_CM.n  LTS_Claim M α) : Prop :=
-- (CM₀.C ∧ CM₂.C ∧ ... ∧ CMₙ.C) → Orgininal_CM.C

I've tried a variety of ways of extracting the "C" fields from the indexed family of claims, but I'm worried that I may have painted myself into a corner by defining C as a term of type (∀ x ∈ X, P x) rather than a term of type Prop. Should I be able to find a way to accomplish this?

view this post on Zulip Yakov Pechersky (Jul 20 2020 at 19:29):

\forall x \in X, P x is a proposition too

view this post on Zulip Logan Murphy (Jul 20 2020 at 19:40):

Right, and so one of my ideas was to do something like

def claim_set {M : LTS} {α : Type} (Original_CM : LTS_Claim M α) (CMs : fin Original_CM.n  LTS_Claim M α) : set Prop :=
 i : fin Original_CM.n, { p : Prop | p = (CMs i).C}

but lean complains that (CMs i).C is not of type Prop

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 20:22):

(deleted)

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 20:23):

What does it think the type is? It might be asking for some random other inputs. Lean is pretty good at telling you the types of things.

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

It reads the type as : ∀ (x : execution M), x ∈ (CMs i).X → (CMs i).P x : Prop . Does this mean I am supposed to provide more arguments?

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 20:30):

I don't really understand your question. Are you saying "I want something to have type Prop but it has type ∀ (x : execution M), x ∈ (CMs i).X → (CMs i).P x?

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 20:30):

Why don't you post some complete working code?

view this post on Zulip Logan Murphy (Jul 20 2020 at 23:02):

I guess the core problem is that I'm struggling with taking an indexed family of structures with fields (C : ∀ x ∈ X, P x), and writing a function which can express the conjunction of the individual C fields. Here's the whole file I'm working with.

-- Basic Transition System,
structure LTS  :=
mk :: (S : Type) (A : Type) (TransRel : set (S × A × S))

inductive execution (M : LTS)
| init {} : M.S  execution
| cons  :  M.A × M.S  execution  execution
open execution
notation e  p := cons p e

-- Given a finite execution in an LTS M, extract its current (latest) state
def cur_st : Π {M : LTS}, execution M  M.S :=
begin
intros M eM,
cases eM with x p eM',
   {exact x},
   have x : M.S, from p.snd,
   exact x
end

/-
Predicate on executions that they are valid
with respect to the transition relation of the
corresponding LTS
-/


def valid {M : LTS} : execution M  Prop
| (init x) := true
| (cons p e) := ((p.snd, p.fst, cur_st e)  M.TransRel)  (valid e)

/-
 An LTS_Claim consists of an LTS with :
- A set X of executions of the LTS about which the claim is made
- Evidence E that all executions in the above set are valid in M
- Some predicate P of executions in M
- A claim C that the above is predicated of all executions in X
- some valuation function f from executions of M to values of α
- set D of values with the type α,
- set of sets of type α ;
- Evidence that elements the above set are universally subsets of D
-/


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, [preimages] 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}



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

/-
Turns and LTS claim into an indexed family of LTS claims
according to how the evaluation function f partitions the
original set X.
CM read as "claim for system M"
(definitely not the most concise proof)
-/

def domain_decomp {M : LTS} {α : Type} (CM : LTS_Claim M α ) : fin CM.n  LTS_Claim M α :=
begin
intro i,
let X := preimages CM i,
have HX : set (execution M), from preimages CM i,
have H₀ :  x  CM.X, valid x, from CM.E,
have E :  x  X, valid x, from
   begin
   intro x,
   intro H₁,
   apply H₀,
   apply helper CM x i,
   apply H₁,
   end,
have C :  x  X, CM.P x, from
   begin
   intro x,
   intro H₁,
   have CMC :   x  CM.X, CM.P x, from CM.C,
   apply CMC,
   apply helper CM x i,
   apply H₁,
   end,
exact LTS_Claim.mk M X E CM.P C CM.f CM.n CM.D CM.sets_D CM.subs_D
end

/-
   The actual idea I'm trying to formalize now:
   Given an LTS_Claim "CM" and an indexed family of LTS_Claims [CM₁, CM₂, ... CMₙ],
   the two are said to be in a  special relation if
   CM₁.C ∧ CM₂.C ∧ ... ∧ CMₙ.C → CM.C
   I.e. the evidence that the property P holds for the sets X_i

-/

/-
One strategy:

Given a family of LTS_Claims, take the set of their "C" fields
The idea is that if I can form this set, I can (maybe) take their conjunction.

-/
def set_claims {M : LTS} {α : Type} {original : LTS_Claim M α}
(subclaims : fin original.n  LTS_Claim M α) : set Prop := sorry

view this post on Zulip Logan Murphy (Jul 20 2020 at 23:10):

But I feel like I'm stuck between considering the "C" fields as evidence or as propositions, and so I need to clarify that distinction before I will be able to find a solution. Again, sorry for the messy code and confusing questions.

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 23:11):

And what is the question?

view this post on Zulip Logan Murphy (Jul 20 2020 at 23:14):

Given an indexed family of structures, each of whom has a field C proving a proposition, how can you form the set of those fields?

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 23:14):

And why do you want to make such a set?

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 23:14):

Lean doesn't have sets, it only has subsets of types

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

right. I think I need to re-evaluate what exactly I'm trying to show. Thanks for the patience

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 23:18):

CM₁.C ∧ CM₂.C doesn't make sense.

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 23:18):

If P : Prop and Q : Prop then P ∧ Q makes sense.

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 23:19):

If h : P and j : Q then h ∧ j doesn't make sense.

view this post on Zulip Logan Murphy (Jul 20 2020 at 23:19):

Yeah that's part of the problem. I want to take the conjunct of the propositions which are the types of CM1.C and CM2.C. So maybe I need to redefine the fields as arbitrary Prop's

view this post on Zulip Logan Murphy (Jul 20 2020 at 23:19):

exactly right

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 23:21):

So you know the type of a.C, it's ∀ x ∈ a.X, a.P x

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 23:21):

and ∀ x ∈ a.X, a.P x : Prop

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 23:23):

You only need to define a.X and a.P to define this type. There's no point defining a.C to equal ∀ x ∈ a.X, a.P x, you already have a name for that and it's ∀ x ∈ a.X, a.P x

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 23:24):

The question is whether to construct a : LTS_Claim M alpha you want to be demanding a proof of ∀ x ∈ a.X, a.P x or not.

view this post on Zulip Reid Barton (Jul 20 2020 at 23:24):

I would suggest adjusting language to not refer to proofs by name

view this post on Zulip Reid Barton (Jul 20 2020 at 23:25):

e.g.

 An LTS_Claim consists of an LTS with :
- A set X of executions of the LTS about which the claim is made
- which are valid in M
- Some predicate P of executions in M
- that holds on all executions in X
- some valuation function f from executions of M to values of α
- set D of values with the type α,
- set of sets of type α ;
- which are subsets of D

view this post on Zulip Logan Murphy (Jul 20 2020 at 23:27):

Yeah that's a good point. I guess can always just define predicates on the claims which are the atcual propositions I want to reason about.

view this post on Zulip Logan Murphy (Jul 20 2020 at 23:28):

(deleted)

view this post on Zulip Reid Barton (Jul 20 2020 at 23:40):

also, I don't have a good sense of what you are trying to do, but it seems like your "claims" are more like theorems, because you require proofs, and this is why you are having a hard time writing something that makes sense

view this post on Zulip Reid Barton (Jul 20 2020 at 23:41):

I mean there are a lot of moving parts whose purpose I don't know

view this post on Zulip Reid Barton (Jul 20 2020 at 23:41):

but certainly given a bunch of propositions P1, P2, ..., Pn, P we can form the proposition P1 /\ P2 /\ ... /\ Pn -> P

view this post on Zulip Reid Barton (Jul 20 2020 at 23:41):

but if we also already have proofs of all the propositions then it's not a very interesting thing to do

view this post on Zulip Reid Barton (Jul 20 2020 at 23:41):

since all the propositions are just equal to true anyways

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 23:42):

A Proposition is a true/false statement, for example 2+2=4 or 2+2=5. Propositions have type Prop. If P is a proposition then you can think of it as a type with one term if it's true, and with 0 terms if it's false. If h : P then h can be thought of as a proof of P. For example it's possible to make a term of type 2 + 2 = 4 in Lean, but it's not possible to make a term of type 2 + 2 = 5.

view this post on Zulip Kevin Buzzard (Jul 20 2020 at 23:44):

Things like 2+2=4 \or 2+2=5 and 2+2=4 \and 2+2=5 make sense, and are also Propositions.

view this post on Zulip Logan Murphy (Jul 21 2020 at 00:48):

Thanks for the thorough explanation guys. I'm actually just trying to strong-arm a colleague's paper about decomposing Safety Cases/Goal Structuring Notation into Lean post hoc, which is part of why it seems awkward (I'm also just still pretty green with Dep. TT). I'm still really enjoying working with Lean in spite of the learning curve though :)


Last updated: May 12 2021 at 23:13 UTC