Notation for instance of dependent type?

Stream: new members

[Mr Proof]

Something I'm a bit confused about:

If we had a type A × B we can make instances (a,b), (a',b') etc of that type
If we had a dependent type ∃(x:A),B(x) then this represents a dependent pair. But (a, b a), (a', b' a') aren't instances AFIK. They are instances of A × B a and A × B a' respectively I believe. And since things can't have two types. This leaves me two wonder if you had a pair which accidentally can also be written as an instance of dependent pair then what happens there?

The instances ∀(x:A),B(x) are functions using lambda notation, but I'm confused about if there is, in the same way, a notation for a dependent pair.

[Eric Wieser]

(just to note, I think you mean "term" not "instance", since the latter can be confused with instance)

[Eric Wieser]

Does

import Mathlib

def p : ℕ × ℕ := (1, 2)
def q : (n : ℕ) × Fin n := ⟨1, 2⟩

answer your question?

[Mr Proof]

Well I'm sort of wondering why this is wrong:

def A : ∃ x : Nat, x*x = 9:= ⟨3 , 3*3 = 9⟩

[Vincent Beffara]

Do you mean this?

def A : ∃ x : Nat, x*x = 9:= ⟨3 , rfl⟩

[Henrik Böving]

The proof of an existential statement is a witness x as well as a proof that the proposition holds for that witness. You are giving a witness x = 3 and the proposition for that specific witness, but not a proof. A proof in this case would be rfl

[Mr Proof]

I see. So the structure ⟨....⟩ can be used to fill in a dependent pair type. But there is no specialised notation to do this other than specifying the type with ∃? Unlike the forall type in which I believe you can define a function directly using the => notation.

[Kyle Miller]

Angle brackets are the generic notation for constructing one-constructor types, and parentheses are specialized just for Prod.

You are correct that there is no specialized notation for Exists.

[Eric Wieser]

Unlike the forall type in which I believe you can define a function directly using the => notation.

The forall type is very special, and is native to the type theory

[Eric Wieser]

docs#Prod and docs#Sigma and docs#Exists are not native, they're just inductive types

[Kyle Miller]

(They're native insofar as inductive types are native. I think there's a point of view that all inductive types that could ever be defined are already present, and the inductive command just names them.)

[Mr Proof]

Could you suggest a notation for a dependent pair? e.g. something like ⟨3◀ rfl⟩ It's strange if there is no notation for it. It should be interpreted "3 is an example of the proposition P(3) whose proof is rfl 3". I think it contains all the information to deduce it's type.

[Eric Wieser]

What's wrong with ⟨3, rfl⟩ notation?

[Eric Wieser]

(or ⟨_, Eq.refl 3⟩, if you want to provide only the second argument)

[Mark Fischer]

You can use the constructor directly:

def A : ∃x : ℕ, x * x = 9 := Exists.intro 3 rfl
def A := @Exists.intro ℕ (λx ↦ x * x = 9) 3 rfl

That's not really ergonomic or idiomatic, but it gets you at a different notation perhaps.

Here are some more examples: I'm not sure if this is helpful or not as this is not how you've see this in the wild, but here we are.

example : (n : ℕ) × Fin n :=  ⟨1, 2⟩
example                   := (⟨1, 2⟩ : (n : ℕ) × Fin n)
example : (n : ℕ) × Fin n :=  { fst := 1, snd := 2 }
example                   :=  { fst := 1, snd := 2 : (n : ℕ) × Fin n }
example                   := ({ fst := 1, snd := 2 } : (n : ℕ) × Fin n )
example : (n : ℕ) × Fin n := Sigma.mk 1 2
example                   := @Sigma.mk ℕ (Fin ·) 1 2

[Mark Fischer]

I'm surprised the following from above type checks.

def q : (n : ℕ) × Fin n := ⟨1, 2⟩

Okay, I'm not sure that's happening...

def Foo : Fin 1 := 20
#check Foo -- Fin 1
#eval Foo -- 0

[Kyle Miller]

(2 : Fin 1) is the same as (0 : Fin 1) since numeric literals wrap around for Fin.

[Mr Proof]

I made some notation just for fun:

import Mathlib
def DependentPair {B:A→Prop} : (x:A) → B x → ∃(y:A), B y := λ a b => ⟨a , b⟩

notation  a "◀" b  => DependentPair a b

def example1 := 3 ◀ rfl
def example2 := 1 ◀ Nat.one_eq_succ_zero
def example3 := 4 ◀ ((by simp):2+2=4)

But I can't think of any other examples of using it except to show that 3=3. :laughing:

Edit: Perhaps a better notation is to have the second argument a function (to abuse the naming):

def DependentPair {B:A→Prop} : (x:A) → ((z:A) → B z) → ∃(y:A), B y := λ a f => ⟨a , f a⟩

notation  a "◀" f  => DependentPair a f

def example1 := 3 ◀ Eq.refl

[Eric Wieser]

It's perhaps worth pointing out that ∃ is not usually called a "dependent pair"

[Eric Wieser]

That's docs#Sigma, not docs#Exists

[Eric Wieser]

Notably, you can't ask an Exists for its first element, so this is a very weird definition of "pair"

[Mark Fischer]

Eric Wieser said:

Notably, you can't ask an Exists for its first element

That's just constructive? I think that with the axiom of choice, you can get the element.

[Jon Eugster]

you can get some element, but you can't prove that the element you are getting from choice is exactly the one you used while constucting. what you can prove is docs#Exists.choose_spec

[Kyle Miller]

In fact, if there's a way to get that element from Exists.intro, then you can make use of proof irrelevance to prove a contradiction.

[Kyle Miller]

Here's an example setup of that: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.E2.9C.94.20Equivalence.20in.20Inductive.20Prop.20Families/near/436606381