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

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

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

being definitionally equal to`x`

.

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

in particular, this is not applying `nb_seats`

to the hypothesis `bicycle x1 = bicycle y1`

.

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.

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.

:-)

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

Indeed, that comes from a pair of examples showing how `change`

may be used to simulate `discriminate`

and `injection`

.

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`

.

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.

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.

Jacob Salzberg has marked this topic as resolved.

Jacob Salzberg has marked this topic as unresolved.

Last updated: Oct 03 2023 at 02:34 UTC