`f_equal` isn't doing anything

Question

I'm trying to do the following thing: take a set (here, nat, for the sake of simplicity), define a subset of "valid" values (here, even numbers), and then prove that two valid values with the same value are the same.

My problem is that my valid values are represented by records. And when I try to prove what I want, I try to use the f_equal tactic on that record and it does nothing. I imagine this is because both parts of the record are dependent, but I really don't know (I'm new to these).

Here is my code. Define a boolean predicate for valid values:

Fixpoint valid (n: nat) : bool :=
  match n with
    | 0 => true
    | 1 => false
    | S (S p) => valid p
  end
.

Define the type for valid values using the predicate and records:

Record valid_nat : Type :=
  { VN_value : nat ;
    VN_prop  : valid VN_value = true }
.

Prove that when the values are the same, the records are the same. I know this implies proof irrelevance, but that's not my main problem yet:

Theorem valid_nat_unique:
  forall (m n: valid_nat), VN_value m = VN_value n -> m = n
.
Proof.
  intros m n H.
  destruct m as [m_value m_prop].
  destruct n as [n_value n_prop].
  simpl in H.
  f_equal.    (* does nothing *)

Here is the goal before and after the f_equal tactic:

m_value : nat
m_prop : valid m_value = true
n_value : nat
n_prop : valid n_value = true
H : m_value = n_value
============================
 {| VN_value := m_value; VN_prop := m_prop |} =
 {| VN_value := n_value; VN_prop := n_prop |}

I was expecting to get m_value = n_value /\ m_prop = n_prop (then hypothesis H and proof irrelevance should be enough to finish. And now I'm stuck.

My Coq version is: The Coq Proof Assistant, version 8.5 (February 2016)

Any help would be highly appreciated. Thank you by advance.

Answer 1

The f_equal tactic does not do anything because what you are trying to prove is not true. You assumed that the first components (VN_value) of m and n are equal, but what about the second components (VN_prop), how do you intend to prove they are equal?

Also note that we cannot decompose the equation

{| VN_value := m_value; VN_prop := m_prop |} =
 {| VN_value := n_value; VN_prop := n_prop |}

into

m_value = n_value

and

m_prop = n_prop

because the second equation is not well typed: the left-hand side has type valid m_value = true and the right-hand side valid n_value = true. Instead, we need to transport m_prop from the type valid m = true to the type valid n = true.

So, you need transport and you need an extra assumption. Here is how you can do it:

Fixpoint valid (n: nat) : bool :=
  match n with
    | 0 => true
    | 1 => false
    | S (S p) => valid p
  end.

Record valid_nat : Type :=
  { VN_value : nat ;
    VN_prop  : valid VN_value = true }.

Definition transport {A : Type} (B : A -> Type) {a b : A}: a = b -> B a -> B b.
Proof.
  intros [] ?; assumption.
Defined.

Lemma valid_nat_unique (m n : valid_nat) (p : VN_value m = VN_value n):
  transport (fun k => valid k = true) p (VN_prop m) = VN_prop n ->
  m = n.
Proof.
  destruct m; destruct n.
  simpl in * |- *.
  destruct p.
  intros [].
  reflexivity.
Qed.