subset of quotient

Stream: general

[Johan Commelin]

For the perfectoid project we often need to work with subsets of quotient types. A mathematician would write

def foobar := {x : QuotType | formula x}

and afterwards bother with the proof obligation of showing that it is well-defined. Can we mimic this in Lean?
I imagine that this subset notation would call the appropriate lift lemma, and generate a proof obligation that we can prove after the subset notation. Something like

def foobar := {x : QuotType | formula x} (by proof_of_soundness)

[Johan Commelin]

Maybe we could have { .. | .. } is_well_defined .. be some fancy notation for this type of things?

[Kevin Buzzard]

Do you mean {[[x]] : QuotType | formula x}?

[Johan Commelin]

Does that work?

[Chris Hughes]

Looks like the image of quotient.mk of some set.

[Chris Hughes]

quotient.mk '' {x | formula x}

[Kenny Lau]

there are two ways of forming subquotient

[Kenny Lau]

and a theorem that they are the same

[Kenny Lau]

(in maths, not in Lean)

[Johan Commelin]

Right, I see where this is going...

[Johan Commelin]

In particular, they aren't defeq

[Kenny Lau]

few things are

[Johan Commelin]

So Chris gives a workaround, but proving that his thing is the same as what I want is non-trivial.

[Chris Hughes]

But it's non trivial because there's mathematical content right?

[Johan Commelin]

Right, you have to prove that formula is constant on equivalence classes

[Chris Hughes]

The harder lift definition is probably the best one to use.

[Johan Commelin]

Yes, so I don't mind proving something hard, but I would like to keep a readable definition. Hence this question.

[Mario Carneiro]

To keep the definition readable, make the well definedness part a lemma that you prove immediately before

[Johan Commelin]

@Mario Carneiro That is certainly an option, but
(1) the definition still won't be able to use subset notation;
(2) it is not what mathematicians are used to. We always define something, and afterwards fill in the proof obligation of showing that the definition is well-defined.

[Mario Carneiro]

I think that it matches mathematical practice in that you aren't licensed to use the definition until you have proven the well definedness condition

[Mario Carneiro]

in lean if you can say it you can use it, so you have to be intercepted right at the definition

[Mario Carneiro]

I'm a little confused about what exactly you want to write though

[Johan Commelin]

I completely agree.

[Johan Commelin]

So my suggestion was to syntactically prove the well-definedness after the definition. But in fact it is just part of the definition.

[Johan Commelin]

Most importantly, I would like the definition to be very readable.

[Mario Carneiro]

Isn't that what quot.lift already does?

[Johan Commelin]

Yes. But then my subset notation goes out of the window.

[Mario Carneiro]

Can you be more specific?

[Johan Commelin]

Any mathematician who first looks at Lean, and wants to look up the definition of Spv in the perfectoid project will not understand anything if he/she sees a quot.lift.

[Johan Commelin]

That is completely foreign.

[Johan Commelin]

And the stuff that follows it is barely recognisable.

[Johan Commelin]

On the other hand

def foobar := {x : QuotType | formula x} is_well_defined (by proof_of_soundness)

is very readable.

[Johan Commelin]

But my Lean-fu is not sufficient to turn that into valid Lean.

[Johan Commelin]

Currently in the perfectoid project we are stacking 5 subquotients on top of each other.

[Johan Commelin]

And it becomes really horrible.

[Johan Commelin]

(Well, currently there is no quot, but that isn't tenable either. So we need the quot, and we'dd like it to be readable.)

[Kevin Buzzard]

I am confused about why your def is not valid lean

[Kevin Buzzard]

I wrote what I thought you were trying to say but you have not adopted my change

[Johan Commelin]

Sorry, which change are you talking about?

[Kevin Buzzard]

I mean, I wrote what I thought was invalid lean

[Kevin Buzzard]

I put the equiv class notation in

[Johan Commelin]

Right. So now I tried using Chris's suggestion.

[Johan Commelin]

But then you can define Spa, and you get stuck when you want to define the opens.

[Johan Commelin]

To paraphrase Mario:

But I do not want to be thinking about quot.lift and subtype.val when I am writing a proof
the mindset is completely different, it is a distraction

[Mario Carneiro]

Is your foobar stuff about Spa? If so can you show what it looks like in situ

[Kevin Buzzard]

All I am saying is that you keep saying that something is invalid lean and it looks fine to me

[Chris Hughes]

But the definitional equality of quotient.lift is really handy. Just give a docstring. Aiming to make your code usable by someone who doesn't know what quotient.lift is is probably impossible.

[Kevin Buzzard]

And I wrote something which was invalid lean and asked if it was what you meant and all you did was asked me if my invalid lean was valid

[Kevin Buzzard]

So we're clearly at cross purposes. My question is what is invalid about your lean

[Patrick Massot]

Are we talking about def foobar := {x : QuotType | formula x} is_well_defined (by proof_of_soundness)?

[Mario Carneiro]

In the case of Spa, I don't think you should try to get defeq just right, because Spa itself is not quite a quotient in the way we want it to be anyway

[Patrick Massot]

It seems pretty invalid to me

[Kevin Buzzard]

I don't have access to lean right now so I'll just shut up and stop adding to the noise

[Johan Commelin]

@Kevin Buzzard Sorry, I finally understand. I think {[[x]] : QuotType | formula x} doesn't leave any room for the proof obligation that formula x only depends on [[x]]. That proof has to go somewhere. Mathematicians also do that.

[Mario Carneiro]

That's a perfectly valid definition, which means the image of such and such

[Mario Carneiro]

why not {q : QuotType | formula q}

[Mario Carneiro]

and define formula q using a lift

[Johan Commelin]

definition Spa (A : Huber_pair) := quotient.mk '' {v : Valuation A | v.is_continuous ∧ ∀ r, r ∈ A⁺ → v r ≤ 1}

[Johan Commelin]

This is what I have now.

[Mario Carneiro]

is is_continuous constant on equivalence classes?

[Johan Commelin]

And

variables (R : Type u₁) [comm_ring R] [decidable_eq R]

structure Valuation (R : Type u₁) [comm_ring R] :=
(Γ   : Type u₁)
(grp : linear_ordered_comm_group Γ)
(val : @valuation R _ Γ grp)

namespace Valuation

instance : has_coe_to_fun (Valuation R) :=
{ F := λ v, R → with_zero v.Γ, coe := λ v, v.val.val }

instance linear_ordered_value_group {v : Valuation R} : linear_ordered_comm_group v.Γ := v.grp

end Valuation

instance Spv.setoid : setoid (Valuation R) :=
{ r := λ v₁ v₂, ∀ r s, v₁ r ≤ v₁ s ↔ v₂ r ≤ v₂ s,
  iseqv := begin
    split,
    { intros v r s, refl },
    split,
    { intros v₁ v₂ h r s, symmetry, exact h r s },
    { intros v₁ v₂ v₃ h₁ h₂ r s,
      exact iff.trans (h₁ r s) (h₂ r s) }
  end }

definition Spv := quotient (Spv.setoid R)

[Johan Commelin]

@Mario Carneiro Yes it is, but the proof is sorried.

[Kevin Buzzard]

is is_continuous constant on equivalence classes?

yes, although I was waiting for module refactoring to prove it.

[Johan Commelin]

Yep, that will need quite some module-juggling.

[Johan Commelin]

And a bit of tfae-icing :lol:

[Kevin Buzzard]

It is mostly rings but I was using module refactoring as an excuse to put it off

[Mario Carneiro]

what happened to the relations?

[Johan Commelin]

Which relations?

[Johan Commelin]

Aah, lol, they are gone

[Johan Commelin]

They are in the setoid

[Johan Commelin]

So there are no longer relations on R.

[Mario Carneiro]

The reason for that definition was because the quotient doesn't work

[Johan Commelin]

So how can you define lift and friends using the relations?

[Mario Carneiro]

it's not universe polymorphic enough, and your definition lives in a higher universe

[Mario Carneiro]

That's what the whole thing about generating valuations is for

[Johan Commelin]

To me quot is a bunch of C++ magic that somehow works. But I don't know how to provide my own lift without at some point resorting to quot.lift.

[Mario Carneiro]

You do it the old fashioned way

[Mario Carneiro]

with sets

[Johan Commelin]

Sorry, I don't follow.

[Johan Commelin]

Given a relation on R. How do you get a valuation?

[Kevin Buzzard]

For the perfectoid project we often need to work with subsets of quotient types. A mathematician would write

def foobar := {x : QuotType | formula x}

and afterwards bother with the proof obligation of showing that it is well-defined. Can we mimic this in Lean?

variables (QuotType : Type) (formula : QuotType → Prop)
definition X := {x : QuotType | formula x}

Mimicked. That was what I was trying to say.

[Mario Carneiro]

The relation is assumed to be the image of some valuation

[Johan Commelin]

Could you write down the definition of lift (with a sorry)?

[Johan Commelin]

I couldn't write down anything of which I was even sure that a proof existed.

[Mario Carneiro]

Wasn't this already done in an earlier version?

[Johan Commelin]

No, only the claim that it should be done.

[Johan Commelin]

mk was done. That's not so hard.

[Johan Commelin]

But lift wasn't.

[Kevin Buzzard]

mk took me forever

[Kevin Buzzard]

Wasn't this the one where I had to invoke the first isomorphism theorem between objects in different universes?

[Mario Carneiro]

yes

[Kevin Buzzard]

I thought I did most of the hard work for this

[Kevin Buzzard]

and that everything else was just noise modulo continuous being constant on equiv classes

[Johan Commelin]

Hmm, sorry. That wasn't nice to say. You indeed need all the minimal_valuation stuff.

[Johan Commelin]

But once that is there mk is not very hard.

[Kevin Buzzard]

I'm not offended, I am just aware that there are issues here I don't understand so am a bit scared of messing with stuff

[Johan Commelin]

definition Spv :=
-- quotient (Spv.setoid R)
{ineq : R → R → Prop // ∃ {Γ : Type u₁} [linear_ordered_comm_group Γ],
  by exactI ∃ (v : valuation R Γ), ∀ r s : R, v r ≤ v s ↔ ineq r s}

[Johan Commelin]

Voila, the old definition.

[Johan Commelin]

I agree that the universe issue wasn't solved by what I did. (I'm really silly when it comes to universes.)

[Johan Commelin]

@Mario Carneiro Do you think this would work?

definition lift {β : Type u₃} (f : Valuation R → β)
(H : ∀ v₁ v₂ : Valuation R, v₁ ≈ v₂ → f v₁ = f v₂) : Spv R → β := sorry

[Mario Carneiro]

can you post enough to make Spv compile? Stub out the definition of valuation and such

[Mario Carneiro]

mathlib doesn't have linear_ordered_comm_group

[Johan Commelin]

import valuations
import analysis.topology.topological_space
import data.finsupp
import group_theory.quotient_group

universes u₁ u₂ u₃

namespace valuation

class is_valuation {R : Type u₁} [comm_ring R] {Γ : Type u₂} [linear_ordered_comm_group Γ]
  (v : R → with_zero Γ) : Prop :=
(map_zero : v 0 = 0)
(map_one  : v 1 = 1)
(map_mul  : ∀ x y, v (x * y) = v x * v y)
(map_add  : ∀ x y, v (x + y) ≤ v x ∨ v (x + y) ≤ v y)

end valuation

def valuation (R : Type u₁) [comm_ring R] (Γ : Type u₂) [linear_ordered_comm_group Γ] :=
{ v : R → with_zero Γ // valuation.is_valuation v }
variables (R : Type u₁) [comm_ring R] [decidable_eq R]

open valuation

structure Valuation (R : Type u₁) [comm_ring R] :=
(Γ   : Type u₁)
(grp : linear_ordered_comm_group Γ)
(val : @valuation R _ Γ grp)

namespace Valuation

instance : has_coe_to_fun (Valuation R) :=
{ F := λ v, R → with_zero v.Γ, coe := λ v, v.val.val }

instance linear_ordered_value_group {v : Valuation R} : linear_ordered_comm_group v.Γ := v.grp

end Valuation

instance Spv.setoid : setoid (Valuation R) :=
{ r := λ v₁ v₂, ∀ r s, v₁ r ≤ v₁ s ↔ v₂ r ≤ v₂ s,
  iseqv := begin
    split,
    { intros v r s, refl },
    split,
    { intros v₁ v₂ h r s, symmetry, exact h r s },
    { intros v₁ v₂ v₃ h₁ h₂ r s,
      exact iff.trans (h₁ r s) (h₂ r s) }
  end }

definition Spv :=
{ineq : R → R → Prop // ∃ {Γ : Type u₁} [linear_ordered_comm_group Γ],
  by exactI ∃ (v : valuation R Γ), ∀ r s : R, v r ≤ v s ↔ ineq r s}

namespace Spv

variables {R} {Γ : Type u₂} [linear_ordered_comm_group Γ]

definition mk (v : valuation R Γ) : Spv R :=
⟨λ r s, v r ≤ v s,
  ⟨(minimal_value_group v).Γ,
    ⟨minimal_value_group.linear_ordered_comm_group v,
      ⟨v.minimal_valuation, v.minimal_valuation_equiv⟩⟩⟩⟩

definition lift {β : Type u₃} (f : Valuation R → β) (H : ∀ v₁ v₂ : Valuation R, v₁ ≈ v₂ → f v₁ = f v₂) :
Spv R → β := quotient.lift f H

[Johan Commelin]

Aah, too bad mathlib doesn't have that.

[Mario Carneiro]

mathlib has the decidable version

[Mario Carneiro]

(rather core has it)

[Mario Carneiro]

is there a reason that doesn't work here?

[Kevin Buzzard]

I agree that the universe issue wasn't solved by what I did. (I'm really silly when it comes to universes.)

I don't know if there is a universe issue with your version. I find subtypes easier to use than quotient types but this might just be lack of practice. I am happy if you think a change will make it more readable but I don't want to run into universe issues. My understanding of the universe issues is that I should not let a valuation be an "equivalence class" of v : R -> with_zero Gamma where Gamma is allowed to vary over any type in any universe. I instead restricted to Gamma varying over things in the same universe as R and then I had to work to show that if I had a Gamma in another universe it was equivalent to Gamma in R's universe. I think that these issues (which I don't understand fully) are not the same as the one Johan is talking about, which is defining Spv not to be the ordering on R but to be the equiv class of valuations which give the ordering, so my guess is that these changes should be fine as long as the equiv reln is defined on valuations taking values in things in R's universe. I am not 100% sure that this is the point but that's my current understanding; I'm currently about to start travelling for 2 hours by the way.

[Johan Commelin]

@Mario Carneiro Mathlibcore has the additive version...

[Mario Carneiro]

Unfortunately, you can't even take an equivalence class over all valuations with type in the same universe as R, because this is already too big

[Johan Commelin]

I have

hv :
  ∃ {Γ : Type u₁} [_inst_3 : linear_ordered_comm_group Γ] (v_1 : valuation R Γ),
    ∀ (r s : R), ⇑v_1 r ≤ ⇑v_1 s ↔ v r s

in my local context. Somehow cases hv complains that it can only eliminate into Prop. :cry:

[Mario Carneiro]

The best you can do is take an equivalence class over all valuations in some "small" collection of representatives

[Mario Carneiro]

Use classical.cases_on

[Johan Commelin]

Unfortunately, you can't even take an equivalence class over all valuations with type in the same universe as R, because this is already too big

Like I just experienced (-;

[Mario Carneiro]

I'm still struggling to get your file to compile, but that's what I was going to do

[Mario Carneiro]

just use classical.cases_on three times and apply the function

[Mario Carneiro]

You won't even need the well definedness assumption, it's just for show

[Johan Commelin]

Let me try

[Johan Commelin]

How do I "use" classical.cases_on with hv?

[Mario Carneiro]

refine classical.cases_on hv (\lam Gamma h', _)

[Johan Commelin]

I see

[Johan Commelin]

Good old refine

[Mario Carneiro]

You might be able to use a custom recursor with induction but I find refine the most straightforward

[Johan Commelin]

type mismatch at application
  classical.cases_on hv
term
  hv
has type
  ∃ {Γ : Type u₁} [_inst_3 : linear_ordered_comm_group Γ] (v_1 : valuation R Γ),
    ∀ (r s : R), ⇑v_1 r ≤ ⇑v_1 s ↔ v r s : Prop
but is expected to have type
  Prop : Type

[Johan Commelin]

Also... lunch time

[Johan Commelin]

See you later

[Mario Carneiro]

lol

[Mario Carneiro]

sorry, I think it's called classical.rec_on

[Mario Carneiro]

it's a bad name

[Mario Carneiro]

it should be more like exists.rec_on_classical

[Johan Commelin]

noncomputable definition lift {β : Type u₃} (f : Valuation R → β) (H : ∀ v₁ v₂ : Valuation R, v₁ ≈ v₂ → f v₁ = f v₂) :
Spv R → β :=
begin
intro v,
cases v with v hv,
refine classical.rec_on hv (λ Γ hv', _),
refine classical.rec_on hv' (λ inst hv'', _),
refine classical.rec_on hv'' (λ v h, _),
exact f {Γ := Γ, grp := inst, val := v}
end

[Johan Commelin]

That kind of worked. But I didn't use H

[Patrick Massot]

Mario announced that you wouldn't need H

[Johan Commelin]

So, is this some sort of "cheating" definition?

[Johan Commelin]

I guess we should leave H in place, because otherwise lift can be abused.

[Reid Barton]

You will need H to prove that lift f H (mk v) = f v

[Johan Commelin]

Good point. Let me prove such things now.

[Patrick Massot]

It seems this is a very convenient way to setup things: define stuff without precondition, and prove they have the expected properties under the appropriate conditions. An extreme example is https://github.com/leanprover-community/mathlib/blob/b3b50ce67c8b73442372c5141e8836c64ea13826/analysis/topology/completion.lean#L442-L446

[Johan Commelin]

Now I'm stuck on the following goal:

⊢ classical.rec_on _
      (λ (Γ : Type u₁)
       (hv' :
         ∃ [_inst_3 : linear_ordered_comm_group Γ] (v_1 : valuation R Γ),
           ∀ (r s : R), ⇑v_1 r ≤ ⇑v_1 s ↔ ⇑(v.val) r ≤ ⇑(v.val) s),
         classical.rec_on hv'
           (λ (inst : linear_ordered_comm_group Γ)
            (hv'' : ∃ (v_1 : valuation R Γ), ∀ (r s : R), ⇑v_1 r ≤ ⇑v_1 s ↔ ⇑(v.val) r ≤ ⇑(v.val) s),
              classical.rec_on hv''
                (λ (v_1 : valuation R Γ) (h : ∀ (r s : R), ⇑v_1 r ≤ ⇑v_1 s ↔ ⇑(v.val) r ≤ ⇑(v.val) s),
                   f {Γ := Γ, grp := inst, val := v_1}))) =
    f v

The maths is clear, but I have no idea how to work with this classical.rec_on. How do I fight those?

[Johan Commelin]

Ok, so I can turn it into the rather unhelpful:

lemma lift_mk {β : Type u₃} {f : Valuation R → β} {H : ∀ v₁ v₂ : Valuation R, v₁ ≈ v₂ → f v₁ = f v₂} (v : Valuation R) :
lift f H (mk v) = f v :=
begin
  refine H _ _ _,
  -- ⊢ {Γ := classical.some _, grp := classical.some _, val := classical.some _} ≈ v
end

[Johan Commelin]

As you can see in the code, there is this bit saying (hv'' : ∃ (v_1 : valuation R Γ), ∀ (r s : R), ⇑v_1 r ≤ ⇑v_1 s ↔ ⇑(v.val) r ≤ ⇑(v.val) s),. I need to extract that, and use it to close my goal.

[Johan Commelin]

Ok, from browsing code I think that I should use some_spec or some_spec2. Can anyone confirm that this is reasonable? (I have yet to figure out how I should use them...)

[Johan Commelin]

This is what I have now:

lemma lift_mk {β : Type u₃} {f : Valuation R → β} {H : ∀ v₁ v₂ : Valuation R, v₁ ≈ v₂ → f v₁ = f v₂} (v : Valuation R) :
lift f H (mk v) = f v :=
begin
  let ineq := mk v,
  have foo := classical.some_spec (ineq.2),
  refine H _ _ _,
  intros r s,
end
-- R : Type u₁,
-- _inst_1 : comm_ring R,
-- _inst_2 : decidable_eq R,
-- β : Type u₃,
-- f : Valuation R → β,
-- H : ∀ (v₁ v₂ : Valuation R), v₁ ≈ v₂ → f v₁ = f v₂,
-- v : Valuation R,
-- ineq : Spv R := mk v,
-- foo : ∀ (r s : R), ⇑(classical.some _) r ≤ ⇑(classical.some _) s ↔ ineq.val r s,
-- r s : R
-- ⊢ ⇑(classical.some _) r ≤ ⇑(classical.some _) s ↔ ⇑v r ≤ ⇑v s

Looks deceptively close, but I can't finish it.

[Johannes Hölzl]

Yes, if you want to proof something about classical.some. What you usually do is to define a the constant using classical.some and then proof when a corresponding value exists, then the constant has the properties.

[Johannes Hölzl]

what is the type of _ in classical.some _?

[Johan Commelin]

Hooray!

lemma lift_mk {β : Type u₃} {f : Valuation R → β} {H : ∀ v₁ v₂ : Valuation R, v₁ ≈ v₂ → f v₁ = f v₂} (v : Valuation R) :
lift f H (mk v) = f v :=
begin
  let ineq := mk v,
  have spec := classical.some_spec (mk v).property,
  refine H _ _ _,
  intros r s,
  dsimp [mk] at spec,
  exact spec r s
end

[Johan Commelin]

Somehow I managed to convince Lean!

[Andrew Ashworth]

I agree some_spec is awkward, but for what it's worth, it is mentioned in TPIL. When I first saw the example provided in 11.6 I didn't have any idea how it worked.

[Andrew Ashworth]

open classical function
local attribute [instance] prop_decidable

noncomputable definition linv {α β : Type} [h : inhabited α]
  (f : α → β) : β → α :=
λ b : β, if ex : (∃ a : α, f a = b) then some ex else arbitrary α

theorem linv_comp_self {α β : Type} {f : α → β}
    [inhabited α] (inj : injective f) :
  linv f ∘ f = id :=
funext (assume a,
  have ex  : ∃ a₁ : α, f a₁ = f a, from exists.intro a rfl,
  have   feq : f (some ex) = f a, from some_spec ex,
  calc linv f (f a) = some ex :  dif_pos ex
             ...    = a       :  inj feq)