Writing decidable_nonneg for a quotient type.

Stream: new members

[kvanvels]

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]

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

[kvanvels]

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

[Kent Van Vels]

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]

rec stands for "recursor"

[Mario Carneiro]

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]

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]

don't use apply, use refine

[Mario Carneiro]

refine quotient.rec_on_subsingleton a _

[Kent Van Vels]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

refine lets you give a partial proof term for the goal, where any _ in the term turn into subgoals

[Mario Carneiro]

apply tries to automatically figure out how many trailing _ there are but this has some side effects in this case

[Kent Van Vels]

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

[Kent Van Vels]

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]

a subsingleton is a type with at most one element

[Kent Van Vels]

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

[Mario Carneiro]

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]

it means "subset of a singleton"

[Mario Carneiro]

If you have a goal of subsingleton (decidable p) for some reason, then you can prove it by apply_instance

[Kent Van Vels]

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

[Mario Carneiro]

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]

If you do show_term { apply_instance } you can see the actual theorem being applied

[Mario Carneiro]

I think it would be docs#decidable.subsingleton

[Kent Van Vels]

library_search worked too, I gave up too easily.

[Mario Carneiro]

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

[Mario Carneiro]

you should use apply_instance

[Mario Carneiro]

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

[Kent Van Vels]

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]

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

[Kent Van Vels]

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]

@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]

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