For the record, two examples of short proofs of uniqueness of identity

proofs, on bool and nat.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15971 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 43 insertions, 0 deletions

diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index 3a6f6a236..16c50b410 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -322,3 +322,46 @@ Proof.
   apply eq_rect_eq_dec.
   apply eq_dec.
 Qed.
+
+  (** Examples of short direct proofs of unicity of reflexivity proofs
+      on specific domains *)
+
+Lemma UIP_refl_bool (b:bool) (x : b = b) : x = eq_refl.
+Proof.
+  destruct b.
+  - change (match true as b return true=b -> Prop with
+            | true => fun x => x = eq_refl
+            | _ => fun _ => True
+            end x).
+    destruct x; reflexivity.
+  - change (match false as b return false=b -> Prop with
+            | false => fun x => x = eq_refl
+            | _ => fun _ => True
+            end x).
+    destruct x; reflexivity.
+Defined.
+
+Lemma UIP_refl_nat (n:nat) (x : n = n) : x = eq_refl.
+Proof.
+  induction n.
+  - change (match 0 as n return 0=n -> Prop with
+            | 0 => fun x => x = eq_refl
+            | _ => fun _ => True
+            end x).
+    destruct x; reflexivity.
+  - specialize IHn with (f_equal pred x).
+    change eq_refl with
+           (match (@eq_refl _ n) in _ = n' return S n = S n' with
+            | eq_refl => eq_refl
+            end).
+    rewrite <- IHn; clear IHn.
+    change (match S n as n' return S n = n' -> Prop with
+            | 0 => fun _ => True
+            | S n' => fun x =>
+                x = match f_equal pred x in _ = n' return S n = S n' with
+                    | eq_refl => eq_refl
+                    end
+            end x).
+  pattern (S n) at 2 3, x.
+  destruct x; reflexivity.
+Defined.