Typechecking "modulo" specified equalities?

Stream: general

[Rish Vaishnav]

In the following code, to prove the theorem ex it seems necessary to define the auxiliary theorem ex_aux first:

inductive T : Nat → Type
| mk : (n : Nat) → T n

axiom a : Nat
axiom b : Nat
axiom hab : a = b
axiom P : Prop
axiom prf : T a → P

theorem ex_aux (prf : T a → P) (v : T b) : P := by
  rw [hab] at prf
  exact prf v

theorem ex (v : T b) : P := ex_aux prf v

I was wondering, does Lean have an option or tactic that takes a list of equalities (here hab) and henceforth simulates typechecking as if this equality was definitional (behind the scenes, injecting type casts using these equalities where necessary)? For example, the above might become something like:

inductive T : Nat → Type
| mk : (n : Nat) → T n

axiom a : Nat
axiom b : Nat
axiom hab : a = b
axiom P : Prop
axiom prf : T a → P

#register_eq [hab]

theorem ex (v : T b) : P := prf v -- elaborates to `prf (Eq.mpr (congrArg T hab) v)`

If not, do we have an idea of how useful such a functionality would be?

[Rish Vaishnav]

Well, of course I take it back that the auxiliary theorem is "necessary" because you can always manually cast things, but I imagine that is something that could be automated if Lean is aware of what equalities it needs to use

[Eric Wieser]

(Presumably this is just an over minimization, but note that you can prove ex with by cases v, i.e. your T type is always empty)

[Rish Vaishnav]

Oh right, thanks yeah I meant for T to represent an arbitrary inductive type family (just added a constructor to it)

[Floris van Doorn]

You don't need ex_aux first, this works: theorem ex (v : T b) : P := prf (hab ▸ v).

[Floris van Doorn]

This register_eq functionality would be useful, but it falls quite far outside the scope of Lean.
The most flexible version of this is extensional type theory, but in such a theory type checking is much more complicated (in particular, undecidable), which has many drawbacks. There are other proof assistants taking this approach.

[Rish Vaishnav]

I see. What I had in mind was a kind of "pseudo-extensionality", where Lean would make its best effort to automatically unify types (via casting) using the equalities that it has. I'm working on something along these lines (to replace definitional proof irrelevance with propositional proof irrelevance for the purpose of translation), so I wanted to see if anything similar exists that I can steal code/ideas from, though my impression now is that there isn't.

[Rish Vaishnav]

Floris van Doorn said:

You don't need ex_aux first, this works: theorem ex (v : T b) : P := prf (hab ▸ v).

Oh nice, I always forget about subst. Though I imagine in some more complex cases it may not be able to correctly infer the motive argument

[Rish Vaishnav]

Here is a more contrived example where subst doesn't cut it, I think:

axiom U : Nat → Type
axiom T : (n : Nat) → U n → Type

axiom a : Nat
axiom ua : U a
axiom b : Nat
axiom ub : U b
axiom hab : a = b
axiom huab : HEq ua ub -- would not need HEq if declared #register_eq [hab] above
axiom h : a = b
axiom P : Prop
axiom prf : T a ua → P

theorem ex_aux (a b : Nat) (hab : Eq a b) (ua : U a) (ub : U b)
  (huab : HEq ua ub) (prf : T a ua → P) (v : T b ub) : P := by
  subst hab
  subst huab
  exact prf v

theorem ex (v : T b ub) : P := ex_aux _ _ hab _ _ huab prf v

[Trebor Huang]

Can this be solved by a variant of the ETT to ITT translation? ETT allows all equality assumptions to be used as definitional equalities. There are several papers detailing how to translate an ETT term (whose type happens to be a valid ITT type) to an ITT term. If this (together with a partial typechecking algorithm for ETT) gets implemented as a tactic we can invoke it and reason as if some equalities became definitional.

[Floris van Doorn]

In more complicated examples you can still do it without additional lemmas, using @Kyle Miller's congruence generator (he reminded me of the existence yesterday). Then it can be this:

theorem ex (v : T b ub) : P := prf <| cast congr(T $hab $huab).symm v

[Rish Vaishnav]

Trebor Huang said:

Can this be solved by a variant of the ETT to ITT translation? ETT allows all equality assumptions to be used as definitional equalities. There are several papers detailing how to translate an ETT term (whose type happens to be a valid ITT type) to an ITT term. If this (together with a partial typechecking algorithm for ETT) gets implemented as a tactic we can invoke it and reason as if some equalities became definitional.

Interesting, I hadn't really conceptualized of my task as one of converting from ETT to ITT, but rather of making a generic framework for "cast injection" (where equalities can be derived from a number of different sources). Now that I think about it, the proof irrelevance axiom (axiom prfIrrel (P Q : Prop) (h : P = Q) (p : Q) (q : P) : HEq p q) can be considered just another one of the registered equalities that would be attempted when typechecking fails (with proof irrelevance disabled). So I suspect those authors may have run into similar issues, I'll have to read more into it.

I guess the "partial typechecking algorithm" you refer to would be the algorithm used to derive the necessary equalities from their more generic forms? I think that Lean's typeclass mechanisms could help here (e.g. in deriving the h argument to the prfIrrel axiom).