2
$\begingroup$

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.

$\endgroup$

1 Answer 1

5
$\begingroup$

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.
$\endgroup$
2
  • $\begingroup$ 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 :) $\endgroup$
    – Niols
    Feb 6, 2016 at 21:30
  • 1
    $\begingroup$ 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). $\endgroup$ Feb 7, 2016 at 0:25

Your Answer

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

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