Lift inductive Prop to Type

Stream: general

[Patrick Johnson]

Given an inductive Prop, is it possible, in general, to define an inductive Type (or higher) that precisely corresponds to the prop, and there exists a conversion function? Consider this simplified example:

inductive T : ℕ → Prop
| zero : T 0
| one : T 1
| add {a b : ℕ} : T a → T b → T (a + b)

inductive T₁ : ℕ → Type
| zero : T₁ 0
| one : T₁ 1
| add {a b : ℕ} : T₁ a → T₁ b → T₁ (a + b)

def T₁_of_T {n : ℕ} : T n → T₁ n := sorry

Because of proof irrelevance, there may be multiple ways to construct T₁ n, so T₁_of_T is allowed to use the axiom of choice. Can we construct it in general and what is the easiest way to do so?

I'm asking because I'm trying to prove that if there exists a refl_trans_gen R between two terms, then there exists a quiver path between them. The definition of quiver.path is more-or-less the same as refl_trans_gen, except that a path is a type.

[Reid Barton]

I would define a map the other way, prove it is surjective (by induction) and use choice to pick a section.

[Gabriel Ebner]

You can also show T n → nonempty (T₁ n) using induction.

[Reid Barton]

Oh yeah, to clarify, by "induction" I meant T.rec.

[Patrick Johnson]

I would define a map the other way, prove it is surjective (by induction) and use choice to pick a section.

Nice!
That works:

def T₁T {n : ℕ} (x : T₁ n) : T n :=
begin
  induction x with a b x y h₁ h₂,
  { exact T.zero },
  { exact T.one },
  { exact T.add h₁ h₂ },
end

lemma surj_T₁T {n : ℕ} : function.surjective (@T₁T n) :=
begin
  rintro h,
  induction h with a b h₁ h₂ h₃ h₄,
  { use T₁.zero },
  { use T₁.one },
  { use T₁.add h₃.some h₄.some },
end

def TT₁ {n : ℕ} : T n → T₁ n :=
function.surj_inv (@surj_T₁T n)

[Eric Rodriguez]

to illustrate the other approach:

def TT₁ {n : ℕ} : T n → nonempty (T₁ n) :=
begin
  apply T.rec,
  iterate 4 {constructor},
  rintro a b - - ⟨ha⟩ ⟨hb⟩,
  use ha.add hb
end

I think the surjection one is a bit more elegant thoughg

[Patrick Johnson]

I see. So the trick is to use refine (_ : nonempty _).some, whenever we need to inductively construct data from a prop using choice.

[Patrick Johnson]

def TT₁ {n : ℕ} : T n → T₁ n :=
begin
  intro h,
  refine (_ : nonempty _).some,
  induction h with a b h₁ h₂ h₃ h₄,
  { use T₁.zero },
  { use T₁.one },
  { use T₁.add h₃.some h₄.some },
end

[Patrick Johnson]

Is it worth having this function in mathlib?

import tactic
import logic.function.basic
import logic.relation
import combinatorics.quiver

noncomputable theory

open function
open relation
open quiver

def quiver.path_of_refl_trans_gen {α : Type*}
  {R : α → α → Prop} {x y : α}
  (h : refl_trans_gen R x y) :
  @path α ⟨R⟩ x y :=
begin
  refine (_ : nonempty _).some,
  induction h with x₁ y₁ h₁ h₂ h₃,
  { use @path.nil α ⟨R⟩ x },
  { use @path.cons α ⟨R⟩ x x₁ y₁ h₃.some h₂ },
end

[Eric Rodriguez]

this trick can be useful in a variety of ways, for example it's what you need (well, using exists.some but same idea) for docs#algebra.adjoin_induction'