Strange metavariable error when using rewrite rules

Stream: new members

[Becky T]

Greetings:

With the following code:

import Mathlib.Init

universe u

axiom Bird : Type u
axiom response : Bird → Bird → Bird
infixl:100 " ◁ " => response
axiom compose : Bird → Bird → Bird
infixr:80 " ∘ " => compose
axiom composition (A B : Bird) : ∀ {x : Bird}, (A ∘ B) ◁ x = A ◁ (B ◁ x)


namespace Combinator





  axiom K : Bird
  axiom K.call : ∀ (x y : Bird), (K ◁ x) ◁ y = x

  axiom I : Bird
  axiom I.call : ∀ (x : Bird), (I ◁ x) = x

  axiom B : Bird
  axiom B.call : ∀ (x y z : Bird), (((B ◁ x) ◁ y) ◁ z) = x ◁ (y ◁ z)

  axiom S : Bird
  axiom S.call : ∀ (x y z : Bird), (((S ◁ x) ◁ y) ◁ z) = (x ◁ z) ◁ (y ◁ z)

  axiom C : Bird
  axiom C.call : ∀ (x y z : Bird), (((C ◁ x) ◁ y) ◁ z) =  (x ◁ z) ◁ y

  axiom W : Bird
  axiom W.call : ∀ (x y : Bird), (W ◁ x) ◁ y = (x ◁ y) ◁ y

end Combinator

open Combinator

axiom S' : Bird
axiom S'.call :  ∀ (x y z : Bird), (((S' ◁ x) ◁ y) ◁ z) = (x ◁ (y ◁ z)) ◁ z


axiom c1 : Bird
axiom c1.call :  ∀ (x y z : Bird), (((c1 ◁ x) ◁ y) ◁ z) = ((((B ◁ (B ◁ W)) ◁ B) ◁ x) ◁ y) ◁ z

theorem c1_correct : ∀ x y z : Bird, S' ◁ x ◁ y ◁ z = c1 ◁ x ◁ y ◁ z := by
intros x y z;
rw [S'.call];
rw [c1.call];
rw [B.call];
rw [B.call];
rw [W.call];
rw [B.call];

I end up with the following error message:

declaration 'c1_correct' contains universe level metavariables at the expression
  response.{?u.3995, u_3, u_4} (response.{u_1, ?u.3991, ?u.3995} x (response.{u_2, u_3, ?u.3991} y z)) z
in the declaration body

fun x y z ↦
    Eq.mpr
      (id
        (congrArg (fun _a ↦ _a = c1 ◁ x ◁ y ◁ z) (S'.call.{u_1, u_2, u_3, u_4, u_5, u_6, u_7, ?u.3995, ?u.3991} x y z)))
      (Eq.mpr
        (id
          (congrArg
            (fun _a ↦
              response.{?u.3995, u_3, u_4} (response.{u_1, ?u.3991, ?u.3995} x (response.{u_2, u_3, ?u.3991} y z)) z =
                _a)
            (c1.call.{u_1, ?u.3893, ?u.3892, ?u.3992, ?u.3891, ?u.3931, ?u.3930, ?u.3963, u_2, u_3, u_4, u_8, u_9, u_10,
                ?u.3964, ?u.3932}
              x y z)))
        (Eq.mpr
          (id
            (congrArg
              (fun (_a : Bird.{?u.3932}) ↦
                response.{?u.3995, u_3, u_4} (response.{u_1, ?u.3991, ?u.3995} x (response.{u_2, u_3, ?u.3991} y z)) z =
                  response.{?u.3964, u_3, u_4} (response.{?u.3932, u_2, ?u.3964} _a y) z)
              (B.call.{?u.3931, ?u.3992, u_1, ?u.3932, ?u.3893, ?u.3892, ?u.3891, ?u.3993}
                (response.{?u.3930, ?u.3963, ?u.3931} B.{?u.3930} W.{?u.3963}) B.{?u.3992} x)))
          (Eq.mpr
            (id
              (congrArg
                (fun (_a : Bird.{?u.3964}) ↦
                  response.{?u.3995, u_3, u_4} (response.{u_1, ?u.3991, ?u.3995} x (response.{u_2, u_3, ?u.3991} y z))
                      z =
                    response.{?u.3964, u_3, u_4} _a z)
                (B.call.{?u.3963, ?u.3993, u_2, ?u.3964, ?u.3932, ?u.3931, ?u.3930, ?u.3994} W.{?u.3963}
                  (response.{?u.3992, u_1, ?u.3993} B.{?u.3992} x) y)))
            (Eq.mpr
              (id
                (congrArg
                  (fun _a ↦
                    response.{?u.3995, u_3, u_4} (response.{u_1, ?u.3991, ?u.3995} x (response.{u_2, u_3, ?u.3991} y z))
                        z =
                      _a)
                  (W.call.{?u.3994, u_3, u_4, ?u.3964, ?u.3963, ?u.3995}
                    (response.{?u.3993, u_2, ?u.3994} (response.{?u.3992, u_1, ?u.3993} B.{?u.3992} x) y) z)))
              (Eq.mpr
                (id
                  (congrArg
                    (fun (_a : Bird.{?u.3995}) ↦
                      response.{?u.3995, u_3, u_4}
                          (response.{u_1, ?u.3991, ?u.3995} x (response.{u_2, u_3, ?u.3991} y z)) z =
                        response.{?u.3995, u_3, u_4} _a z)
                    (B.call.{u_1, u_2, u_3, ?u.3995, ?u.3994, ?u.3993, ?u.3992, ?u.3991} x y z)))
                (Eq.refl
                  (response.{?u.3995, u_3, u_4} (response.{u_1, ?u.3991, ?u.3995} x (response.{u_2, u_3, ?u.3991} y z))
                    z)))))))

I am not sure how to start debugging the proof term, so any advice would be very much appreciated!

[Kyle Miller]

when you define

axiom Bird : Type u

this defines a whose family of Bird constants, one for every universe level u (full notation: Bird.{u}). The u is not a fixed constant. Whenever you mention Bird without the full notation, Lean interprets it as Bird.{_}, using a fresh universe level metavariable at _. Lean requires that universe level metavariables all be solved for.

The easiest fix is to go back to the axiom and instead define

axiom Bird : Type

This creates one type Bird in only the Type universe. There are no universe level metavariables that need to be solved for.

[Becky T]

Thank you! I presume that means that the universe declaration is not needed? I presume Lean has some sort of built-in universe polymorphism that deals with this.

[Kyle Miller]

The function of universe u is to make it legal to refer to u and have it automatically become a universe parameter for the declaration.

Doing

universe u
axiom Bird : Type u
```
is the same as
```
axiom Bird.{u} : Type u
```
The key thing to realize, what I was saying about how `Bird` by itself in your code means `Bird.{_}`, is that `u` is not fixed for the whole module. Each individual use of `Bird` can have its own `u` so to speak. You would need to consistently write `Bird.{u}` yourself for every `Bird` to be in the same universe.

[Kyle Miller]

Becky T said:

Lean has some sort of built-in universe polymorphism that deals with this.

My suggestion to remove u in Type u is to make it non-polymorphic.

[Edward van de Meent]

if you want to say "let Bird be some element of Type u", use variables instead

[Edward van de Meent]

that will "fix" the universe level (sort of)

[Kyle Miller]

Won't that cause every combinator to be a function of Bird, which would mean needing to pass Bird in as an argument?

[Edward van de Meent]

:hmm: i guess you could bundle it all in an instance?

[Edward van de Meent]

something like

import Mathlib.Init
set_option autoImplicit false

universe u
class Forest (Bird : Type u) where
  response : Bird → Bird → Bird
  compose : Bird → Bird → Bird
  composition (a b : Bird) : ∀ x : Bird, response (compose a b) x = response a (response b x)

infixl:100 " ◁ " => Forest.response

infixr:80 " ∘ " => Forest.compose

variable {Bird : Type u} [Forest Bird]
-- whatever stuff you want to do