Convertability and Typing of Terms · Coq users

Stream: Coq users

Topic: Convertability and Typing of Terms

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

Paolo Giarrusso (Oct 30 2022 at 18:51):

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
*)

Paolo Giarrusso (Oct 30 2022 at 18:53):

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

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.

Paolo Giarrusso (Oct 30 2022 at 18:58):

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

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.

Jacob Salzberg (Oct 30 2022 at 19:01):

Paolo Giarrusso said:

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.

:-)

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).

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.

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.

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.

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.

Notification Bot (Nov 01 2022 at 23:18):

Jacob Salzberg has marked this topic as resolved.

Notification Bot (Nov 01 2022 at 23:18):

Jacob Salzberg has marked this topic as unresolved.

Last updated: Oct 13 2024 at 01:02 UTC