Is this provable? (Axiomatizing proof irrelevance)

Stream: general

[Rish Vaishnav]

To make Lean proofs more readily translatable to Dedukti (and eventually other proof assistants), I've been experimenting with using an axiom representing proof irrelevance to allow me to modify terms that implicitly make use of (definitional) proof irrelevance in their typing to instead do so explicitly via type casts (i.e. propositional proof irrelevance). My goal is to build the proofs needed for such casts recursively, in parallel to typechecking, and "inject" them where necessary. For example, here is what I (initially) envisioned this "patching" would look like:

axiom prfIrrel (P : Prop) (p q : P) : p = q

axiom P : Prop
axiom p : P
axiom q : P
axiom p' : P
axiom q' : P

inductive Test : P → P → Type
| mk : (p q : P) → Test p q

theorem PatchTest : Test q q' := Test.mk p p'

theorem PatchTest' : Test q q' :=
  @Eq.mpr (Test q q') (Test p p')
  (congr (f₁ := fun x => Test q x) (f₂ := fun x => Test p x)
    (congr (f₁ := fun x => Test x) (f₂ := fun x => Test x) rfl (prfIrrel P q p))
    (prfIrrel P q' p'))
  (Test.mk p p')

I was quite happy with this approach, until I encountered a somewhat worrysome edge case. It looks like Lean allows for propositions to be indexed by proofs (analogously to how types can be indexed by type instances), which seems to make it difficult to patch examples like the following:

axiom P : Type
axiom irrel (p q : P) : p = q
axiom p : P
axiom q : P

axiom Q : P → Type
axiom Qp : Q p
axiom Qq : Q q

axiom Test : (p : P) → (Q p) → Type

theorem ex (t : Test q Qq) : Test p Qp := sorry -- replacing `Type` with `Prop` above, `t` suffices

(of course, I will eventually be using Prop instead of Type). I could not manage to prove this with existing theorems (though I may be missing something obvious). I was eventually able to do so, but only by adding an axiom for congruence for HEq, and an extra HEq irrelevance axiom:

axiom irrelHEq (P Q : Type) (heq : P = Q) (p : P) (q : Q) : HEq p q

axiom congr'.{u, v}
  {α₁ α₂: Sort u}
  {β₁ : α₁ → Sort v} {β₂ : α₂ → Sort v}
  {f₁ : (a : α₁) → β₁ a} {f₂ : (a : α₂) → β₂ a}
  {a₁ : α₁} {a₂ : α₂}
  (h₁ : HEq f₁ f₂) (h₂ : HEq a₁ a₂)
  : HEq (f₁ a₁) (f₂ a₂)

theorem ex' (t : Test q Qq) : Test p Qp :=
  @Eq.mpr (Test p Qp) (Test q Qq)
  (eq_of_heq (congr' (f₁ := fun x => Test p x) (f₂ := fun x => Test q x)
    (congr' (f₁ := fun x => Test x) (f₂ := fun x => Test x) HEq.rfl $ heq_of_eq (irrel p q))
    (irrelHEq (Q p) (Q q) (congrArg Q $ irrel p q) Qp Qq)))
  t

Looking at the HEq docs, however, it seems like such a congruence theorem cannot be proven. So, my questions are:

1. Is the theorem ex above provable?
2. If not, would it be problematic to add the congr' axiom above? I imagine doing so might lead to inconsistency somehow (I need to analyze this more thoroughly myself, but if someone already knows...)
3. Is this case of proof-indexed propositions even worth considering? Again, this is something I will probably investigate myself by modifying the typechecker to disallow such a case and seeing if mathlib still typechecks, but just wondering if someone already has an idea.

[Yaël Dillies]

What do you mean by "ex being provable"? It is data, hence it cannot be proved, but it certainly can be constructed, eg def ex (t : Test q Qq) : Test p Qp := fun _ _ ↦ Unit

[Yaël Dillies]

congr' is independent of Lean's logic, so it is not inconsistent to add it

[Rish Vaishnav]

Yaël Dillies said:

What do you mean by "ex being provable"? It is data, hence it cannot be proved, but it certainly can be constructed, eg def ex (t : Test q Qq) : Test p Qp := fun _ _ ↦ Unit

Right, I guess having changed Prop to Type I should have said "inhabited". I'm not sure I follow your construction though, it looks like you gave an instance of the type of Test rather than of Test p Qp?

[Yaël Dillies]

Oh sorry, I completely misread Test

[Yaël Dillies]

import Mathlib.Tactic.SimpRw

axiom P : Type
axiom irrel (p q : P) : p = q
axiom p : P
axiom q : P

axiom Q : P → Prop -- `ex` is not true if `Q : P → Type`
axiom Qp : Q p
axiom Qq : Q q

axiom Test : (p : P) → (Q p) → Prop

-- I need this because I can only substitute variables, not axioms
theorem ex_aux (p q : P) (Qp : Q p) (Qq : Q q) (t : Test q Qq) : Test p Qp := by
  obtain rfl := irrel p q
  exact t

theorem ex (t : Test q Qq) : Test p Qp := ex_aux _ _ _ _ t

[Kyle Miller]

Just so you know, if you specialize congr' to have Prop as the codomain, it's a theorem:

theorem congr'_prop.{u}
    {α₁ α₂: Sort u}
    {β₁ : α₁ → Prop} {β₂ : α₂ → Prop}
    {f₁ : (a : α₁) → β₁ a} {f₂ : (a : α₂) → β₂ a}
    {a₁ : α₁} {a₂ : α₂}
    (h₁ : HEq f₁ f₂) (h₂ : HEq a₁ a₂)
    : HEq (f₁ a₁) (f₂ a₂) := by
  cases h₂
  exact proof_irrel_heq (f₁ a₁) (f₂ a₁)

[Kyle Miller]

irrelHEq is inconsistent:

axiom irrelHEq (P Q : Type) (heq : P = Q) (p : P) (q : Q) : HEq p q

example : False := by
  have := irrelHEq Bool Bool rfl true false
  simp at this

[Kyle Miller]

The Prop version is fine, and it's the theorem docs#proof_irrel_heq

[Kyle Miller]

It turns out you can omit h1 and h2 from congr'_prop:

theorem congr'_prop.{u}
    {α₁ α₂: Sort u}
    {β₁ : α₁ → Prop} {β₂ : α₂ → Prop}
    {f₁ : (a : α₁) → β₁ a} {f₂ : (a : α₂) → β₂ a}
    {a₁ : α₁} {a₂ : α₂}
    : HEq (f₁ a₁) (f₂ a₂) := by
  congr! -- this ends up being `exact proof_irrel_heq (f₁ a₁) (f₂ a₂)`

[Rish Vaishnav]

Thanks a lot! Though unfortunately both ex_aux and congr'_propneed proof irrelevance in order to type, so I can't (directly) translate them a system where proof irrelevance doesn't exist. This is why I kept things in Type rather than Prop (so that you could try to prove this without having to do any kernel modifications; perhaps I should have been more clear about that).

However, since congr' is a theorem if I make the fs end in Prop, that tells me that it should be okay for me to add that as an axiom in my translation without risking inconsistency. So I think I'll roll with that for now. Thanks again!

[Rish Vaishnav]

Oh, and actually I think congr'_prop is typable without proof irrelevance using the simpler patching approach I mentioned initially (using just normal congr and prfIrrel), so I think it doesn't even have to be an axiom after all!

[Rish Vaishnav]

Ah yes, and the same could apply to Yael's ex_aux, I suppose. That auxilliary theorem with abstracted variables strategy gives me an idea for how to potentially simplify the patching and perhaps avoid HEq entirely...

[Rish Vaishnav]

Alright! Taking inspiration from Yael's proof, I was able to prove the original statement (sorry, I forgot to include the proposition argument to irrel) without using HEq:

axiom P : Type
axiom irrel (P : Type) (p q : P) : p = q
axiom p : P
axiom q : P

axiom Q : P → Type
axiom Qp : Q p
axiom Qq : Q q

axiom Test : (p : P) → (Q p) → Type

theorem ex (t : Test q Qq) : Test p Qp :=
  @Eq.mpr (Test p Qp) (Test q Qq)
  (@Eq.ndrec P p (fun q => ∀ (Qq : Q q), Test p Qp = Test q Qq) (fun Qq =>
    @Eq.ndrec (Q p) Qp (fun Qq => Test p Qp = Test p Qq) rfl Qq (irrel (Q p) Qp Qq)
  ) q (irrel P p q) Qq) t

So, it seems like my handling of the application case of definitional equality will require building the proof linearly (in the left-to-right order of the arguments) rather than recursively so that I can handle any dependent propositions. A bit more complex, but should be doable I think. Thanks again!

[Matt Diamond]

irrel seems problematic though, as you can use it to prove False:

axiom irrel (P : Type) (p q : P) : p = q

example : False := by simpa using irrel Bool true false

[Matt Diamond]

this is basically what Kyle pointed out earlier

[Matt Diamond]

irrel is an axiom that says "all types are subsingletons", which is clearly not true

[Rish Vaishnav]

Yeah, the final version will have P in Prop, that was just for demo purposes (I’ll be typechecking the patched terms with proof irrelevance disabled)

[Rish Vaishnav]

Though I do see how the inconsistency could be problematic in allowing me to prove things I shouldn’t — I didn’t make use of this inconsistency in my proof above, but if I want to be sure I could instead replace it with a few axioms specializing it to each of the “propositions” (here, types) that I use it with.