Transport along identity

Stream: new members

[Rémi Bottinelli]

Hey! Short question: In MLTT, you can pretty much by definition get a map A -> B from equality A = B. Am I right that this is not possible in lean due to eq living in Prop ? Is there an analogous non propositional identity allowing for such transport?

[Rémi Bottinelli]

Also, how much sense does it make to interpret inductive types defined as living in Prop to be "propositionally truncated" (in the HoTT sense): You first assume your newly defined inductive type to live in whichever large enough universe it would fit, and then take the propositional truncation, which means that (1) your type is now a Prop; and (2) the only way to get _out_ of this type is by mapping to a Prop.

[David Wärn]

You do get A -> B from A = B, see docs#cast. Essentially, eq is an inductive type family with a fully general elimination rule . And also, separately from this, it is a proposition. You're right that for general inductive types, like nat, it wouldn't make sense to both make it a proposition and allow elimination into non-propositions. But it makes sense for some inductive types, including eq. I believe the technical term is "syntactic subsingleton".

[Mario Carneiro]

It is called "large elimination" or "subsingleton elimination" in #leantt . Certain propositional inductive types have a recursor targeting all universes, if they meet a syntactic criterion for being a subsingleton

[Mario Carneiro]

important examples of this are docs#false, docs#and, docs#eq, and docs#acc

[Mario Carneiro]

Rémi Bottinelli said:

Also, how much sense does it make to interpret inductive types defined as living in Prop to be "propositionally truncated" (in the HoTT sense): You first assume your newly defined inductive type to live in whichever large enough universe it would fit, and then take the propositional truncation, which means that (1) your type is now a Prop; and (2) the only way to get _out_ of this type is by mapping to a Prop.

This "squash" elaboration of inductive types is explicitly worked out in the "reduction to W-types" chapter of #leantt . The short answer is: except for large eliminating types, this is a correct model for how the inductives work. The "squash to Prop" operator in lean is docs#nonempty . For large eliminating types, you need a separate encoding which writes them in terms of eq and acc to preserve the large eliminating behavior

[Rémi Bottinelli]

Thanks! #leantt is quite a bit more technical than what I can easily digest, but I think i'm slowly getting the gist of it. If I'm not mistaken, inductive families as used in lean were introduced by Dybjer first; is this "subsingleton elimination" thing a "patch" added later on or did he introduce it at the same time?

[Rémi Bottinelli]

Two more questions if I may:
1) Taking this view of "Propositional inductive types as propositionally truncated": can I expand the analogy to say that "subsingleton elimination" should be interpreted as the inductive type _already_ being a proposition? It at least makes sense intuitively for and and eq, since I think lean has UIP and and preserves the property of being a proposition/subsingleton.
2) Am I correct that any inductive (indexed?) type (family?) can be encoded in terms of W types + equality? It seems to be the case from your paper, but you also mention acc, which I don't exactly understand.

[Nathaniel Yazdani]

I think that (1) is true, but I'm honestly not sure where/when subsingleton elimination was introduced.

As for (2), Dybjer's original work actually presented two equivalent schema for inductive type families: the nowadays standard form ("generalized inductive type families") where each constructor _computes_ its type indices from arguments and an alternative form ("restricted inductive type families") where each constructor _constrains_ its type indices with equality arguments. As a caveat, W-types aren't _quite_ enough to get the proof theory of inductive type families, unless you have functional extensionality.

[Rémi Bottinelli]

Would you happen to know of a resource explaining/comparing the two approaches (and this W-type not being enough problem)?

[Nathaniel Yazdani]

The only comparison that I can recommend is the introduction of this paper from Dybjer, although the rest of the paper is in the more complicated context of inductive-recursive definitions rather than just inductive definitions, i.e., inductive type families. (Btw, this paper was probably what I was remembering in my previous comment; now i'm unsure whether there is a single Dybjer paper that presents inductive type families with both "computed indices" and "constrained indices.")

As for W-types, this other Dybjer paper gives a rather concise explanation of why W-types cannot perfectly encode inductive types (as the root problem is the same for inductive type families).

[Nathaniel Yazdani]

oh, this blog post by Conor McBride is an even better explanation of how W-types and equality relate in dependent type theory!

[Mario Carneiro]

There is also a chapter on reduction to W-types in my thesis #leantt . The short answer is that you can use plain W-types as long as you have eta for structures or the restricted version, eta for pairs and ulift. (Without this, you can get by with indexed W-types.) Also large eliminating props need a different encoding using acc, which is in some sense the equivalent of W for props.

[Mario Carneiro]

Rémi Bottinelli said:

If I'm not mistaken, inductive families as used in lean were introduced by Dybjer first; is this "subsingleton elimination" thing a "patch" added later on or did he introduce it at the same time?

I'm also not sure who introduced subsingleton elimination or its reasonable-but-complex rules for validity. It's not in the Dybjer papers that lean cites, and deals essentially with the interaction between inductive types and the impredicative and proof-irrelevant Prop universe, which as I understand it was introduced to address some perceived deficiencies in the Coq model (which were later also added to Coq in the form of the SProp universe). Perhaps @Jeremy Avigad might know?

[Rémi Bottinelli]

Sorry for hijacking this thread, but I'm trying to understand ite, and this is close enough to be related I guess… In the code:

theorem dif_pos {c : Prop} [h : decidable c] (hc : c)
  {α : Sort*} {t : c → α} {e : ¬c → α} : dite c t e = t hc :=
match h with
| (is_true hc)   := rfl
| (is_false hnc) := absurd hc hnc
end

is it true that we can make use of rfl because c is a Prop, hence a subsingleton? As I see it, if c was a type with more than one element, it wouldn't necessary be the case that the hc of is_true hc is the same as the hc given as a parameter, hence the resulting then branch would maybe result in something different. Am I mistaken?

[Mario Carneiro]

That's correct. The hc in the match is only defeq to the hc passed to the theorem because of proof irrelevance

[Rémi Bottinelli]

Ah, #leantt, last rule of p. 6! Prop is "judgementally a subsingleton"

[Rémi Bottinelli]

Thanks a lot, it's nice when things seem to get into place :)

[Mario Carneiro]

also illustrated by src#proof_irrel

[Rémi Bottinelli]

I'm looking at the proof that left inverses behave well assuming choice and all (last part of #tpil) and the combination of it all seems quite magic.

[Mario Carneiro]

lowercase: #tpil

[Rémi Bottinelli]

(deleted)

[Rémi Bottinelli]

(deleted)

[Jeremy Avigad]

Perhaps Jeremy Avigad might know?

I am afraid I don't. When I first learned Coq in 2009, Russell O'Connor told me about singleton elimination, and explained how using it with a well-founded predicate can be used to do a search for a natural number satisfying a decidable predicate. Google turned up this: https://coq.inria.fr/library/Coq.Logic.ConstructiveEpsilon.html.

But as as already been noted, subsingleton elimination is implicitly used to justify the elimination rule for equality. The rules for equality types, in the predicate setting, go back to Martin-Löf's formulations of type theory in the 1970s (https://ncatlab.org/nlab/show/identity+type). I don't really know the history of how equality type was first formulated as an inductive type in the impredicative setting and linked to subsingleton elimination. This 1989 paper by Pfenning and Paulin-Mohring describes equality as an inductive type, but I don't see any elimination rules: https://www.cs.cmu.edu/~fp/papers/mfps89.pdf. This paper by Coquand and Paulin-Mohring from around the same time mentions the need to restrict elimination from Prop, but I don't see any mention of equality or subsingleton elimination: http://david.darais.com/assets/Inductively_Defined_Types--Coquand+Paulin.pdf. Section 3.3 of the 1993 paper give the inductive characterizations of Acc and Eq, it it seems that they only eliminate to Prop: https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.32.5387&rep=rep1&type=pdf,

There is a lot of history here: https://coq.inria.fr/refman/history.html. (Search in "inductive" "Paulin" "equality" etc.). There is the following note regarding version 7.3, which was released in the early 2000s:

"Changes in the allowed elimination sorts for certain class of inductive definitions : an inductive definition without constructors of Sort Prop can be eliminated on sorts Set and Type A "singleton" inductive definition (one constructor with arguments in the sort Prop like conjunction of two propositions or equality) can be eliminated directly on sort Type (In V7.2, only the sorts Prop and Set were allowed)."

This might be what we are looking for: one of the first documented instances of using a subsingleton argument to justify elimination from Prop to Type.

[Rémi Bottinelli]

Another thing: In the sources, I see

lemma cast_eq {α : Sort u} (h : α = α) (a : α) : cast h a = a := rfl

which I understand to be true since h is defeq to eq.refl α, so that casting "along h" is defeq equal to casting "along eq.refl α", which I want to be equal to the identity. But why exactly is that last claim true? In my "HoTT book understanding", transport is defined using J and the base case is exactly what we need. But here I'm not sure.

[Anne Baanen]

Lean has proof-irrelevance: since eq is a Prop, every proof of equality is automatically defeq to rfl.

[Rémi Bottinelli]

But that only covers the fact that h is defeq to rfl, doesn't it? I still have to provide a term of the form cast h a = a.

[Kevin Buzzard]

In lean if P : Prop and h1 : P and h2 : P then h1 = h2 and the proof is rfl. This is very much not like HoTT.

[Eric Wieser]

cast h a unfolds to eq.rec h a or similar, which as you remark is the same as eq.rec rfl a; and recursors unfold definitionally on constructors

[Rémi Bottinelli]

Ah, I see what I got wrong: The equality type is "based" in lean, contrary to, say agda (or at least the one I know of), which I didn't take into account.

[Rémi Bottinelli]

I think the term is "indexed" rather than "based". In any case, is eq implemented this way to allow subsingleton elimination, or am I off-base here?

[Mario Carneiro]

The "based" formulation of eq seems strictly better than the other version, I don't see any downside to it. I assume you are asking why it is defined as

inductive eq {α} (a : α) : α → Prop
| refl : eq a

rather than

inductive eq' {α} : α → α → Prop
| refl (a) : eq' a a

[Mario Carneiro]

This makes a difference in the recursors:

#print eq.rec
-- protected eliminator eq.rec : Π {α : Sort u} {a : α} {motive : α → Sort l},
--   motive a → Π {x : α}, a = x → motive x

#print eq'.rec
-- protected eliminator eq'.rec : Π {α : Sort u_1} {motive : α → α → Sort l},
--   (Π (a : α), motive a a) → Π {x y : α}, eq' x y → motive x y

[Mario Carneiro]

In order to use the second one, you need both sides of the equality to be variables; in the first one only the RHS has to be a variable

[Mario Carneiro]

You can prove them equivalent, of course, but the first one is easier to use directly

[Rémi Bottinelli]

So, nothing to do with subsingleton elimination?

[Mario Carneiro]

they are both subsingleton eliminators, which you can tell above by noting that both versions live in Prop and yet have a motive that targets Sort l

[Rémi Bottinelli]

Also, since you're here:

1. Why is eq defined with | refl [] : eq a; why the [] ?
2. Defining a type eq2 which is exactly the same as eq and then
   def tr {α : Sort*} {P : α → Sort*} {a b : α} (p : Eq2 a b) (x : P a) : P b := @eq2.rec α a P x b p
   , I get an error: 
   ``failed to generate bytecode for 'tr' code generation failed, inductive predicate 'eq2' is not supported
   Does that mean eq has some built-in stuff to it?

[Mario Carneiro]

1. Compare with and without []:

universe u
inductive eq' {α : Sort u} (a : α) : α → Prop
| refl : eq' a

#print eq.refl
-- constructor eq.refl : ∀ {α : Sort u} (a : α), a = a
#print eq'.refl
-- constructor eq'.refl : ∀ {α : Sort u} {a : α}, eq' a a

[Mario Carneiro]

refl with an implicit a argument is also useful, we call it rfl, but for historical reasons that's not the constructor

[Mario Carneiro]

Note that [] used to be the default and {} was not; the default got switched at one point and so eq.refl got a [] to avoid breakage

[Rémi Bottinelli]

Hum, the only difference I see is eq' a a vs a = a, which I take to be pretty printing. Am I missing something?

[Mario Carneiro]

the braces around a

[Rémi Bottinelli]

ah, right, sorry!

[Mario Carneiro]

2. Yes, inductive predicates could be supported but almost all large eliminating props are written in terms of eq and acc in practice, so the current implementation skimps out and just implements code generation manually on these two types

[Mario Carneiro]

there are three other large eliminating predicates in lean: true, false, and and. true.rec is totally useless and never used, false.rec is deliberately unimplemented since it's impossible to call, and and.rec... not sure

[Mario Carneiro]

looks like and.rec works too

[Rémi Bottinelli]

Actually,

  inductive eq {α : Sort u} (a : α) : α → Prop
  | refl [] : eq a

is trippy to read, since the eq a in the second line really is more like eq a a.

[Rémi Bottinelli]

Iirc, that's because the index is not needed in the constructors.

[Mario Carneiro]

Lean 4 addresses this by making the parameters required to write but must be the same as the inputs

[Rémi Bottinelli]

@Mario Carneiro Thanks a lot for the patient explanations :)

[Julian Berman]

Does the "large" in "large eliminating" mean into Sort u vs Type?

[Rémi Bottinelli]

I think Sort u vs Prop, rather.