1
$\begingroup$

In Unclarity about Preorder class in Lean4 I asked why the third and fourth field (lt and lt_iff_le_not_le) in the definition of MyPreorder below would both be necessary, as one follows from the other as far as I can see. The answer was that this happens because there is no clear preference over defining LE or LT - hence the fourth line - and that the third line is there for convenience, as a default definition.

However, if I next want to build a product preorder, it seems that I do need to repeat the definition of lt, even though it was expected to be a default? At least, if I leave it out, the assumptions at the end of the proof do not get resolved properly anymore. Notably, Lean does not ask me to define lt, it just doesn't recognize that I mean the default definition aparently.

class MyPreorder.{u} (α : Type u) extends LE α, LT α :=
(le_refl : ∀ a : α, a ≤ a)
(le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c)
(lt := λ a b => a ≤ b ∧ ¬ b ≤ a) -- default definition introduced for convenience
(lt_iff_le_not_le : ∀ a b : α, a < b ↔ (a ≤ b ∧ ¬ b ≤ a)) -- expected relation between lt and le

instance MyProd_Preorder [P : MyPreorder α] [Q : MyPreorder β] : MyPreorder (Prod α β) where
      le := fun x y => x.fst ≤ y.fst ∧ x.snd ≤ y.snd
      lt := λ a b => a ≤ b ∧ ¬ b ≤ a -- WHY DO I HAVE TO REPEAT THE DEFAULT ?
      le_refl := by 
        intros
        constructor
        . apply P.le_refl
        . apply Q.le_refl        
      le_trans := by
        intros x y z
        intros a b
        have ineq1 := And.left a
        have ineq2 := And.right a
        have ineq3 := And.left b
        have ineq4 := And.right b
        constructor
        . apply P.le_trans _ _ _ ineq1 ineq3
        . apply Q.le_trans _ _ _ ineq2 ineq4
      lt_iff_le_not_le := by
         intros x y         
         constructor         
         . intro
           assumption
         . intro         
           assumption

I'm not entirely sure however whether this is really the problem, or it's just my inability in Lean. A related attempt to just derive lt_iff_le_not_le from the definition of lt also fails. So perhaps I'm doing something different wrong...

class AnotherPreorder.{u} (α : Type u) extends LE α, LT α :=
(le_refl : ∀ a : α, a ≤ a)
(le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c)
(lt := λ a b => a ≤ b ∧ ¬ b ≤ a) -- default definition introduced for convenience
-- I've left out the iff relation from this definition, in order to try to derive it...

example (α : Type u) [P : AnotherPreorder α] : ∀ a b : α, a < b ↔ (a ≤ b ∧ ¬ b ≤ a) := by 
   intros a b
   constructor
   . intro
     assumption -- these fail miserably, and I don't understand why, as they do work in the other example...
   . intro    
     assumption -- these fail miserably, and I don't understand why, as they do work in the other example...
```
New contributor
Pieter Cuijpers is a new contributor to this site. Take care in asking for clarification, commenting, and answering. Check out our Code of Conduct.
$\endgroup$
2
  • $\begingroup$ You first example isn't type checking for me. Are you sure it is correct? $\endgroup$
    – Jason Rute
    Sep 22 at 14:37
  • $\begingroup$ Ah, you are right, when I run it in complete isolation the example doesn't type check. I've by now also figured out a few steps towards my solution because of this. $\endgroup$ Sep 22 at 15:22

1 Answer 1

1
$\begingroup$

Thanks to Jason Rute his comment, I think I can now answer my own question partially. I figured out that my example does not typecheck in isolation, whereas it did in my sandbox file because there was an import that defined instProdLE under the hood. My definition of lt in the MyProd_Preorder took that instance in order to determine the type of the definition.

That also explains why I needed to explicitly define lt in the first place. Although in Unclarity about Preorder class in Lean4 it was mentioned that the definition of MyPreorder provides a default, that is not the default that is taken when I leave the definition of lt implicit. It turns out that, in the Lean4 core there is a definition of instLTProd which takes preference. That definition is subtly different.

Which only leaves me with the question, is there a tactic for unrolling definitions? I.e. if I've defined lt := fun x y => x something y and the state in my proof says x < y, how can I turn it into an explicit x something y?

New contributor
Pieter Cuijpers is a new contributor to this site. Take care in asking for clarification, commenting, and answering. Check out our Code of Conduct.
$\endgroup$
4
  • $\begingroup$ Can you ask about the unfolding as a different question? $\endgroup$
    – Jason Rute
    Sep 22 at 16:38
  • $\begingroup$ Actually, for the last question do you want this tactic to solve theorems or just to inspect the state to know what instances are used? For the later, see proofassistants.stackexchange.com/questions/1672/… $\endgroup$
    – Jason Rute
    Sep 22 at 17:33
  • $\begingroup$ Also, you should generally try to avoid getting yourself into situations where you are defining two instances for the same thing. This is called a diamond and it creates problems, especially when the instances are not definitionally equal (and worse when they are totally different as in this case). In this case you were defining two instances of < for (α × β). $\endgroup$
    – Jason Rute
    Sep 22 at 17:35
  • $\begingroup$ Thanks for the insights. Indeed, I would like to avoid defining two instances for the same thing. So I'm not entirely happy with the amount of "predefined" notations in Lean4, simply because it forces me to overload them and then later run into trouble interpreting whether what I wrote down is actually what I mean. $\endgroup$ Sep 23 at 15:17

Your Answer

Pieter Cuijpers is a new contributor. Be nice, and check out our Code of Conduct.

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.