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

<p>Also note that we cannot decompose the equation</p>

<pre><code>{| VN_value := m_value; VN_prop := m_prop |} =
 {| VN_value := n_value; VN_prop := n_prop |}
</code></pre>

<p>into</p>

<pre><code>m_value = n_value
</code></pre>

<p>and</p>

<pre><code>m_prop = n_prop
</code></pre>

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

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

<pre><code>Fixpoint valid (n: nat) : bool :=
  match n with
    | 0 =&gt; true
    | 1 =&gt; false
    | S (S p) =&gt; valid p
  end.

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

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

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

CC BY-SA 3.0
2016-02-06T21:30:30.560Z
Hum, I think I understand what you're doing here. However, I don't understand why the types `valid m_value = true` and `valid n_value = true` wouldn't be equal since I have an hypothesis `m_value = n_value` (I understand it must be hard to explain this to Coq though). I've tried rewriting using that same hypothesis but it's not working either (I don't know how to rewrite in the goal and in the assumptions at the same time…). It might not be clear, and I will edit my post if this is the case. Thanks for the help you already brought me :)
Niols
CC BY-SA 3.0
2016-02-07T00:25:34.597Z
The type `valid m_value = true` and `valid n_value = true` are *propositionally* equal, which means that the type `(valid m_value = true) = (valid n_value = true)` is inhabited by some `p`. But they are *not* judgmentally equal, an so from `x : valid m_value = true` we cannot conclude `x : valid n_value = true`. Instead we get to conclude that *the transport of `x` along `p`* has type `valid n_value = true`. Have you looked at homotopy type theory? There these things are explained carefully (and also why things are done this way).
Andrej Bauer
CC BY-SA 3.0
2016-02-06T18:24:00.833Z
2016-02-06T18:47:35.903Z
2016-02-06T18:47:35.903Z
Andrej Bauer
<p>I'm trying to do the following thing: take a set (here, <code>nat</code>, 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.</p>

<p>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 <code>f_equal</code> 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).</p>

<p>Here is my code. Define a boolean predicate for valid values:</p>

<pre><code>Fixpoint valid (n: nat) : bool :=
  match n with
    | 0 =&gt; true
    | 1 =&gt; false
    | S (S p) =&gt; valid p
  end
.
</code></pre>

<p>Define the type for valid values using the predicate and records:</p>

<pre><code>Record valid_nat : Type :=
  { VN_value : nat ;
    VN_prop  : valid VN_value = true }
.
</code></pre>

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

<pre><code>Theorem valid_nat_unique:
  forall (m n: valid_nat), VN_value m = VN_value n -&gt; 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 *)
</code></pre>

<p>Here is the goal before and after the <code>f_equal</code> tactic:</p>

<pre><code>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 |}
</code></pre>

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

<p>My Coq version is: <code>The Coq Proof Assistant, version 8.5 (February 2016)</code></p>

<p>Any help would be highly appreciated. Thank you by advance.</p>

<coq>
`f_equal` isn't doing anything
Niols
# `f_equal` isn't doing anything

(Asked by: username_0 on 2016-02-06)

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.

**Tags:** coq

---

## 1 answers

### Answer by username_1 on 2016-02-06. Score: 5 | Accepted answer

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.

> **Comments:**
> **username_0**: Hum, I think I understand what you're doing here. However, I don't understand why the types `valid m_value = true` and `valid n_value = true` wouldn't be equal since I have an hypothesis `m_value = n_value` (I understand it must be hard to explain this to Coq though). I've tried rewriting using that same hypothesis but it's not working either (I don't know how to rewrite in the goal and in the assumptions at the same time…). It might not be clear, and I will edit my post if this is the case. Thanks for the help you already brought me :)  
> **username_1**: The type `valid m_value = true` and `valid n_value = true` are *propositionally* equal, which means that the type `(valid m_value = true) = (valid n_value = true)` is inhabited by some `p`. But they are *not* judgmentally equal, an so from `x : valid m_value = true` we cannot conclude `x : valid n_value = true`. Instead we get to conclude that *the transport of `x` along `p`* has type `valid n_value = true`. Have you looked at homotopy type theory? There these things are explained carefully (and also why things are done this way).  

---

