failed to synthesize instance HasSSubset Prop

Stream: lean4

[Alexandre Rademaker]

This is the error I got in the definition of only when I tried to explore the automatic coercion from Prop to Set. What can be an alternative?

section
variable {x : Type}
variable {people : x → Prop}
variable {live_in_dreadbury : x → Prop}

def R (a : x) := people a ∧ live_in_dreadbury a

#check (R : Set x)

def only (P : x → Prop) := ∀ x, P x ∧ (∀ y, P y → P y ⊂  P x)

#check (only R)

end

[Raghuram]

IIRC, in mathlib Set x is defined to be x -> Prop, so the first #check involves no coercion - note that R : x -> Prop is not itself a Prop, so there is no conversion from Prop to Set involved.
If you replaced it with #check fun (a : x) => (R a : Set x) you would probably get an error.

In the definition of only you have written P y ⊂ P x in a context where P y and P x are of type Prop (not x -> Prop this time). There is no coercion from Prop to Set x.
This notation is syntactic sugar, which is expanded using a typeclass, HasSSubset in this case.
If someone had written an 'instance' of this typeclass for Prop, then Lean would interpret P x ⊂ P y as whatever that instance said. Since nobody has (and nobody should), you get the error you see.

[Raghuram]

As for an alternative, it's not clear to me what you want only to be.
The condition looks like only P would require P a to hold for all a : x --- which already determines P uniquely (e.g., by Set.ext).

[Raghuram]

Are you trying to define the property of a predicate being satisfied by a unique element? That can be defined as follows (and is probably in Mathlib under some other name).

def isOnlyElement (a : x) (P : x -> Prop) : Prop := P a ∧ ∀ b, P b -> b = a

[Alexandre Rademaker]

I appreciate your attention to my question. Indeed, after reading more carefully Mathematics in Lean, I understand that R : Set α by definition is R: α → Prop. But I didn't pay attention to R (a : α) meaning a ∈ R. If I want to say A ⊂ B, that means I have two functions A : α → Prop and B: α → Prop such that ∀ a, A a → B a.

The example came from a text on formal semantics for the natural language sentence:

they are the only people who live therein.

The presentation is confusing and I was trying to convert to Lean! It seems not a resonable formalization after all.

[[people who live therein]] would be a property of sets of people living in Dreadbury
\X -> people(X) & live_in_Dreadbury(X)

and [[only]] would be a property modifier

\P \X -> P(X) & forall Y: P(Y) => Y < X

(where Y < X means that Y is a part of X)

Putting them together, [[only people who live therein]] is

\X -> people(X) & live_in_Dreadbury(X) & forall Y: (people(Y) & live_in_Dreadbury(Y)) => Y < X

In words, this holds of X iff X is the maximal set of people living in Dreadbury.

[Alexandre Rademaker]

Continuing my goal to formalize plurals from natural language, I need a way to lift a predicate from an element to a set of elements. My problem is that live₁ and live₂ below should be equal by definition. Why can't I finish the proof of the example with reflection?

section

variable (u : Type)
variable (live : u → Prop)
variable (live₁ : Set u → Prop)
variable (live₂ : (u → Prop) → Prop)

def plur {u : Type} (p : u → Prop) : Set u → Prop :=
  λ x => ∀ y, p y → x y

#check live
#check (plur live)
#check ∀ (a : Set u), (plur live) a
#check ∀ (a : u), live a

example : ∀ a, live₁ a = live₂ a := by
 intro h
 rfl

The error I got is

type mismatch
  HEq.rfl
has type
  HEq ?m.229 ?m.229 : Prop
but is expected to have type
  live₁ h = live₂ h : Prop

[Kyle Miller]

live₁ and live₂ are two different predicates on sets, so there's no reason they need to be equal

[Alexandre Rademaker]

I'm ashamed of my previous message... for some reason, my mind fixed a crazy interpretation of the code. Your message made me wake up... sorry for the question... hahaha

Indeed, nothing tells me that the two properties with the same signature need to be equal -- even considering that all elements of a given type have the same value for the properties. Actually, I was just trying to validate that a type for live1 also works for live2 (same signature). This can be verified with the simple #check below:

#check ∀ a, live₁ a ∧ live₂ a