1
$\begingroup$

I'm having an issue with dependent typing. I have reduced it to the following minimal example:

Require Import Arith.
Require Import Equality.

Inductive Ex (n : nat) :=
  | X : Ex n.

Definition Cast (n : nat) {n'} 
  (eq : n = n') (e : Ex n) : Ex n'.
Proof.
  destruct eq.
  exact e.
Defined.

Lemma dim_help {x y} (H: x =? y = true) : x = y.
Proof.
  apply Nat.eqb_eq; easy.
Defined.

Definition test {dim} (n : nat) : Ex dim.
  destruct (n =? dim) eqn:H.
  + apply (Cast _ (dim_help H)).
    apply (X n).
  + apply (X dim).
Defined.

Lemma test_lemma : forall n, @test n n = X n.
Proof.
  intros.
  unfold test.
Abort.

In the following code my goal in test_lemma works out to be

(if n =? n as b return ((n =? n) = b -> Ex n)
 then fun H : (n =? n) = true => Cast n (dim_help H) (X n)
 else fun _ : (n =? n) = false => X n) eq_refl = X n

Intuitively I'd like to destruct over n =? n however that yields the error

fun b0 : bool =>
(if b0 as b1 return (b0 = b1 -> Ex n)
 then fun H : b0 = true => Cast n (dim_help H) (X n)
 else fun _ : b0 = false => X n) eq_refl = X n
which is ill-typed.
Reason is: Illegal application: 
The term "@dim_help" of type "forall x y : nat, (x =? y) = true -> x = y"
cannot be applied to the terms
 "n" : "nat"
 "n" : "nat"
 "H" : "b0 = true"
The 3rd term has type "b0 = true" which should be coercible to
 "(n =? n) = true".

Is there a way to work around this issue? How can I destruct the equality to do case analysis over test?

$\endgroup$
2
  • $\begingroup$ Ex n is equivalent to True. Are you sure this is what you intend? $\endgroup$
    – Trebor
    Jan 31, 2023 at 2:34
  • 1
    $\begingroup$ This is just a reduced minimal example to show issues with the handling of specific proof terms. It is not an actually used proof script. However, the answer still applies to our proof script. $\endgroup$
    – Adrian L
    Jan 31, 2023 at 21:28

1 Answer 1

3
$\begingroup$

Coq simply tells you that when it is trying to do a case on n ?= n in the expression

(if n =? n as b return ((n =? n) = b -> Ex n)
 then fun H : (n =? n) = true => Cast n (dim_help H) (X n)
 else fun _ : (n =? n) = false => X n) eq_refl = X n

your argument eq_refl does not vary as needed : it should be a proof of (n =? n) = true in the first case and a proof of (n =? n) = false in the second case. There is no way eq_refl will meet this,

You can fix this with a simpler definition of test

Definition test {dim} (n : nat) : Ex dim.
  destruct (Nat.eq_dec n dim) as [e|e].
  + apply (Cast _ e).
    apply (X n).
  + apply (X dim).
Defined.

Then you are left with proving

forall e : n = n, Cast n e (X n) = X n

which can be done because unicity of identity proof holds in Coq for natural numbers. so we have

forall n (e : n = n), e = refl_eq n.
$\endgroup$
1
  • $\begingroup$ Thank you for the clear explanation! This is exactly what I was looking for $\endgroup$
    – Adrian L
    Jan 31, 2023 at 18:35

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.