# Zulip Chat Archive

## Stream: new members

### Topic: Writing decidable_nonneg for a quotient type.

#### kvanvels (Aug 25 2022 at 22:41):

I am trying to define the integers as a quotient group of pairs of natural numbers. I am am trying to extend the construction as in here.. In this construction, two pairs of natural numbers $(a_p,a_n), (b_p,b_n)$ are equivalent if $a_p + b_n = b_p+a_n$.

The way to define (almost all?) most function/relations on the the quotient group is outlined in the linked file. I am having trouble extending this approach to a function like `decidable_nonneg`

because the type of the output depends on the input (a Pi term). I have looked at certain functions like "quot.lift_beta" but haven't been able to get anything to work. what follows is my minimal (non-working) example.

```
import tactic
abbreviation N2 := ℕ × ℕ
namespace N2
def r (ab cd : N2) : Prop :=
ab.1 + cd.2 = cd.1 + ab.2
lemma r_def (ab cd : N2) : r ab cd ↔ ab.1 + cd.2 = cd.1 + ab.2 := iff.rfl
def r_refl : reflexive r := sorry
def r_symm : symmetric r := sorry
def r_trans : transitive r := sorry
namespace Z
instance mysetoid : setoid N2 := ⟨r, r_refl, r_symm, r_trans⟩
@[simp] lemma equiv_def (ab cd : N2) : ab ≈ cd ↔ ab.1 + cd.2 = cd.1 + ab.2 := iff.rfl
def Z := quotient N2.Z.mysetoid
def nonneg_aux (ab : N2) : Prop :=
(ab.snd ≤ ab.fst)
@[simp] lemma nonneg_aux_def (a0 a1 : ℕ) :
nonneg_aux (a0,a1) ↔ a1 ≤ a0 := iff.rfl
def nonneg (a : Z) : Prop :=
begin
revert a,
apply quotient.lift nonneg_aux,
rintros ⟨_,_⟩ ⟨_,_⟩,
simp,
sorry,
--the rest is very simple so i skipped it
end
def decidable_nonneg_aux (ab : N2) : decidable (nonneg_aux ab) :=
begin
cases ab with p0 p1,
rw nonneg_aux_def,
exact nat.decidable_le p1 p0,
end
@[simp] lemma decidable_nonneg_aux_def (a0 a1 : ℕ) :
decidable_nonneg_aux (a0,a1) = (nat.decidable_le a1 a0) := rfl
def decidable_nonneg (a : Z) : decidable (nonneg a) :=
begin
revert a,
sorry,
--- How do proceed here? The normal approach of using "apply quotient.lift nonneg_aux" doesnt work,
--I think because of the "Pi" term.
end
end Z
end N2
```

Please let me know if I am on the wrong path. I plan on doing this same construction to generate a toy version of the rationals and then I would like to generate/define the real numbers as equivalence classes of Cauchy sequences, so getting this correct seems important even if it just an exercise. Any ideas/help is appreciated.

Thanks you.

#### Eric Wieser (Aug 25 2022 at 22:43):

For the dependent version you need docs#quotient.rec_on, but you can also use the more convenient docs#quotient.rec_on_subsingleton

#### kvanvels (Aug 25 2022 at 22:48):

Thank you. I appreciate it. I will follow up if I have more questions.

#### Kent Van Vels (Aug 25 2022 at 23:46):

Thank you. I got it to work. I had to add a "definitional lemma" so I could rewrite `nonneg`

in the proof. Does "rec" stand for recurse, or record or something else? I had the return type incorrect in my `decidable_nonneg_aux`

definition.

I was successful with the `quotient.rec_on`

and got pretty far with the `quotient.rec_on_subsington`

, but in the latter case, I got stuck at

```
a : Z,
p0 p1 : ℕ
⊢ subsingleton (decidable (p1 ≤ p0))
```

Any ideas here? I can generate `decidable (p1<= p0)`

from `nat.decidable_le p1 p0`

.

I really appreciate the help. Thanks again.

#### Mario Carneiro (Aug 25 2022 at 23:48):

`rec`

stands for "recursor"

#### Mario Carneiro (Aug 25 2022 at 23:48):

If you use `quotient.rec_on_subsington`

the subsingleton side goal should be automatically proved by typeclass inference. How are you using it?

#### Kent Van Vels (Aug 25 2022 at 23:53):

I am just working on a file that was identical to my minimal working example. To be honest, I don't even know what "typeclass inference means. :smiley:

For your convenience, here is the current state of my code.

```
import tactic
abbreviation N2 := ℕ × ℕ
namespace N2
def r (ab cd : N2) : Prop :=
ab.1 + cd.2 = cd.1 + ab.2
lemma r_def (ab cd : N2) : r ab cd ↔ ab.1 + cd.2 = cd.1 + ab.2 := iff.rfl
def r_refl : reflexive r := sorry
def r_symm : symmetric r := sorry
def r_trans : transitive r := sorry
namespace Z
instance mysetoid : setoid N2 := ⟨r, r_refl, r_symm, r_trans⟩
@[simp] lemma equiv_def (ab cd : N2) : ab ≈ cd ↔ ab.1 + cd.2 = cd.1 + ab.2 := iff.rfl
def Z := quotient N2.Z.mysetoid
def nonneg_aux (ab : N2) : Prop :=
(ab.snd ≤ ab.fst)
@[simp] lemma nonneg_aux_def (a0 a1 : ℕ) :
nonneg_aux (a0,a1) ↔ a1 ≤ a0 := iff.rfl
def nonneg (a : Z) : Prop :=
begin
revert a,
apply quotient.lift nonneg_aux,
rintros ⟨_,_⟩ ⟨_,_⟩,
simp,
intro h₀,
apply iff.intro,
intro h₁,
linarith,
intro h₁,
linarith,
end
@[simp] lemma nonneg_def (p0 p1 : ℕ) : Z.nonneg ⟦(p0,p1)⟧ ↔ p1 ≤ p0 := iff.rfl
def decidable_nonneg_aux (ab : N2) : decidable (nonneg (⟦ab⟧ : Z)) :=
begin
cases ab with a b,
rw nonneg_def,
exact nat.decidable_le b a,
end
def decidable_nonneg_NOT_WORKING (a : Z) : decidable (nonneg a) :=
begin
apply (quotient.rec_on_subsingleton a),
rintros ⟨p0,p1⟩,
rw nonneg_def,
exact nat.decidable_le p1 p0,
rintros ⟨p0,p1⟩,
rw nonneg_def,
sorry,
end
def decidable_nonneg_WORKING (a : Z) : decidable (nonneg a) :=
begin
apply (quotient.rec_on a),
rintros ⟨p0,p1⟩ ⟨p2,p3⟩,
intro h0,
simp,
apply decidable_nonneg_aux,
end
end Z
end N2
```

#### Mario Carneiro (Aug 25 2022 at 23:54):

don't use `apply`

, use `refine`

#### Mario Carneiro (Aug 25 2022 at 23:54):

`refine quotient.rec_on_subsingleton a _`

#### Kent Van Vels (Aug 25 2022 at 23:58):

I haven't used refine at all. I will be looking into it. I didn't understand what it did when I read about it. But yeah, I will be looking in to it.

I got it to work using refine for the `rec_on_subsingleton`

case.... but not on the "vanilla" `rec_on`

case.

#### Mario Carneiro (Aug 25 2022 at 23:59):

you have to put the right number of underscores at the end corresponding to the subgoals

#### Mario Carneiro (Aug 26 2022 at 00:00):

`rec_on`

has two subgoals, one for the function and one for the proof that the function respects the equivalence relation

#### Mario Carneiro (Aug 26 2022 at 00:01):

`refine`

lets you give a partial proof term for the goal, where any `_`

in the term turn into subgoals

#### Mario Carneiro (Aug 26 2022 at 00:02):

`apply`

tries to automatically figure out how many trailing `_`

there are but this has some side effects in this case

#### Kent Van Vels (Aug 26 2022 at 00:03):

Ok, that worked. I read the pop up help and now I understand what it does.

#### Kent Van Vels (Aug 26 2022 at 00:06):

Just for my future reference, do you know how I can show `subsingleton (decidable (p1 <= p0))`

for two natural numbers p0 p1. Is a `subsingleton`

something like the empty-set?

#### Mario Carneiro (Aug 26 2022 at 00:06):

a subsingleton is a type with at most one element

#### Kent Van Vels (Aug 26 2022 at 00:07):

Ha, ok. A "sub-or-equal" singleton.

#### Mario Carneiro (Aug 26 2022 at 00:07):

`decidable p`

is a subsingleton because there are only two different ways to prove `decidable p`

and they can never both apply simultaneously

#### Mario Carneiro (Aug 26 2022 at 00:07):

it means "subset of a singleton"

#### Mario Carneiro (Aug 26 2022 at 00:08):

If you have a goal of `subsingleton (decidable p)`

for some reason, then you can prove it by `apply_instance`

#### Kent Van Vels (Aug 26 2022 at 00:08):

yeah, I guess I turned that in my head to "(proper) subset of a singleton". :)

#### Mario Carneiro (Aug 26 2022 at 00:09):

which explicitly calls typeclass inference (normally that happens automatically but `apply`

constructed the proof in a weird way and it ended up as a subgoal)

#### Mario Carneiro (Aug 26 2022 at 00:09):

If you do `show_term { apply_instance }`

you can see the actual theorem being applied

#### Mario Carneiro (Aug 26 2022 at 00:10):

I think it would be docs#decidable.subsingleton

#### Kent Van Vels (Aug 26 2022 at 00:11):

library_search worked too, I gave up too easily.

#### Mario Carneiro (Aug 26 2022 at 00:11):

but I want to emphasize that these lemmas are explicitly not intended for directly being referenced

#### Mario Carneiro (Aug 26 2022 at 00:11):

you should use `apply_instance`

#### Mario Carneiro (Aug 26 2022 at 00:11):

or just rejigger the proof so that the goal doesn't appear in the first place

#### Kent Van Vels (Aug 26 2022 at 00:12):

Is it a rule/expectation here to use your real name? I have never been on a message board with almost everyone using real (looking) names.

#### Mario Carneiro (Aug 26 2022 at 00:13):

It's not a requirement, but it is preferred. It helps establish this place as a professional environment

#### Kent Van Vels (Aug 26 2022 at 00:15):

Well, I will be changing my handle. My name is Kent Van Vels. I really appreciate the help. I have a lot to learn. Thanks again.

#### Kevin Buzzard (Aug 27 2022 at 09:03):

@Kent Van Vels you were looking at a course I gave in 2021. In 2022 I slightly revised my approach to quotients; you can see it here https://github.com/ImperialCollegeLondon/formalising-mathematics-2022/tree/master/src/section06quotients .

As for real names, yeah I know it's weird, but this isn't a chat room (even though it looks like a chat room), it's a serious research forum. I sometimes don't respond to people who aren't using their real names here (in contrast to my Discord, where there are a ton of people who aren't using their real names and this is fine).

#### Kent Van Vels (Aug 27 2022 at 15:50):

Thank you, I think I will be going through those notes right now.

Last updated: Dec 20 2023 at 11:08 UTC