The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I think it's a bug with universes.  I've reported it at https://github.com/HoTT/coq/issues/52.

-Jason

On Wednesday, July 31, 2013, Jason Gross wrote:

Hi,

I have a goal where the following succeed:

    lazymatch goal with |- ?f ?x0 ?x1 ?x2 ?x3 ?x4 ?x5 = ?g ?x0 ?x1 ?x2 ?x3 ?x4' ?x5

    => let check := constr:(eq_refl : f = g) in idtac

    end.

    lazymatch goal with |- ?f ?x0 ?x1 ?x2 ?x3 ?x4 ?x5 = ?g ?x0 ?x1 ?x2 ?x3 ?x4' ?x5

    => change f with g

    end.

    lazymatch goal with |- ?f ?x0 ?x1 ?x2 ?x3 ?x4 ?x5 = ?g ?x0 ?x1 ?x2 ?x3 ?x4' ?x5

    => let F := eval hnf in f in let G := eval hnf in g in constr_eq F G

    end.

    lazymatch goal with |- ?f ?x0 ?x1 ?x2 ?x3 ?x4 ?x5 = ?g ?x0 ?x1 ?x2 ?x3 ?x4' ?x5

    => pose Type as stupid;

      let F := eval cbv delta [stupid] in f in let G := eval cbv delta [stupid] in g in constr_eq F G

    end.

    lazymatch goal with |- ?f ?x0 ?x1 ?x2 ?x3 ?x4 ?x5 = ?g ?x0 ?x1 ?x2 ?x3 ?x4' ?x5

    => let T := type of f in let T' := type of g in constr_eq T T'

    end.

    lazymatch goal with |- ?f ?x0 ?x1 ?x2 ?x3 ?x4 ?x5 = ?g ?x0 ?x1 ?x2 ?x3 ?x4' ?x5

    => let F := constr:(fun _ : Set => f) in let G := constr:(fun _ : Set => g) in constr_eq F G

    end.

and the following fail:

    lazymatch goal with |- ?f ?x0 ?x1 ?x2 ?x3 ?x4 ?x5 = ?g ?x0 ?x1 ?x2 ?x3 ?x4' ?x5

    => constr_eq f g

    end.

    (* note the lack of [g] in the following match *)

    lazymatch goal with |- ?f ?x0 ?x1 ?x2 ?x3 ?x4 ?x5 = ?f ?x0 ?x1 ?x2 ?x3 ?x4' ?x5

    => idtac

    end.

note that [match goal with |- ?G => has_evar G end] fails, indicating that the problem is not evars.

Even more weirdly,

    lazymatch goal with |- ?f ?x0 ?x1 ?x2 ?x3 ?x4 ?x5 = ?f' ?x0 ?x1 ?x2 ?x3 ?x4' ?x5

    => let check := constr:(idpath : f = f') in idtac

    end.

    lazymatch goal with |- ?f ?x0 ?x1 ?x2 ?x3 ?x4 ?x5 = ?f' ?x0 ?x1 ?x2 ?x3 ?x4' ?x5

    => progress change f with f'

    end.

fails, but if I switch the order of the lazymatches, then it goes through!

What's going on here?  I strongly suspect that this is a bug.  (Also, what's kind of reduction does [cbv deta [foo] in bar] do when [foo] doesn't appear in [bar]?)

-Jason

P.S. The code I'm working with is available at https://github.com/JasonGross/HoTT-categories/blob/3a47db011ea7ff6f7a3fcb538fd9bcefbd6e4b0f/theories/Grothendieck/ToCat.v#L194.  It only runs on top of HoTT/coq, sorry.