Pavel Shuhray (Apr 22 2023 at 00:14): Pavel Shuhray (Apr 22 2023 at 00:14):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?
Patrick Nicodemus (Apr 22 2023 at 03:04):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.
Patrick Nicodemus (Apr 22 2023 at 03:06):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
Patrick Nicodemus (Apr 22 2023 at 03:07):And you would have to restate your theorem to use this bijection
Patrick Nicodemus (Apr 22 2023 at 18:02):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
James Wood (Apr 22 2023 at 18:54):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: Oct 04 2023 at 23:01 UTC