Extract constituents of a Prop?

Stream: general

[Marvin]

When I write an expression that resolves to a Prop, is there any way for me to get back what the operands of the expression were afterwards?

axiom Noun : Type

axiom john : Noun
axiom alice : Noun

axiom loves : Noun → Noun → Prop

def p : Prop := loves john alice

-- hypothetical code I want:
def subject := p.second -- john
def verb    := p.first  -- love
def object  := p.third  -- alice

I know that if a conjuction Prop is expressed as a type instead of as a value, you can use And.left to extract it:

def p : loves john alice ∧ loves alice john := sorry

#check p.left -- john loves alice

But that doesn't suffice for my use case where I store propositions as values.

Is there any way to do this? I know I can create my own intermediary representation before resolving to a Prop, but is there another route already in the language I can leverage?

[Filippo A. E. Nuccio]

I'm slightly confused by the questions: just to understanding the setting, are you aware of "proof irrelevance"/"impredicativity" or are these terms new to you (which is of course fine, they certain were to me when I started off with Lean!)? Also, when you speak about an "expression resolving to Prop" do you mean a type in Prop or a term in some type itself in Prop? And, finally, are you aware of the difference between the commands #check and #eval?

[Kevin Buzzard]

p.second can't exist because if p and q are arbitrary provable Props in lean than you can prove p = q from which you can deduce p.second = q.second. You can define .second at the meta (Expr) level (and then you can't prove any theorems about it) or you can make your own type of loving relationships, including an evaluation function to Prop, and do what you want with it.