Stream: Coq users

Topic: Convertability and Typing of Terms


view this post on Zulip Jacob Salzberg (Oct 30 2022 at 18:12):

Hi, I have two questions on convertibility.

1) Is there some sort of unification algorithm that tracks type level constraints? For example, when i try

Inductive eq2 {A : Type} (x : A) : A -> Prop := eq_refl : eq2 x x.
Theorem eq2_trans3 : forall x y z : Type, eq2 x y -> eq2 y z -> eq2 x z.
Proof.
  - intros A B C H1 H2.
    pattern H2.
    pattern H1.
    case H2.
    exact H1.
Defined.

It works, seemingly registering the type-level constraint B = C upon the application of H2.

2) What determines the convertibility of terms in the case of equality? For example

Screenshot-2022-10-30-141019.png

here somehow applying nb_seats across the equality preserves convertibility, because they use change.. I don't understand. I understand how applying nb_seats can preserve the equality by liebniz' definition of equality / that applying nb_seats results in the following equality; that said, I don't understand how you can convert the term including nb_seats that the two are equal, unless nb_seats is injective. (which it is in this case, but I assume that this is using convertability).

Thanks

view this post on Zulip Paolo Giarrusso (Oct 30 2022 at 18:51):

  1. this example does not use "type-level constraints", and B and C remain definitionally distinct as shown below. case H2. just modifies the goal by producing a dependent pattern match expression — how _that_ works is a more advanced question
    case H2.
    Fail Check (eq_refl _ : eq2 B C).
    Check (eq_refl _ : eq2 B B).
(*
The term "eq_refl B" has type "eq2 B B" while it is expected to have type
 "eq2 B C" (cannot unify "B" and "C").
eq_refl B : eq2 B B
     : eq2 B B
*)

view this post on Zulip Paolo Giarrusso (Oct 30 2022 at 18:53):

  1. Your snapshot is not self-contained, but it seems to only rely on nb_seats (bicycle x) being definitionally equal to x.

view this post on Zulip Paolo Giarrusso (Oct 30 2022 at 18:56):

At least, I'm inferring this to be the self-contained version:

Record B := bicycle { nb_seats : nat }.
Add Printing Constructor B.

Theorem bicycle_eq_seats :
  forall x1 y1 : nat, bicycle x1 = bicycle y1 -> x1 = y1.
Proof.
  intros x1 y1 H.
  change (nb_seats (bicycle x1) = nb_seats (bicycle y1)).
  rewrite H; trivial.
Qed.

view this post on Zulip Paolo Giarrusso (Oct 30 2022 at 18:58):

in particular, this is not applying nb_seats to the hypothesis bicycle x1 = bicycle y1.

view this post on Zulip Paolo Giarrusso (Oct 30 2022 at 19:00):

which I point out for clarity because there _might_ be a misunderstanding, but I'm not sure if I read your message correctly here:

here somehow applying nb_seats across the equality preserves convertibility, because they use change.. I don't understand.

view this post on Zulip Jacob Salzberg (Oct 30 2022 at 19:01):

Paolo Giarrusso said:

  1. this example does not use "type-level constraints", and B and C remain definitionally distinct as shown below. case H2. just modifies the goal by producing a dependent pattern match expression — how _that_ works is a more advanced question

    case H2.
    Fail Check (eq_refl _ : eq2 B C).
    Check (eq_refl _ : eq2 B B).
(*
The term "eq_refl B" has type "eq2 B B" while it is expected to have type
 "eq2 B C" (cannot unify "B" and "C").
eq_refl B : eq2 B B
     : eq2 B B
*)

Thank you Paolo. I appreciate your time.

May I ask you one clarifying question -- is case then basically taking H2 of the goal and pattern matching on it to find the only way it could have been constructed is with an eq_refl : B B?

Thanks. I'm just trying to make sure I have at least a high level idea of how this works in case in the future when programming in coq I get stuck.

:-)

view this post on Zulip Paolo Giarrusso (Oct 30 2022 at 19:05):

your explanation of case H2 is the correct intuition. However, case is often less smart than this kind of intuition and the exact rules are tricky (and luckily, they're often unnecessary).

view this post on Zulip Pierre Castéran (Oct 30 2022 at 19:06):

Indeed, that comes from a pair of examples showing how change may be used to simulate discriminate and injection.

view this post on Zulip Paolo Giarrusso (Oct 30 2022 at 19:06):

If you want to relate what the tactics do to the actual typechecking algorithm, you should first looks at the proof terms, for instance through Print eq2_trans3.

view this post on Zulip Paolo Giarrusso (Oct 30 2022 at 19:08):

The full rules for conversion are documented in the manual (https://coq.inria.fr/refman/language/core/conversion.html), but the basic idea is that a and b are convertible if Eval cbv in a and Eval cbv in b produce the same normal form.

view this post on Zulip Paolo Giarrusso (Oct 30 2022 at 19:10):

to keep things a bit simpler, I'm ignoring on purpose the sections on eta-expansion — https://coq.inria.fr/refman/language/core/conversion.html#expansion — and on SProp — https://coq.inria.fr/refman/language/core/conversion.html#proof-irrelevance.

view this post on Zulip Notification Bot (Nov 01 2022 at 23:18):

Jacob Salzberg has marked this topic as resolved.

view this post on Zulip Notification Bot (Nov 01 2022 at 23:18):

Jacob Salzberg has marked this topic as unresolved.


Last updated: Jan 27 2023 at 00:03 UTC