Questions about Lean's type theory

Stream: new members

[Emilie Uthaiwat]

Hello,

I am trying to understand Lean's type theory and have 2 small questions.

1) Statements which begin with a universal quantifier are an example of dependent function types. Are there other examples of dependent function types which are not statements of this kind?

2) From what I have understood, the mathematical equality corresponds to the definitional equality in Lean and "Eq" just gives us the symbol "=" needed to write statements (because its unique constructor only allows use to prove the statement "a = a"). Am I misunderstanding?

[Kevin Buzzard]

Mathematical equality is = but = is not definitional equality -- definitional equality is when the proof is rfl and this is essentially never true for equalities in advanced mathematics.

[Henrik Böving]

1) Statements which begin with a universal quantifier are an example of dependent function types. Are there other examples of dependent function types which are not statements of this kind?

Generally speaking all functions that take some value which appears later on in the the type are dependent functions. To take a more programmingy example: docs#Array.get takes an (a : Array α) and then later a value that depends on a: (i : Fin (Array.size a))

2) From what I have understood, the mathematical equality corresponds to the definitional equality in Lean and "Eq" just gives us the symbol "=" needed to write statements (because its unique constructor only allows use to prove the statement "a = a"). Am I misunderstanding?

If you can prove something by just using docs#Eq.refl it is definitionally equal yes, but usually there are a lot more things involved to get you to the point where you can use Eq.refl. If you want a precise definition of definitional equality and the whole type theory stuff check out Mario's thesis: #leantt

[Mario Carneiro]

For a simple example of something that is true but not "true by definition": 1 + n = n + 1 is not true by rfl even though you can prove it by induction on n

[Eric Rodriguez]

I was wondering the other day - is there a way to make it so, somehow? Obviously nothing resembling our current definition...

[Mario Carneiro]

there is only one case I know of where you get an identity as a "surprising defeq", namely (f ∘ g) ∘ h = f ∘ (g ∘ h). However I don't know how to turn this example into one that is definitionally commutative instead of associative

[Emilie Uthaiwat]

Thank you for your answers! So, rfl uses the reduction rules of the lambda calculus. Is this right?

[Emilie Uthaiwat]

Alright, thank you!