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.