0
$\begingroup$

I am trying to create an instance of TotalBLE for my comparison function.

import Std.Classes.Order

-- BEGIN: no need to read, it is just here for completion sake

inductive Desc where
  | intro
    (name : String)
    (hash : UInt64)
    (params : List Desc)
    (reader: Bool)
  : Desc
  deriving Repr

def cmp (x y: Desc): Ordering :=
  match x with
  | ⟨xname, xhash, xparams, _⟩ =>
    match y with
    | ⟨yname, yhash, yparams, _⟩ =>
      let chash := compare xhash yhash
      if chash != Ordering.eq
      then chash
      else
        let cname := compare xname yname
        if cname != Ordering.eq
        then cname
        else cmps xparams yparams
where cmps (xs ys : List Desc) : Ordering :=
  match xs, ys with
  | x::xs, y::ys =>
    let r := cmp x y
    if r != Ordering.eq
    then r
    else cmps xs ys
  | _, _ => Ordering.eq

instance : Hashable Desc where
  hash x := get_hash x

instance : Ord Desc where
  compare x y := cmp x y

def le (x y: Desc): Bool :=
  match cmp x y with
  | Ordering.lt => true
  | Ordering.eq => true
  | _ => false

-- END: no need to read, it is just here for completion sake

theorem le_total: ∀ (x y: Desc),
  le x y ∨ le y x = true := by
  sorry

instance : Std.TotalBLE le where
  total x y := le_total x y

But I get a type error

type mismatch
  fun x y => le_total x y
has type
  ∀ (x y : Desc), le x y = true ∨ le y x = true : Prop
but is expected to have type
  le a✝ b✝ = true ∨ le b✝ a✝ = true : Prop
the following variables have been introduced by the implicit lambda feature
  a✝ : Desc
  b✝ : Desc
you can disable implict lambdas using `@` or writing a lambda expression with `{}` or `[]` binder annotations.Lean 4

I have tried writing

instance : Std.TotalBLE le where
  @total x y := le_total x y

But then I get a syntax error

Does anyone have any ideas of how to write the syntax, so that I can work on the proof later?

Note: this is not an ask to write the proof.

$\endgroup$
1
  • $\begingroup$ Btw I have the same issue with Std.TransCmp $\endgroup$ Commented Mar 10, 2023 at 15:43

2 Answers 2

2
$\begingroup$

I agree this is strange (possibly even a bug I'm not sure) but this works:

instance : Std.TotalBLE le where
  total := le_total _ _
$\endgroup$
2
  • $\begingroup$ Yeah it does feel like a bug, but this works until it is fixed, thank you :) $\endgroup$ Commented Mar 12, 2023 at 11:34
  • $\begingroup$ In the end I got the following to work ``` theorem le_total : ∀ (x y: Desc), le x y = true ∨ le y x = true := by sorry instance : Std.TotalBLE le where total x y := le_total x y theorem cmp_trans : ∀ (x y: Desc), cmp x y ≠ .gt → cmp y z ≠ .gt → cmp x z ≠ .gt := by sorry instance : Std.TransCmp cmp where le_trans := cmp_trans _ _ ``` I do think there is a bug $\endgroup$ Commented Mar 12, 2023 at 11:41
0
$\begingroup$

I don't know why it wasn't working before, but now I am able to create those instances consistently

theorem le_total : ∀ (x y: Desc),
  le x y = true ∨ le y x = true := by
  sorry

instance : Std.TotalBLE le where
  total x y := le_total x y

theorem cmp_trans : ∀ {x y z: Desc},
  cmp x y ≠ .gt → cmp y z ≠ .gt → cmp x z ≠ .gt := by
  sorry

instance : Std.TransCmp cmp where
  le_trans cxy cyz := cmp_trans cxy cyz
```
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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