Zulip Chat Archive

Stream: Is there code for X?

Topic: trunc


view this post on Zulip Scott Morrison (Jun 02 2020 at 03:27):

Is

import data.quot

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

definable?

view this post on Zulip Scott Morrison (Jun 02 2020 at 03:27):

(computably)

view this post on Zulip Mario Carneiro (Jun 02 2020 at 03:43):

Nope

view this post on Zulip Mario Carneiro (Jun 02 2020 at 03:44):

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

view this post on Zulip Simon Hudon (Jun 02 2020 at 03:45):

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)

view this post on Zulip Mario Carneiro (Jun 02 2020 at 03:46):

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

view this post on Zulip Simon Hudon (Jun 02 2020 at 03:49):

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

view this post on Zulip Mario Carneiro (Jun 02 2020 at 03:51):

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

view this post on Zulip Mario Carneiro (Jun 02 2020 at 04:00):

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

view this post on Zulip Scott Morrison (Jun 02 2020 at 04:03):

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.

view this post on Zulip Mario Carneiro (Jun 02 2020 at 04:07):

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

view this post on Zulip Mario Carneiro (Jun 02 2020 at 04:43):

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

view this post on Zulip Scott Morrison (Jun 02 2020 at 05:34):

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.

view this post on Zulip Mario Carneiro (Jun 02 2020 at 06:22):

That could be a subtype instead of a Sigma'


Last updated: May 16 2021 at 05:21 UTC