Propositions as Types and Antipatterns

Stream: lean4

[Nathan]

I have a few questions..

Given propositions,

variable {this_is_about_w : Prop}
variable {this_is_about_x : Prop}
variable {this_is_about_y : Prop}
variable {this_is_about_z : Prop}
.
.
.

Is there an appropriate way to type inference rules and type new variables from existing variables?

Why are the following type definitions, invalid?

variable {w_and_x_and_y : this_is_about_w ∧ this_is_about_x ∧ this_is_about_y}

and

variable {expression : w_and_x_and_y}

Much appreciated!

[James Gallicchio]

In your example, I think everything is fine until the last variable -- w_and_x_and_y is not a proposition (ie a type), rather it's a proof of this_is_about_w /\ .... And proofs can't appear in type position, since they're not types, so the last variable declaration should complain

[James Gallicchio]

(does that answer what you were asking about?)

[Hyun Kim]

Does anyone know where to find the solutions to the exercises from the Lean Theorem Prover: https://leanprover.github.io/logic_and_proof/sets_in_lean.html.

[Nathan]

Thanks James Gallicchio and Hyun Kim.

Yes.

To represent, "a proposition for a theory in T' is a proof in theory T," I was under the impression I could coerce the expression 'this_is_about_w ∧ this_is_about_x ∧ this_is_about_y' to be a Proposition through defining it the way I had.

Sorry to be so convoluted.

[Alistair Tucker]

To give a name to that conjunction you can write

def this_is_about_w_and_x_and_y : Prop :=
  this_is_about_w ∧ this_is_about_x ∧ this_is_about_y

or

structure this_is_about_w_and_x_and_y where
  hw : this_is_about_w
  hx : this_is_about_x
  hy : this_is_about_y