Zulip Chat Archive

Stream: new members

Topic: Type theory without non-trivial reflexivity proofs?


view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Oct 16 2020 at 15:47):

Yes, metamath computations work like this, HOL too

view this post on Zulip Mario Carneiro (Oct 16 2020 at 15:48):

In fact I think it is a feature unique to DTT

view this post on Zulip 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: May 10 2021 at 23:11 UTC