quotient.induction_on order of variables

Stream: general

[Kevin Buzzard]

I noticed something when descending proofs from a function on an object to a function on a quotient object. In short: I have v : R -> X satisfying some axioms, and it is constant on cosets of J so it descends to a function vbar: R/J -> X. I now need to prove that vbar satisfies the axioms which v satisfies, and in each case the proof is "this follows immediately". But look at my proofs:

  map_zero := map_zero v,
  map_one := map_one v,
  map_mul := λ x y, quotient.induction_on₂' x y $
    λ a b, -- my goal does not even mention x and y
    map_mul _ _ _,

The function map_mul wants two elements x and y of R/J and then a proof that vbar(x*y)=vbar(x)*vbar(y). I eat x and y and then apply one of these standard quotient.induction_on₂' functions which instantly wants x and y as input, plus a proof that for all a,b in R, v(a*b)=v(a)*v(b). My goal does not even mention x and y, they have already been used.

So I defined a new quotient.induction_on₂'' which asks for the proof first (it is simply re-ordering the inputs):

definition quotient.induction_on₂'' :
∀ {α : Sort*} {β : Sort*} {s₁ : setoid α} {s₂ : setoid β}
{p : quotient s₁ → quotient s₂ → Prop}
-- this first
(h : ∀ (a₁ : α) (a₂ : β), p (quotient.mk' a₁) (quotient.mk' a₂))
-- then these
(q₁ : quotient s₁) (q₂ : quotient s₂), p q₁ q₂
:= λ α β s₁ s₂ p h q₁ q₂, quotient.induction_on₂' q₁ q₂ h

and now for map_add I could just write

map_add := quotient.induction_on₂'' (λ a b, map_add _ _ _)

People here are smart and they must have realised this before. Is my quotient.induction_on₂'' function already in Lean or mathlib?

[Kevin Buzzard]

Hmm, does _on mean "I am going to ask for the variables first", like rec_on?

[Rob Lewis]

Hmm, does _on mean "I am going to ask for the variables first", like rec_on?

Yes, usually. Without looking at the details, is quotient.ind₂ what you want?

[Patrick Massot]

@Kevin Buzzard Did you trying using more rintro magic as I told you?

[Patrick Massot]

as in

import ring_theory.ideals

variables (R : Type) [comm_ring R] (I : ideal R)

example : ∀ x : I.quotient, true :=
begin
  rintro ⟨x⟩,
  trivial
end

look at tactic state after the first line

[Kevin Buzzard]

I am not even in tactic mode; I want to say "this is trivial" as quickly as possible.

[Kevin Buzzard]

I wasn't in front of Lean when the penny dropped about _on but now I am, and I think that the ' also has a meaning -- ' means "use quotient.mk' not quotient.mk". I am only just getting to the bottom of things. Maybe I want quotient.ind₂'? Is that the name of this function? It doesn't appear to be there.

[Kevin Buzzard]

So apparently quotient.mk means "infer the equivalence relation using type class inference" and quotient.mk' means "infer it using unification"

[Kevin Buzzard]

In my situation I have a quotient of a ring by an ideal, and rings have lots of ideals, so I guess I will not be using type class inference. This seems to put me in the ' world. So currently my belief is that the function I want should be called quotient.ind₂'.

[Kevin Buzzard]

And I can't find this. Have I got this straight? My conclusion is that I should write a short PR adding quotient.ind' and quotient.ind₂' and maybe a 3 variable version, to data/quot.lean.

[Chris Hughes]

quotient.induction_on' and quotient.induction_on₂'

[Kevin Buzzard]

The variables are in the wrong order for me with _on

[Kevin Buzzard]

#check @quotient.ind'
/-
quotient.ind' :
  ∀ {α : Sort u_5} {s₁ : setoid α} {p : quotient s₁ → Prop},
    (∀ (a : α), p (quotient.mk' a)) → ∀ (q : quotient s₁), p q
    -/
#check @quotient.induction_on'
/-
quotient.induction_on' :
  ∀ {α : Sort u_5} {s₁ : setoid α} {p : quotient s₁ → Prop} (q : quotient s₁),
    (∀ (a : α), p (quotient.mk' a)) → p q
    -/

I want the hypothesis before the quotient variables. I hope I've understood the rules for naming these functions correctly.