Adding conditions for Structures

Stream: lean4

[Bach Hoang]

I am learning about structures, I was wondering there is anyway to add a condition to a structure.

For example, I am creating a Structure called Example as such

structure Example (α : Type) (A : Set Prop) where
  current : α
  condition : Prop
  next : α

In this example, I am wondering how to enforce that 'condition' has to belong to 'A' ?

[Kyle Miller]

structure Example (α : Type) (A : Set Prop) where
  current : α
  condition : Prop
  condition_prop : condition ∈ A
  next : α

[Kyle Miller]

Proofs are values too, so you can add them as a field like for any other value.

[Bach Hoang]

Thanks Kyle, if condition_prop is based on this, how can I initialize a 'Example' variable ?

[Bach Hoang]

As I am constructing an example myself, it keeps showing a 'Type mismatch error' when I initialize condition_prop with a True (since I need condition ∈ A) but Lean keeps telling me that condition_prop must have a type of
condition ∈ A

[François G. Dorais]

Hopefully you're initializing condition with an element of A?

[François G. Dorais]

Maybe a less generic mwe would help?

[Bach Hoang]

Here is an example that I am wondering what I am doing wrong

def set_proposition_example : Set Prop := {True, False, 1 > 2, 2 > 3}

def Example_1 : Example ℝ set_proposition_example :=
{
  current := 1,
  condition := 1 > 2,
  next := 2
  simple_condition := transition_example.condition ∈ set_proposition_example
}

[Bach Hoang]

But Lean keeps alert me this: "type mismatch
Example_1.condition ∈ set_proposition_example
has type
Prop : Type
but is expected to have type
(1 > 2) ∈ set_proposition_example : Prop"

[Giacomo Stevanato]

In simple_condition you have to put a proof tha 1 > 2 is in the set_proposition_example, what you're doing instead is just repeating the proposition statement.

simple_condition := by simp[set_proposition_example] should make it work.