Zulip Chat Archive

Stream: new members

Topic: Type theory without non-trivial reflexivity proofs?

Chris M (Oct 16 2020 at 12:59):

In the Lean tutorial it says that nontrivial identities can be proved by reflexivity. An example is :

example : 2+3=5 := eq.refl _

My understanding of how the Lean type checker does this is that it kind of "computes 2 + 5 at compile time, and if it indeed computes to 5, accepts the proof".

So in a sense, we ca think of an equality proof as a kind of "compile-time computation" that gives you a token that allows you to "skip the computation at runtime" and just grab the precomputed result.

Are there type systems (other than Lean's) where this is explicit? I.e. where you have to actually do the "compile time computation" yourself, and can only use equational reflexivity for the trivial case?

Mario Carneiro (Oct 16 2020 at 15:47):

Yes, metamath computations work like this, HOL too

Mario Carneiro (Oct 16 2020 at 15:48):

In fact I think it is a feature unique to DTT

Mario Carneiro (Oct 16 2020 at 15:50):

See for example http://us.metamath.org/mpeuni/2p2e4.html and note that the proof is not "by refl" but rather by a couple of applications of associativity

Last updated: Dec 20 2023 at 11:08 UTC