1
$\begingroup$

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?

$\endgroup$
1
  • 2
    $\begingroup$ Please post a working piece of code. It is not clear whether A, B, foo, rang` etc. are concrete types or variables. As written, without knowing more about them, you cannot prove the desired equalities. There is information that you are not communicating. $\endgroup$ May 22, 2023 at 12:49

3 Answers 3

1
$\begingroup$

Since the code snippet doesn't work I will assume that you are trying to construct an equality type on dependent types.

Hypothesis A: nat -> Type.
Hypothesis B: Type.

Definition foo (n: nat) (a: A n) : B.  Admitted.
Definition rang (b: B) : nat. Admitted.
Definition bar (b: B) : A (rang b). Admitted.

You now have

Theorem thm1: forall (b: B), foo (rang b) (bar b) = b.
Proof. Admitted.

Theorem thm2: forall (n: nat) (a: A n),  rang (foo n a) = n.
Proof. Admitted.

You have difficulty writing this:

Theorem thm3: forall (n:nat) (a: A n), bar (foo n a) = a.

which gives you the error:

In environment
n : nat
a : A n
The term "a" has type "A n" while it is expected to have type
"A (rang (foo n a))".

Is this what you want? Well, in that case, the root problem is that to construct a type = you have to let Coq know that the types of two terms must be the same, but since you have wrapped $n$ inside some functions, Coq has no idea whether rang (foo n a) = n. You can check how eq is constructed:

Check eq.
eq
     : ?A -> ?A -> Prop
where
?A : [ |- Type]

This is checked syntactically, which means propositional equality won't simply work in your case (even though you can prove that rang (foo n a) = n). This is also known as heterogenous equality. Also, by checking the recursion rule of eq you will know more about this:

Check eq_rect.
------------------------
eq_rect
     : forall (A : Type) (x : A) (P : A -> Type),
P x -> forall y : A, x = y -> P y

It says you will obtain a new term of type $ P y $ if you can provide a proof which states that $x = y$ holds (this is actually the Leibniz rule). So the trick to type check is using transport or type cast as suggested by @djao.

$\endgroup$
0
$\begingroup$

Maybe use an explicit cast?

Theorem rang_foo : ∀ (n:nat) (a: A n), rang (foo n a) = n.
Proof.
  admit.
Admitted.

Definition cast {X Y : nat} (e : X = Y) : A X → A Y :=
  match e with erefl => id end.

Goal ∀ (n:nat) (a: A n), cast (rang_foo n a) (bar (foo n a)) = a.
$\endgroup$
6
  • $\begingroup$ "The term "id" has type "ID" while it is expected to have type "A X -> A Y" (cannot unify "Top.A X" and "Type")." $\endgroup$ Apr 22, 2023 at 3:23
  • $\begingroup$ Since you didn't post a full working file, I don't know exactly what you did. Here is my file, in which it works: gist.github.com/davidjao/b6209fa5242368b80d77c996d7273600 $\endgroup$
    – djao
    Apr 22, 2023 at 3:51
  • $\begingroup$ Probably erefl is being seen as a variable name, rather than the alias from SSReflect. eq_refl in its place should work. $\endgroup$
    – James Wood
    Apr 22, 2023 at 14:46
  • $\begingroup$ @djao Yes, I can write the theorem now, but I can't prove it:) The function cast need eq_refl to be simplified. Is each proof e: X=Y equal to eq_refl? $\endgroup$ Apr 22, 2023 at 18:38
  • $\begingroup$ In general you need Streicher's axiom K to show that all proofs of equality are equal. When equality is decidable (which is the case for nat), you can prove the result directly without axioms. See coq.inria.fr/library/Coq.Logic.Eqdep_dec.html $\endgroup$
    – djao
    Apr 23, 2023 at 4:00
0
$\begingroup$

One option is to use heterogeneous or "John-Majors" equality.

Essentially, the problem is that you are trying to say that two terms of syntactically different (but equal) types are the same. However, Coq and related systems require that terms are reducible to the same thing, rather than merely equal.

Heterogeneous equality solves this by allowing you to use two different types to set up your equality. You then must prove that both the types and the terms are equal in order to prove the equality.

In Coq, there's an implementation of heterogeneous equality in the standard library: https://coq.inria.fr/library/Coq.Logic.JMeq.html. You can then write

forall (n : nat) (a : A n), JMeq a (bar (foo n a))

just as you wanted. Working with JMeq is a little more difficult, see http://adam.chlipala.net/cpdt/html/Equality.html for examples.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.