Reflexive product order

Stream: new members

[YurySerdyuk]

What is wrong with the syntax of my code :

@[class] structure refl_order (A : Type) extends has_le A :=
(refl : ∀ a, le a a)

def prod_order {A B : Type} (o₁ : A → A → Prop) (o₂ : B → B → Prop) (s : A × B) (t : A × B) :=
o₁ (s.1) (t.1) ∧ o₂ (s.2) (t.2)

instance refl_prod {A B: Type} [o₁ : refl_order A] [o₂ : refl_order B] : refl_order (A × B) :=
let op : A × B → A × B → Prop := prod_order o₁.le o₂.le in
have refl : ∀ p : A × B, op p p, by intro; apply and.intro; repeat {apply refl_order.refl},
show _, from refl_order.mk (has_le.mk op) refl

type mismatch at application
{to_has_le := ?m_2, refl := {le := op}}
term
{le := op}
has type
has_le (A × B) : Type
but is expected to have type
∀ (a : ?m_1), a ≤ a : Prop

error message
too many arguments

[Bolton Bailey]

Here is the code with #backticks

@[class] structure refl_order (A : Type) extends has_le A :=
(refl : ∀ a, le a a)

def prod_order {A B : Type} (o₁ : A → A → Prop) (o₂ : B → B → Prop) (s : A × B) (t : A × B) :=
o₁ (s.1) (t.1) ∧ o₂ (s.2) (t.2)

instance refl_prod {A B: Type} [o₁ : refl_order A] [o₂ : refl_order B] : refl_order (A × B) :=
let op : A × B → A × B → Prop := prod_order o₁.le o₂.le in
have refl : ∀ p : A × B, op p p, by intro; apply and.intro; repeat {apply refl_order.refl},
show _, from refl_order.mk (has_le.mk op) refl

[Bolton Bailey]

It seems refl_order.mk is supposed to only have one explicit argument, of type (∀ (a : A), a ≤ a), but this code gives two arguments, (has_le.mk op) and refl

[Bolton Bailey]

I see the issue - you included the (has_le.mk op) as one of the arguments, but this was supposed to be implicit, so Lean got confused.

[Bolton Bailey]

This fixes it @refl_order.mk _ (has_le.mk op) refl. The @ tells Lean to treat all implicit arguments as explicit, after which there are three arguments, and the _ tells Lean to infer the first one.

[Bolton Bailey]

@YurySerdyuk