Beta-reduction not doing what I expect

[mikeshulman]

The following code fails:

constant ty : Type
constant ( |= ) : ty → ty → Type
constant id : Π (p : ty), p |= p

constant tm : ty → Type
constant cell : Π (p : ty), tm p → tm p → Type

constant trans : Π (p q : ty), (p |= q) → tm q → tm p
constant trans_id : Π (p : ty) (mu : tm p), trans p p (id p) mu ≡ mu
now betas = add_beta trans_id

constant maphom : Π (p : ty) (q : tm p → ty) (mu mu' : tm p),
  (cell p mu  mu') → (q mu |= q mu')

constant maphom_const : Π (p q : ty) (mu mu' : tm p) (s : cell p mu mu'),
  maphom p (λ _ : tm p, q) mu mu' s ≡ id q
now betas = add_beta maphom_const

let doesnt_work =
  assume p : ty in
  assume q : ty in
  assume mu : tm p in
  assume mu' : tm p in
  assume nu : tm p → tm q in
  assume s : cell p mu mu' in
  refl (trans q q (id q) (nu mu'))
  : (trans ((λ _ : tm p, q) mu) ((λ _ : tm p, q) mu') (maphom p (λ _ : tm p, q) mu mu' s) (nu mu'))
    ≡ (trans q q (id q) (nu mu'))

with the error "failed to check that ... and ... are equal". However, they are in fact equal, as I can verify with some manual help:

let works =
  assume p : ty in
  assume q : ty in
  assume mu : tm p in
  assume mu' : tm p in
  assume nu : tm p → tm q in
  assume s : cell p mu mu' in
  let test = refl (trans q q (id q)) :
    (trans ((λ _ : tm p, q) mu) ((λ _ : tm p, q) mu') (maphom p (λ _ : tm p, q) mu mu' s))
    ≡ (trans q q (id q)) in
  assume x : tm q in
  assume qq : ty in
    let be1 = (beta_step x (refl (tm p)) (refl ty) q mu) in
    let be1' = (beta_step x (refl (tm p)) (refl ty) q mu') in
    let be1a = (congr_apply qq (refl tm) be1 (refl ty) (refl Type)) in
    let be1a' = (congr_apply qq (refl tm) be1' (refl ty) (refl Type)) in
    congr_apply x test (refl (nu mu' : tm ((λ _ : tm p, q) mu'))) be1a' be1a
      : (trans ((λ _ : tm p, q) mu) ((λ _ : tm p, q) mu') (maphom p (λ _ : tm p, q) mu mu' s) (nu mu'))
      ≡ (trans q q (id q) (nu mu'))

Now I know that equality in general is undecidable, but I'm surprised that the standard beta-reduction algorithm isn't able to check this equality. It gets almost all the way there (the equality test), while the rest is just a couple of beta_steps and some congr_applys, which seems like it ought to be doable automatically. Are there any extra hints I can give to the algorithm that will enable it to check this equality?

[SkySkimmer]

You need to add reducing hints so that when it's looking at foo bar it reduces bar before checking if some beta rule applies. Something like

constant ty : Type
constant ( |= ) : ty → ty → Type
constant id : Π (p : ty), p |= p

constant tm : ty → Type
constant cell : Π (p : ty), tm p → tm p → Type

constant trans : Π (p q : ty), (p |= q) → tm q → tm p
constant trans_id : Π (p : ty) (mu : tm p), trans p p (id p) mu ≡ mu
now betas = add_beta trans_id

constant maphom : Π (p : ty) (q : tm p → ty) (mu mu' : tm p),
  (cell p mu  mu') → (q mu |= q mu')

constant maphom_const : Π (p q : ty) (mu mu' : tm p) (s : cell p mu mu'),
  maphom p (λ _ : tm p, q) mu mu' s ≡ id q
now betas = add_beta maphom_const

now reducing = add_reducing maphom [eager, eager]
now reducing = add_reducing trans [eager,eager,eager]

constant p : ty
constant q : ty
constant mu : tm p
constant mu' : tm p
constant nu : tm p -> tm q
constant s : cell p mu mu'

let right = (trans ((λ _ : tm p, q) mu) ((λ _ : tm p, q) mu') (maphom p (λ _ : tm p, q) mu mu' s) (nu mu'))
let e1 = whnf right

let right2 = match e1 with |- _ : _ == ?x => x end

do right2
(* no reducing:
⊢ trans ((λ (_ : tm p), q) mu) ((λ (_ : tm p), q) mu') (maphom p
    (λ (_ : tm p), q) mu mu' s) (nu mu')
  : tm ((λ (_ : tm p), q) mu)

reducing:
 ⊢ trans q q (id q) (nu mu') : tm ((λ (_ : tm p), q) mu) *)

This still isn't quite enough for some reason though, I guess the invisible annotations make it not match trans_id.

[mikeshulman]

What do you mean by "invisible annotations"? Is there something I can do to make it match?

[SkySkimmer]

Each application node is annotated with the domain and codomain of the function. An applied lambda must have matching annotations to beta reduce. (the application being well typed does not imply that the annotations are the same because we don't have pi injectivity)

Is there something I can do to make it match?

It's been a while since I touched andromeda so I don't remember how to make things work / what things can be made to work.

[mikeshulman]

Ah right. Is there a way to display those annotations?

I did notice that nothing has been done on andromeda for a year. Have you all given up on it?