1

I'm reading Software Foundations book and in Imp.v file, there is this definition of a theorem eq_id_dec as follows: 

Theorem eq_id_dec : forall id1 id2 : id, {id1 = id2} + {id1 <> id2}.
Proof.
   intros id1 id2.
   destruct id1 as [n1]. destruct id2 as [n2].
   destruct (eq_nat_dec n1 n2) as [Heq | Hneq].
   Case "n1 = n2".
     left. rewrite Heq. reflexivity.
   Case "n1 <> n2".
     right. intros contra. inversion contra. apply Hneq. apply H0.
Defined.

Does this theorem mean that for any id1 and id2 of type id, both id1=id2 and id1!=id2 cannot happen? I'm not sure.

elysefaulkner
  • 973
  • 2
  • 8
  • 8

2 Answers2

3

No, it does not preclude the case that both the equality and the inequality are true at the same time (though in practice it is the case here).

The type sumbool A B, of notation {A} + {B}, characterizes a decision procedure that will prove either A or B.

So this eq_id_dec is a term that will take two ids as input, and either return a proof that they are equal, or a proof that they are distinct.

More about sumbool here: https://coq.inria.fr/distrib/current/stdlib/Coq.Bool.Sumbool.html

Ptival
  • 9,167
  • 36
  • 53
  • So, if I have to call this function, i have to pass in a value of type id. Id is Id: nat -> id. How would i do that. I do Eval Compute in (eq_id_dec (id 4) (id 5)). and it fails – elysefaulkner May 03 '15 at 05:19
  • Eval compute in (eq_id_dec (Id 4) (Id 5)). – Ptival May 03 '15 at 07:52
-1

For all id1 and id2, id1 = id2 or id1 does not equal id2.

Pretty straightforward - either it equals id2 or it does not, which will by definition always be true - so it is true for all id1/id2.

King Dedede
  • 970
  • 1
  • 12
  • 28
  • 1
    Except that in an intuitionistic framework like Coq, `P \/ ~P` is not necessarily true (you can add excluded middle as an axiom). You have to prove that the equality is decidable (hence the `dec` in the name of the theorem) in the type of `id1` and `id2`. – Virgile May 05 '15 at 06:30