Stream: Coq users

Topic: Need eq to unfold?


view this post on Zulip Shea Levy (Oct 15 2020 at 20:41):

I have a use case where I need to do something like

match (eq_refl : foo = bar) in _ = bar return bar with
| eq_refl => my_foo
end

to get a term to typecheck (my_foo alone fails). Is this a bug? I can try to make a minimal example but this seems really odd that eq_refl is typechecking but I can't just use the term directly.

view this post on Zulip Gaëtan Gilbert (Oct 15 2020 at 20:49):

weird
what about (my_foo : foo) : bar and my_foo : bar?

view this post on Zulip Shea Levy (Oct 15 2020 at 21:14):

First one works!

view this post on Zulip Shea Levy (Oct 15 2020 at 21:14):

Oh so does second one, I thought I'd tried that...

view this post on Zulip Shea Levy (Oct 15 2020 at 21:15):

But without the cast it fails

view this post on Zulip Gaëtan Gilbert (Oct 15 2020 at 21:18):

what failure?
are you just doing Check my_foo or something more complicated?

view this post on Zulip Shea Levy (Oct 15 2020 at 21:21):

Require Import Unicode.Utf8.

Inductive composition_endpoints : nat  Type :=
| both_endpoints_same : Type  composition_endpoints 0
| endpoints_are :  {n}, Type  Type  composition_endpoints (S n).

Definition compose_type n (ce : composition_endpoints n) :=
  let
    (dom, cod) := match ce with
                  | both_endpoints_same A => (A, A)
                  | endpoints_are A B => (A, B)
                  end
  in (fix compose_type' n dom' :=
        match n with
        | 0 => dom  dom'
        | S n' =>
          let
            go cod := (dom'  cod)  compose_type' n' cod
          in match n' with
             | 0 => go cod
             | _ =>  cod, go cod
             end
        end
     ) n dom.

Fixpoint compose n :  ce, compose_type n ce :=
  match n with
  | 0 =>
    λ ce,
    match ce with
    | both_endpoints_same T =>
      ((λ (x : T), x) : compose_type 0 (both_endpoints_same T))
    end
  | S n' => _
  end.

If I remove the cast near the bottom (but keep the fully typed binding on the lambda) I get:

Error: The type of this term is a product while it is expected to be
(compose_type ?n0@{y0:=0} ?c@{y0:=0; c0:=both_endpoints_same T}).

view this post on Zulip Paolo Giarrusso (Oct 15 2020 at 22:03):

The errore seems accurate? compose_type n isn't definitionally a product type.

view this post on Zulip Paolo Giarrusso (Oct 15 2020 at 22:04):

That is, if n is a Coq variable.

view this post on Zulip Paolo Giarrusso (Oct 15 2020 at 22:05):

If you apply to a number starting with a constructor, then it's probably a product again (and clearly so for 0)

view this post on Zulip Shea Levy (Oct 15 2020 at 22:24):

But in context I know n is 0, it's instantiated as such.

view this post on Zulip Jasper Hugunin (Oct 15 2020 at 22:28):

If you annotate match n with as match n return forall ce, compose_type n ce with, does it go through? Or do you need to also add match ce return compose_type 0 ce with?

view this post on Zulip Paolo Giarrusso (Oct 15 2020 at 22:43):

@Shea Levy not necessarily, without full GADT semantics or the appropriate return type annotation for match: match n as n0 return ... compose_type n0 ...

view this post on Zulip Paolo Giarrusso (Oct 15 2020 at 22:46):

Stronger inference algorithms exist, including in Equations, but it's not unusual to need annotations in such cases (even simpler ones)

view this post on Zulip Paolo Giarrusso (Oct 15 2020 at 22:48):

In your case, Coq knows that it must substitute 0 for y0 in ?n0, but it hasn't yet decided what to unify n0 with.

view this post on Zulip Shea Levy (Oct 15 2020 at 23:17):

Hmm this worked (with the explicit idProp line for the other ctor):

    match ce as ce' in composition_endpoints n' return match n' with
                                                       | 0 => compose_type 0
                                                       | S _ => λ ce, IDProp
                                                       end ce' with

Last updated: Feb 04 2023 at 22:29 UTC