trunc

Stream: Is there code for X?

[Scott Morrison]

Is

import data.quot

def foo {α : Type*} {Z : α → Type*} (f : Π a, trunc (Z a)) : trunc (Π a, Z a) :=
sorry

definable?

[Scott Morrison]

(computably)

[Mario Carneiro]

Nope

[Mario Carneiro]

This comes up every once in a while. It has some reasonably obvious computational interpretation, but you can't prove it from lean's axioms

[Simon Hudon]

I think we could remove the noncomputable keyword by using a vm_override though. Am I wrong? (I haven't used them that way yet)

[Mario Carneiro]

This is also relevant for the QPF implementation that Jeremy, Simon and I worked on last year. I think @Gabriel Ebner told me that this makes the definitional equality problem much harder because you have to work under binders; I forget the details now. It might end up like cubical type theory reduction

[Simon Hudon]

To answer my own question: vm_override don't do that yet

[Mario Carneiro]

Oh, I also remembered a trick that @Chris Hughes pointed out:

def bar {α : Type*} : trunc (trunc α → α) := foo (@id (trunc α))

you can do some really funny things with this function, because the VM representation of this function does not respect equality

[Mario Carneiro]

Ah, here it is:

import data.quot

meta def foo {α : Type*} {Z : α → Type*} (f : Π a, trunc (Z a)) : trunc (Π a, Z a) :=
unchecked_cast f

meta def bar {α : Type*} : trunc (trunc α → α) := foo (@id (trunc α))

meta def lie : bool :=
(@bar bool).lift (λ f, to_bool (f (trunc.mk tt) = f (trunc.mk ff))) $ λ f g,
by simp [show trunc.mk tt = trunc.mk ff, from subsingleton.elim _ _]

meta example : lie = tt :=
show trunc.lift _ _ bar = _, begin
  generalize : bar = x,
  refine trunc.ind (λ x, _) x,
  apply to_bool_tt,
  rw show trunc.mk tt = trunc.mk ff, from subsingleton.elim _ _
end

#eval lie -- ff

[Scott Morrison]

Ok, to #xy the problem, what I really wanted was:

import data.fintype.basic

def equiv.sigma_quotient_fin_card
  {α : Type*} [fintype α] [decidable_eq α] (s : setoid α) [decidable_rel s.r]:
   trunc (α ≃ Σ (q : quotient s), fin (fintype.card {x // ⟦x⟧ = q})) :=

which I can construct using foo, but so far not otherwise.

[Mario Carneiro]

I think this can be proven. First you fix an ordering of the base type, then this induces an order on every equivalence class and you get the map to fin that way

[Mario Carneiro]

def equiv.sigma_quotient_fin_card
  {α : Type*} [fa : fintype α] [decidable_eq α] (s : setoid α) [decidable_rel s.r] :
  trunc (α ≃ Σ (q : quotient s), fin (fintype.card {x // ⟦x⟧ = q})) :=
begin
  resetI, rcases fa with ⟨⟨S, hS₁⟩, hS₂⟩,
  refine quotient.rec_on_subsingleton S (λ l h₁ h₂, trunc.mk _) hS₁ hS₂, clear hS₂ hS₁ S,
  exact (equiv.sigma_preimage_equiv quotient.mk).symm.trans (equiv.sigma_congr_right (λ q,
    fintype.equiv_fin_of_forall_mem_list
      (λ ⟨x, px⟩, list.mem_pmap.2 ⟨x, list.mem_filter.2 ⟨h₂ _, px⟩, rfl⟩)
      (list.nodup_pmap (λ a _ b _, congr_arg subtype.val) (list.nodup_filter _ h₁)))),
end

[Scott Morrison]

Excellent, thanks. I'll upgrade this to a trunc (Σ' e : α ≃ Σ (q : quotient s), fin (fintype.card {x // ⟦x⟧ = q}), ∀ x, (e x).1 = ⟦x⟧), recording the "fibre-wise" property, and eventually include it in a PR.

[Mario Carneiro]

That could be a subtype instead of a Sigma'