## 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 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):

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

#### 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`.

#### 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 }.

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:

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.

:-)

#### 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 03 2023 at 02:34 UTC