## 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