has_le isn't working even though has_add, has_mul, etc are.

Stream: new members

[kvanvels]

I come across a tutorial on defining mathematical classes from the use of equivalence classes here on Dr. Buzzards web page. I did the tutorial and as a further exercise I want to define an ordering on Z. So I added the appropriate le_aux, le_aux_def, le functions/proofs. I added the line instance : has_le Z := ⟨le⟩ to allow me (I thought) to use the (less or equal) symbol like I could use the plus sign for addition and the star for multiplication.

If anyone can tell me what I did wrong in the following code, I would appreciate it.

The following code is probably overkill, but I wanted to show that lean had no issue with accepting has_zero, has_one, has_add, etc.

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 := by refl
lemma r_def' (a b c d : ℕ) : r (a,b) (c,d) ↔ a + d = c + b := by refl


def r_refl : reflexive r := sorry
def r_symm : symmetric r := sorry
def r_trans : transitive r := sorry

instance setoid : setoid N2 := ⟨r, r_refl, r_symm, r_trans⟩

example (x y : N2) : x ≈ y ↔ r x y := by refl
@[simp] lemma equiv_def (ab cd : N2) : ab ≈ cd ↔ ab.1 + cd.2 = cd.1 + ab.2 := by refl
@[simp] lemma equiv_def' (a b c d : ℕ) : (a,b) ≈ (c,d) ↔ a + d = c + b := iff.rfl
end N2

-- Now we can take the quotient!
def Z := quotient N2.setoid

namespace Z
--## Giving Z a commutative ring structure

def zero : Z := ⟦(0, 0)⟧
def one : Z := ⟦(1, 0)⟧


instance : has_zero Z := ⟨zero⟩
instance : has_one Z := ⟨one⟩

-- let's start to train the simplifier
@[simp] lemma zero_def : (0 : Z) = ⟦(0, 0)⟧ := rfl -- works
@[simp] lemma one_def : (1 : Z) = ⟦(1, 0)⟧ := rfl

--## Addition
def add_aux (ab cd : N2) : Z := ⟦(ab.1 + cd.1, ab.2 + cd.2)⟧

@[simp] lemma add_aux_def (ab cd : N2) :
  add_aux ab cd = ⟦(ab.1 + cd.1, ab.2 + cd.2)⟧ :=rfl

def add : Z → Z → Z := quotient.lift₂ add_aux sorry


instance : has_add Z := ⟨add⟩

-- train the simplifier, because we have some axioms to prove about `+`
@[simp] lemma add_def (a b c d : ℕ) :
  (⟦(a, b)⟧ + ⟦(c, d)⟧ : Z) = ⟦(a+c, b+d)⟧ := rfl

-- THIS IS THE STUFF I ADDED
-- I don't understand why has_add seemed to work but my has_le didn't.

def le_aux (ab cd : N2) : Prop :=
  (ab.fst + cd.snd) ≤ (cd.fst + ab.snd)

lemma le_aux_def (a0 a1 b0 b1: ℕ) :
  le_aux (a0, a1) (b0, b1) ↔ (a0 + b1) ≤ (b0 + a1) := by refl


def le : Z → Z → Prop := quotient.lift₂ le_aux sorry


instance : has_le Z := ⟨le⟩

@[simp] lemma le_def (a b c d : ℕ) :
  (⟦(a,b)⟧ : Z) ≤  (⟦(c,d)⟧ : Z) ↔ (a + d = b + c) := rfl


end Z

Lean tells me that it

failed to synthesize type class instance for
 a b c d : ℕ
 ⊢ has_le (quotient N2.setoid) (lean-checker)

on the le_def line. Any help will be appreciated. Thanks.

[kvanvels]

I am wondering if quotient.lift is inappropriate since the "return value" of the function is a proposition and not element of Z.

[Yaël Dillies]

It's because it interprets ⟦(a,b)⟧ as having type quotient N2.setoid, not ℤ. Those are definitionally equal, but not syntactically so, and that's what typeclass inference needs. One solution is to define a specialisation of quotient.mk to your ℤ.

[kvanvels]

I thought that the the : Z made it into an element of Z. I honestly don't know what you it would mean to define a specialization of quotient.mk. Any pointers/links would be appreciated.

I just checked, and lean has no problem if I tell it that Z.zero <= Z.one. So what you told me makes sense. Thanks for the response.

[Yaël Dillies]

It's because a type-ascription doesn't actually mean "Make the type be this" but rather "Check that this is defeq to the type you found". And here indeed the type it found is defeq to ℤ.

[Yaël Dillies]

What I'm talking about is

def mk : ℕ × ℕ → ℤ := quotient.mk

[kvanvels]

Thanks for the response. I will post more when I find out if I can get this to work.

[Damiano Testa]

As Yaël mentioned, type-ascription is more of a suggestion to Lean. If you really want to force the type, a common trick is to use (id a : α). Sticking the identity in guarantees (I think) that the type will be α.

[kvanvels]

I think the (id a : \alpha) trick is working. Thank you.

[Yaël Dillies]

You can also use show α, from a, which is a macro that basically unfolds to the id trick.

[Yaël Dillies]

The problem is that this changes the syntactic form of your lemma, which is undesirable for rewriting.

[kvanvels]

I was just wondering about that the fact that. I hope the addition of (id) wont till be a problem. Like you said, I need to use this for rewriting. Any ideas on why the other operations worked? I wonder if the return type helped it figure things out.

I will post more if I have more questions. Thank you.

[Yaël Dillies]

Yes exactly, the return type is enough for Lean to infer what you actually mean. This is not the case when you only have type-ascriptions.

[kvanvels]

Yeah, it isn't working with the id's. Is there any way i could do Z.le or something like Z.operator<= like in C++? By the way, I didn't get very far with the quotient.mk idea very far.

[Yaël Dillies]

Define def mk : ℕ × ℕ → ℤ := quotient.mk and use it instead of the square brackets notation.

[kvanvels]

It works as a theorem/lemma, but I can't use it to rewrite terms in other proofs. Maybe I could to another level and have a theorem/lemma to write things with brackets in terms of the mk.

[kvanvels]

THANK YOU. I got it to work, using an extra level (another theorem to transform mk's to square bracket terms). I really appreciate the help.

[kvanvels]

I turned on a bunch of "messages" (the pp.universes, pp.implicit ,etc. switches ) and was able to figure out that that the $\le$ sign I needed can be called by the incantation @has_le.le Z Z.has_le so I didn't need to use the idea of (that worked great) of the quotient.mk. I suppose I could run into problems later from this hack, but I am just trying to learn the library. Again, thanks for your help.