Proofs as structure fields

Stream: new members

[Logan Murphy]

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?

[Yakov Pechersky]

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

[Logan Murphy]

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

[Kevin Buzzard]

(deleted)

[Kevin Buzzard]

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.

[Logan Murphy]

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?

[Kevin Buzzard]

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?

[Kevin Buzzard]

Why don't you post some complete working code?

[Logan Murphy]

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

[Logan Murphy]

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.

[Kevin Buzzard]

And what is the question?

[Logan Murphy]

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?

[Kevin Buzzard]

And why do you want to make such a set?

[Kevin Buzzard]

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

[Logan Murphy]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Logan Murphy]

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

[Logan Murphy]

exactly right

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Reid Barton]

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

[Reid Barton]

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

[Logan Murphy]

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.

[Logan Murphy]

(deleted)

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

since all the propositions are just equal to true anyways

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Logan Murphy]

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 :)