Subsets

Stream: maths

[Victor Porton]

Why doesn't

theorem subsubset {α β γ: Type} (c: α → Prop) (d: α → Prop) : --[decidable_pred c]
 ∀x,(d x → c x) → { x: α // c x ∧ d x } = { y: {x:α // c x} // d y }
 sorry;

compile? (Lean 3)

[Victor Porton]

It says that {x:α // c x} is Type, but it indeed should be a Type. What's wrong?

[Patrick Johnson]

You are missing :=. Lean thinks that you're trying to call function { y: {x : α // c x} // d y } with argument sorry.
This compiles fine:

example {α β γ : Type} (c d : α → Prop) :
  ∀ (x : α), (d x → c x) → {x // c x ∧ d x} = {y : {x : α // c x} // d y} :=
begin
  sorry
end

[Victor Porton]

Does Lean3 have a powerful SMT? How to call it?

[Patrick Johnson]

Note that // is for subtypes, not subsets. You probably want this instead:

import tactic

example {α β γ : Type} (c d : α → Prop) :
  ∀ (x : α), (d x → c x) → {x | c x ∧ d x} = {y ∈ {x : α | c x} | d y} :=
by simp

[Victor Porton]

@Patrick Johnson What is the difference of sets vs types? Is it that sets are the lowest level, while types have an infinite hierarchy of sorts?

[Julian Berman]

No, Lean is based on glossary#dependent-type-theory, so types are the primitive concept, sets are built on top of them, and less commonly used

[Victor Porton]

Victor Porton said:

Does Lean3 have a powerful SMT? How to call it?

Yes, https://github.com/leanprover/super works in Lean3.

[Julian Berman]

(At a basic level, conceptually thinking of types as just sets, but where you can't ask "nonsensical" questions like "is 2 an element of 3 given they're both possibly defined as sets" is a simplistic mental model)

[Kevin Buzzard]

It's probably also worth mentioning that another difference is that the type goal which Patrick left you is probably not solvable, because equality of types is poorly behaved. This is why they suggested the set goal.

[Victor Porton]

import super

open quotient
theorem subsubset {α β γ: Type} (c: α → Prop) (d: α → Prop) : --[decidable_pred c]
 ∀x,(d x → c x) → { x: α // c x ∧ d x } = { y: {x:α // c x} // d y } :=
 by super

does not verify. Why?
a. super tactic is a weak SMT.
b. Not all necessary axioms were introduced.
c. super needs explicit arguments to introduce axioms.

[Victor Porton]

I am trying to check if there is or there is no royal road in Lean to easily prove theorems just passing assumptions and making big steps in "human" way by using super SMT.

[Victor Porton]

By "human" way I mean not specifying any other tactics except of super.

[Kevin Buzzard]

Your theorem is an equality of types so is probably undecidable in Lean, no tactic will prove it

[Kevin Buzzard]

$\mathbb{N}=\mathbb{Z}$ is undecidable in Lean. This is why you should do what Patrick suggests, and make an equality of sets.

[Victor Porton]

@Kevin Buzzard Even with open quotient? (It implies extensionality.) If extensionality is not enough, what else axiom to add?

[Victor Porton]

Kevin Buzzard said:

$\mathbb{N}=\mathbb{Z}$ is undecidable in Lean. This is why you should do what Patrick suggests, and make an equality of sets.

With sets the theorem statement even does not compile: { y: {x:α | c x} | d y } isn't a well-formed expression.

[Kevin Buzzard]

Did you look at what Patrick wrote? This is the way to do what you want to do in type theory. https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Subsets/near/277477240

[Victor Porton]

Yeah,

example {α β γ : Type} (c d : α → Prop) :
  ∀ (x : α), (d x → c x) → {x | c x ∧ d x} = {y ∈ {x : α | c x} | d y} :=
by super

does work.

[Victor Porton]

But it makes me a sad feeling that it does not work for types. I even cannot axiomatize extensionality for types, the following doesn't work:

axiom typeext {α β: Type} : ∀x,(α x ↔ β x) → α = β

Is there a way to work around of this?

[Kevin Buzzard]

Victor Porton said:

Kevin Buzzard Even with open quotient? (It implies extensionality.) If extensionality is not enough, what else axiom to add?

Extensionality of types is a meaningless concept. This is a big difference between type theory and set theory. You can't even state extensionality of types in type theory. If you're trying to prove equality of types, you're doing it wrong.

[Kyle Miller]

Victor Porton said:

Even with open quotient?

All this does is take what's in the quotient namespace and make it so you can reference it without the quotient. out front, for example it lets you write lift instead of quotient.lift. Maybe you've been let do believe open classical tells Lean to use classical logic? Even then, what that does is make it so you can write, for example, em instead of classical.em.

[Kyle Miller]

Victor Porton said:

Why doesn't

theorem subsubset {α β γ: Type} (c: α → Prop) (d: α → Prop) : --[decidable_pred c]
 ∀x,(d x → c x) → { x: α // c x ∧ d x } = { y: {x:α // c x} // d y }
 sorry;

compile? (Lean 3)

Maybe you'd reconsider thinking that this should compile if you consider that if z : { x: α // c x ∧ d x } then you can refer to z.val, z.property.left, and z.property.right for the components, but if z : { y: {x:α // c x} // d y } then you can refer to z.val.val, z.val.property, and z.property for corresponding components. This leads me to think that this pair of types fails whatever we might think "type extensionality" might mean.

You can write what we call an equivalence between these two types (docs#equiv), which is a pair of functions that are left and right inverses of each other, in case that's what you're looking for.