Hi all.

I have types `B`

and `A n`

where `n:nat`

. I want to prove that `B`

is the sum of all `A n`

. I have three functions

```
foo (n:nat) (a: A n) : B
rang (b:B) : nat
bar (b:B) : A (rang b)
```

I can prove

```
forall (b:B), foo (rang b) (bar b) = b
forall (n:nat) (a: A n), rang (foo n a) = n
```

But when I write the theorem

```
forall (n:nat) (a: A n), bar (foo n a) = a
```

I get "The term `bar (foo n a)`

has type `A (rang (foo n a))`

while it is expected to have type `A n`

"

What can I do?

When you write `x = y`

, this is an abbreviation for `eq _ x y`

, and Coq tries to fill in the wildcard `_`

with the (common) type of `x`

and `y`

. In order for this to type check, `x`

and `y`

need to have the same type.

This statement will only type check if `A n`

is convertible (or "definitionally equal", or "judgementally equal") to `A (rang (foo n a))`

. Your assumption only states that `rang (foo n a)`

is *propositionally* equal to `n`

, which is weaker. In Coq the "logic of the grammar" (what expressions are well-formed) is more fundamental than the "logic of propositions" (what sentences are true and false) and you can't use a proposition (x = y) to prove a grammatical claim (y is of type A (rang (foo n a)).

This is somewhat annoying but think of it this way: You want the "logic of the grammar" to be simple, so that Coq can automatically decide on its own (by carrying out a deterministic decision procedure) whether a term is well-typed. But suppose that `n`

is defined to be `0`

if Goldbach's conjecture is correct, and `1`

otherwise, and suppose we have `x : A(0)`

. Is `x : A(n)`

? Coq cannot decide this without deciding Goldbach's conjecture, so it is very hard to determine whether this is well-typed.

Anyway, you can prove that if `x,y : X`

, and `p :x=y`

and `A`

is a dependent type `X -> Type`

then there is a bijection between `A(x)`

and `A(y)`

. You can prove this yourself, but you can also use the Logic.Transport function in the equations module

And you would have to restate your theorem to use this bijection

Oh, there's also another equality type which Conor McBride has studied, he calls it "John Major equality" but this is a kind of inside joke from british politics that I don't really understood. It's also called heterogeneous equality. Anyway this equality is not the same as the usual one without assuming certain additional axioms but it does let you state theorems like this

To clarify, John Major equality itself is not a joke, but the name is. And I think Conor originally studied it as a way to deal with (iterated) Σ-types, so it might be relevant here. However, it has the habit of offering itself up as an easy solution where careful thought would produce something smoother (this is not part of the joke), so it's generally good not to use it if there's another way IME.

Last updated: Jun 15 2024 at 05:01 UTC