Quot.lift for dependent products

Stream: lean4

[Tomas Skrivan]

I have a function (f : ((i : I) → X i) → Y) can it be lifted it to a function of type (f : ((i : I) → Quot (r i) (X i)) → Y) for some collection of relations (r : (i : I) → X i → X i → Prop)?

For I = Fin n one can probably define such lifting by induction. I have tried it but got lost in all those dependent types.

Does it hold for arbitrary I? If it does not hold for arbitrary I, is it okay just axiomatize it?

Here is my attempt, there is still one sorry to make it sound. However, I had to use implemented_by to keep it computable.

code

import Lean

unsafe def Quot.unquot {r : α → α → Prop} : Quot r → α :=
  cast lcProof -- Porting note: was `unchecked_cast` before, which unfolds to `cast undefined`

noncomputable def Quot.out {r : α → α → Prop} (q : Quot r) : α :=
  Classical.choose (Quot.exists_rep q)

unsafe def Quot.liftForallImpl {I : Sort u} {X : I → Sort v}
  {r : (i : I) → X i → X i → Prop}
  (f : ((i : I) → X i) → Y)
  (h : ∀ (xs xs' : (i : I) → X i), (∀ i, r i (xs i) (xs' i)) → f xs = f xs')
  (xs : (i : I) → Quot (r i)) : Y :=
  f (fun i => (xs i).unquot)

@[implemented_by Quot.liftForallImpl]
def Quot.liftForall {I : Sort u} {X : I → Sort v}
  {r : (i : I) → X i → X i → Prop}
  (f : ((i : I) → X i) → Y)
  (h : ∀ (xs xs' : (i : I) → X i), (∀ i, r i (xs i) (xs' i)) → f xs = f xs')
  (xs : (i : I) → Quot (r i)) : Y :=
  f (fun i => (xs i).out)

universe u v w

-- Is this true? Seems it should be true
theorem Quot.out_rel_self (r : X → X → Prop) (x : X) :
    r (Quot.mk r x).out x := by
  unfold Quot.out
  have h := Classical.choose_spec (Quot.exists_rep (mk r x))
  sorry -- can this

theorem Quot.liftFolallBeta {I : Sort u} {X : I → Sort v}
    {r : (i : I) → X i → X i → Prop} {Y : Sort w}
    (f : ((i : I) → X i) → Y)
    (h : ∀ (xs xs' : (i : I) → X i), (∀ i, r i (xs i) (xs' i)) → f xs = f xs')
    (xs : (i : I) → X i)
    : liftForall f h (fun i => Quot.mk (r i) (xs i)) = f xs := by
  apply h
  simp
  intro i; apply Quot.out_rel_self

[Tomas Skrivan]

Ahh the supporting theorem Quot.out_rel_self is not true as stated. I think it needs that r is an actual relation.

[Yuyang Zhao]

This has been discussed many times and a related PR is #5576.

[Tomas Skrivan]

Very nice, do you know if it works/is sound for types that are not finite?

[Yuyang Zhao]

See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Should.20we.20merge.20.60Quotient.2Eout.60.20and.20.60Quotient.2Eunquot.60.3F/near/390172207

[Tomas Skrivan]

Very interesting, it will take me some time to digest this. Thanks a lot for the links.

From the first look, I'm a bit confused why the argument there breaks for finite ι.

[Tomas Skrivan]

Ohh wait, your Quotient.choice is quite different from my Quot.liftForallso I do not see how it answers my question.

Sure I can implement Quot.liftForall using Quotient.choice' if it were sound. I don't think it works the other way around, so it is unclear to me if Quot.liftForall is unsound.

[Kyle Miller]

I think Quot.out_rel_self needs that r be an equivalence relation.

[Tomas Skrivan]

Yes I agree and I meant to write " I think it needs that r is an actual equivalence" previously.

[Kyle Miller]

theorem Quot.out_rel_self (r : X → X → Prop) (hr : Equivalence r) (x : X) :
    r (Quot.mk r x).out x := by
  unfold Quot.out
  have h := Classical.choose_spec (Quot.exists_rep (mk r x))
  exact Quotient.exact (s := {r, iseqv := hr}) h

[Kyle Miller]

@Tomas Skrivan I got @Mario Carneiro's example to work for your lifting function. The observation is that if you make Y be the quotient of the domain of f then you can implement Quotient.choice' and use of the soundness counterexample. Here's directly using docs#Squash:

import Mathlib.Data.Quot

universe u v w

unsafe def Quot.liftForallImpl {I : Sort u} {X : I → Sort v} {Y : Sort w}
  {r : (i : I) → X i → X i → Prop}
  (f : ((i : I) → X i) → Y)
  (h : ∀ (xs xs' : (i : I) → X i), (∀ i, r i (xs i) (xs' i)) → f xs = f xs')
  (xs : (i : I) → Quot (r i)) : Y :=
  f (fun i => (xs i).unquot)

@[implemented_by Quot.liftForallImpl]
def Quot.liftForall {I : Sort u} {X : I → Sort v} {Y : Sort w}
  {r : (i : I) → X i → X i → Prop}
  (f : ((i : I) → X i) → Y)
  (h : ∀ (xs xs' : (i : I) → X i), (∀ i, r i (xs i) (xs' i)) → f xs = f xs')
  (xs : (i : I) → Quot (r i)) : Y :=
  f (fun i => (xs i).out)

def bad (A : Type _) : Squash (Squash A → A) :=
  Quot.liftForall (I := Squash A) (X := fun _ => A) (r := fun _ _ _ => True)
    (Y := Squash (Squash A → A))
    (f := Quot.mk _)
    (xs := id)
    (h := by intros; apply Quot.sound; trivial)

#eval True
-- true

-- Override the instance used when evaluating `True`:
local instance exoticInstance : Decidable True :=
  Quot.recOnSubsingleton (bad Bool) fun f =>
    decidable_of_iff (f (Squash.mk true) = f (Squash.mk false)) <|
      iff_true_intro (congr_arg f (Quot.sound trivial))

#eval True
-- false

-- Also, type theory disagrees with the evaluator:
example : decide True = true  := .trans (by congr) decide_True

[Tomas Skrivan]

Thanks a lot but this is really really strange :)

I tried reproducing the counter example using mathlibs Quotient.finChoice and of course it failed

code

import Mathlib.Data.Fintype.Quotient

instance : Fintype (Squash Bool) where
  elems := {
      val := Quot.mk _ [Quot.mk _ false]
      nodup := by decide
    }
  complete := by
    intro x; simp
    have ⟨_,h⟩ := x.exists_rep
    rw[← h]
    apply Quot.sound; apply True.intro

instance : DecidableEq (Quotient (trueSetoid (α:=Bool))) := (by infer_instance : DecidableEq (Squash Bool))
instance : Fintype (Quotient (trueSetoid (α:=Bool))) := (by infer_instance : Fintype (Squash Bool))

def exoticInstance : Decidable True :=
  @Quot.recOnSubsingleton _ _ (fun _ => Decidable True) _
    (@Quotient.finChoice (@Quotient Bool trueSetoid) _ _ (fun _ => Bool) (fun _ => trueSetoid) id)
    (fun f => decidable_of_iff (f (Quot.mk _ false) = f (Quot.mk _ true))
      (iff_true_intro (congr_arg f (Quotient.sound trivial))))

example : @decide True exoticInstance = true  := .trans (by congr) decide_True

-- this fails now
example : @decide True exoticInstance = false := by native_decide

-- this is "isTrue" now
#eval exoticInstance

[Kyle Miller]

Here's code analogous to my previous one:

import Mathlib.Data.Fintype.Quotient

instance (A : Type _) [Fintype A] : Fintype (Squash A) :=
  Fintype.ofSurjective Squash.mk (by rintro ⟨x⟩; exact ⟨x, rfl⟩)

def notBadAux (A : Type _) [Fintype A] :=
  let _inst : Setoid A := trueSetoid
  Quotient.finChoice (ι := Squash A) (α := fun _ => A) (f := id)

def notBad (A : Type _) [Fintype A] : Squash (Squash A → A) :=
  Quot.recOnSubsingleton (notBadAux A) (Quot.mk _)

#eval True
-- true

local instance exoticInstance : Decidable True :=
  Quot.recOnSubsingleton (notBad Bool) fun f =>
    decidable_of_iff (f (Squash.mk true) = f (Squash.mk false)) <|
      iff_true_intro (congr_arg f (Quot.sound trivial))

-- Still true:
#eval True
-- true

(By the way, you can use inferInstanceAs <| DecidableEq (Squash Bool) rather than going into tactic mode.)

[Kyle Miller]

A proximal reason for this not giving a paradox is that it's not evaluating anything unsafe :-)

[Kyle Miller]

Reading the code for Quotient.finChoice (or trying to), I think that's the best you can say what the reason is.

The way it gets around needing to unsafely extract terms from quotients is that Quotient.finChoice is able to recursively apply Quotient.liftOn₂ for each term in the indexing set. (In particular, it makes an if/else chain for each representative of the index type, and the resulting function will use the DecidableEq instance to see that Squash.mk true = Squash.mk false.)

There doesn't seem to be a way to do simultaneous lifting of a family. Here it uses Fintype and DecidableEq to nondeterministically sequence the lifts. Presumably FinEnum would work too.

[Tomas Skrivan]

Now I'm wondering if marking Quot.liftForall as opaque and Quot.liftFolallBeta as axiom would also lead to issues.

[Kyle Miller]

I'm not sure if my intuition is right here, but it seems to me that the fundamental computational issue with Quot.liftForall is that you need to be able to ensure that if i = i' then your xs' : (i : I) -> X i (the function fed to f) has the property that xs' i = xs' i'. Using xs' i := (xs i).unquot causes problems because this allows internal details of the representation of xs i to leak. In bad, we used xs := id, and so xs' (Squash.mk v) = (Squash.mk v).unquot = v, which makes that property fail (so long as the type we're squashing is nontrivial).

A way around this is to memoize the choices. If you have DecidableEq, you can be sure that xs' uses the same answer for inputs that are Eq, assuming it's possible to lazily construct a data structure backing xs' while xs' is evaluated — I think this is only possible by extending the runtime, and it would be fiddly since you have to worry about concurrency (what if f evaluates xs' at i and i' simultaneously, but i and i' have different internal representations, and i = i'?).

The Quot.finChoice function makes use of the fact the indexing type is finite to be able to make all the choices up front.

[Kyle Miller]

So, I think you can't get around this by marking it as opaque. The issue isn't that theory and evaluation disagree, but that evaluation is wrong.

[Tomas Skrivan]

I see, this should very reasonable. To fully understand it I should go back and understand what Quot.finChoice is actually doing. Anyway thanks a lot for the explanation!

[Kyle Miller]

I suppose another solution is normalizing the index somehow. If your index type is countable, in the strong sense of being Equiv to Nat, then this would probably work and avoid the incorrectness issues:

universe u v

unsafe def Quot.liftForallUnsafe {I : Sort u} {X : I → Sort v} {Y : Sort _}
  (g : ℕ ≃ I)
  {r : (i : I) → X i → X i → Prop}
  (f : ((i : I) → X i) → Y)
  (h : ∀ (xs xs' : (i : I) → X i), (∀ i, r i (xs i) (xs' i)) → f xs = f xs')
  (xs : (i : I) → Quot (r i)) : Y :=
  f (fun i => (g.apply_symm_apply _ ▸ xs (g <| g.symm <| i)).unquot)

@[implemented_by Quot.liftForallUnsafe]
def Quot.liftForall {I : Sort u} {X : I → Sort v} {Y : Sort _}
  (g : ℕ ≃ I)
  {r : (i : I) → X i → X i → Prop}
  (f : ((i : I) → X i) → Y)
  (h : ∀ (xs xs' : (i : I) → X i), (∀ i, r i (xs i) (xs' i)) → f xs = f xs')
  (xs : (i : I) → Quot (r i)) : Y :=
  f (fun i => (xs i).out)

[Kyle Miller]

Let's put the probability on that "probably" fairly low, but I was imagining that the runtime would fully evaluate the Nat produced by g.symm, which seems reasonably safe to assume.

[Kyle Miller]

It doesn't need to be Nat, just any inductive type that we know will evaluate to something concrete.

Notice that the Squash examples can't use this. If A is nonempty, you can't construct Unit ≃ Squash A in general. This function would let you normalize Squash A values. However, assuming A is a Fintype, we're able to construct such a function, which is consistent with our observation that we can't get into trouble with Quotient.finChoice.

[Eric Wieser]

I don't follow how Fintype helps in that Squash example

[Giacomo Stevanato]

Eric Wieser said:

I don't follow how Fintype helps in that Squash example

I believe the intuition is that FinType allows to go through all the values in I and evaluate the Quotient-producing function for those inputs, then the function inside the final Quotient is build using those values. This ensures that computationally that function does not depend on the runtime value of the index i (i.e. it allows normalizing the index), which is ultimately the cause of the unsoundness.

[Kyle Miller]

You can use the Fintype's underlying List, taking its first element. At runtime Fintype is a List.

import Mathlib.Data.Fintype.Quotient

def unitEquivSquash (A : Type _) [instn : Nonempty A] [inst : Fintype A] : Unit ≃ Squash A where
  toFun _ :=
    let ⟨⟨univ, hnd⟩, h⟩ := inst
    Quotient.recOnSubsingleton
      (motive := fun (x : Multiset A) ↦
        (x_1 : x.Nodup) → (∀ (x_2 : A), x_2 ∈ Finset.mk x x_1) → Squash A)
      univ
      (fun (l : List A) hnd h =>
        match l with
        | x :: _ => Squash.mk x
        | [] => False.elim <| instn.elim fun x => by have := h x; simp at this)
      hnd h
  invFun _ := ()
  left_inv _ := rfl
  right_inv := by
    rintro ⟨x⟩
    obtain ⟨⟨⟨_ | ⟨x, _⟩⟩, hnd⟩, h⟩ := inst
    · obtain ⟨x⟩ := instn
      specialize h x
      simp at h
    · exact Quot.sound trivial

(Incidentally this uncovered a bug in elab_as_elim; the explicit motive is a workaround. Fixed in lean4#5266)

[Kyle Miller]

The important part here is that unitEquivSquash A () gives the runtime-canonical value of Squash A, but you could also (unnecessarily) compose this with its inverse to get a function Squash A -> Squash A that does runtime normalization.