failed to synthesize Trans instance

Stream: lean4

[Elisabeth Bonnevier]

I have my own natural numbers MyNat (with addition) and have created an instance of LE MyNat and instances Trans le le le and Trans le (· = ·) le. But the code

theorem le_le_add {k l m n : MyNat} (p : k ≤ l) (q : m ≤ n) : k + m ≤ l + n :=
  calc
    k + m ≤ l + m := le_add p
    l + m = m + l := comm_add
    m + l ≤ n + l := le_add q
    n + l = l + n := comm_add

produces the error message "invalid 'calc' step, failed to synthesize Trans instance Trans LE.le LE.le ?m.551" at the line m + l ≤ n + l := le_add q. The code works if I replace ≤ with MyNat.le in the calculation steps. How can I fix this so that I don't have to write MyNat.le but can use ≤?

[Arthur Paulino]

Can you post a #mwe please?

[Elisabeth Bonnevier]

inductive MyNat where
  | zero : MyNat
  | succ : MyNat → MyNat
open MyNat

namespace MyNat

def add (m n : MyNat) : MyNat :=
  match n with
  | zero   => m
  | succ n => succ (add m n)

instance : Add MyNat where
  add := add

theorem add_zero_left (n : MyNat) : zero + n = n := by
  induction n with
  | zero      => rfl
  | succ n ih =>
    show succ (zero + n) = succ n
    rw [ih]

theorem add_succ_left (m n : MyNat) : succ m + n = succ (m + n) := by
  induction n with
  | zero      => rfl
  | succ n ih =>
    show succ (succ m + n) = succ (succ (m + n))
    rw [ih]

theorem comm_add {m n : MyNat} : m + n = n + m := by
  induction m with
  | zero =>
    show zero + n = n
    apply add_zero_left
  | succ m ih =>
    show succ m + n = succ (n + m)
    rw [← ih]
    apply add_succ_left

inductive le : MyNat → MyNat → Prop
  | zero_le : {n : MyNat} → le zero n
  | succ_le : {m n : MyNat} → le m n → le (succ m) (succ n)

instance : LE MyNat where
  le := le

theorem trans_le {k l m : MyNat} : k ≤ l → l ≤ m → k ≤ m := by
  revert l m
  induction k with
  | zero =>
    intros
    constructor
  | succ k ihk =>
    intro l
    match l with
    | zero =>
      intros
      contradiction
    | succ l =>
      intros m p
      cases p with
      | succ_le p' =>
        match m with
        | zero =>
          intro _
          contradiction
        | succ m =>
          intro q
          cases q with
          | succ_le q' =>
            apply le.succ_le
            apply ihk
            . exact p'
            . exact q'

instance : Trans MyNat.le MyNat.le MyNat.le where
  trans := trans_le

theorem trans_le_eq {k l m : MyNat} : k ≤ l → l = m → k ≤ m := by
  intros p h
  rw [← h]
  assumption

instance : Trans le Eq le where
  trans := trans_le_eq

theorem le_add {k l m : MyNat} : k ≤ l → k + m ≤ l + m := by
  revert k l
  induction m with
  | zero => exact id
  | succ m ih =>
    intros
    apply le.succ_le
    apply ih
    assumption

theorem le_le_add {k l m n : MyNat} (p : k ≤ l) (q : m ≤ n) : k + m ≤ l + n :=
  calc
    -- MyNat.le (k + m) (l + m) := le_add p  --(this works)
    k + m ≤ l + m := le_add p
    l + m = m + l := comm_add
    -- MyNat.le (m + l) (n + l) := le_add q  --(this works)
    m + l ≤ n + l := le_add q -- error message here
    n + l = l + n := comm_add

end MyNat

[Ruben Van de Velde]

I don't think you're supposed to repeat the terms, from the second line you should start with _ =

[Elisabeth Bonnevier]

Ruben Van de Velde said:

I don't think you're supposed to repeat the terms, from the second line you should start with _ =

Still the same error message :cry:

[Alistair Tucker]

It works with your Trans instance parametrised by LE.le : MyNat → MyNat → Prop instead of MyNat.le.

[Elisabeth Bonnevier]

Alistair Tucker said:

It works with your Trans instance parametrised by LE.le : MyNat → MyNat → Prop instead of MyNat.le.

Yes, that works! :+1: