Subject reduction failure, applications?

Stream: Type theory

[Kyle Miller]

I've heard through the years about quotient types breaking subject reduction, and how it's a problem for theory.

Something I've never heard though is whether there are applications of subject reduction failure. Is it something that can be taken advantage of in some way?

For example, perhaps it can be wielded to make a term that relieves some dependence issues, for example a term that has type Fin (n + m) in one context but Fin (m + n) in another.

(Out of scope for this discussion: whether this is a good idea or not. The question is motivated out of a hacker spirit to see what's possible :slight_smile:)

[Parth Shastri]

In #leantt there are two notions of definitional equality, the ideal one and the algorithmic one. The ideal definitional equality satisfies subject reduction, while the algorithmic one fails due to a lack of transitivity caused by subsingleton elimination. If I'm not mistaken, the ideal definitional equality is the transitive closure of the algorithmic definitional equality, so I think there cannot be an application of the subject reduction failure in the way you describe.

[Parth Shastri]

Side note: The subject reduction failure (really the defeq transitivity failure) for quotient types is easily fixable (just bump the universe to max 1 u since quotients of Props are useless). The actual problem is with Acc, used in well-founded recursion, and it isn't just a problem for theory. This is the reason why well-founded definitions don't satisfy definitional equations. For example, Nat.log2 2 = 1 would be provable by rfl if not for the defeq transitivity failure:

unseal Nat.log2

example : Nat.log2 2 = 1 := rfl -- fails

noncomputable def f : Acc Nat.lt n → Nat :=
  Acc.rec fun n _ log2 => if _ : n ≥ 2 then log2 (n / 2) (by simp; omega) + 1 else 0

example : Nat.log2 2 = 1 := calc -- works
  Nat.log2 2 = f _                                       := rfl
  _          = f ⟨2, fun n _ => Nat.lt_wfRel.wf.apply n⟩ := rfl
  _          = 1                                         := rfl

[Aaron Liu]

What if you add axioms like Quot.sound

[Parth Shastri]

Axioms don't add new definitional equalities

[Aaron Liu]

I guess yeah

[Aaron Liu]

if you don't add any new definitional equalities you can't have more stuff be definitionally equal

[Jason Rute]

You might be interested in this PA.SX answer (by me) on the subject including lots of links back to Zulip. https://proofassistants.stackexchange.com/a/1194