Zulip Chat Archive

Stream: general

Topic: K-like inductives don't take arguments

Mario Carneiro (Mar 26 2018 at 00:21):

@Gabriel Ebner I just discovered by reading the source code that lean doesn't consider an inductive suitable for K-like reduction unless it has 0 arguments in the constructor, rather than having all arguments in the output type like I thought (and wrote in my paper). Do you know why this is?

inductive  eq' {α} : α → α →  Prop
| refl : ∀ a, eq' a a
variables {α : Sort*} {C : α → α → Sort*}
(e : ∀ (a : α), C a a) (a : α) (h : eq' a a)
#reduce  @eq'.rec α C e a a h --expected: e a

Gabriel Ebner (Mar 26 2018 at 06:36):

The purpose of K-like reduction is that eq and heq reduce better. And "single constructor with no arguments" is the easiest criterion for that. IIRC, the code even constructs an explicit eq.refl/heq.refl/etc. term and checks whether it is def-eq with the major premise during reduction.

Last updated: Dec 20 2023 at 11:08 UTC