# coq/coq

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```
• Loading branch information...
herbelin committed Nov 15, 2012
1 parent e41da6e commit 86c8f958a739f16dc24d684cd396ab75a072ebee
Showing with 43 additions and 0 deletions.
1. +43 −0 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.

#### 0 comments on commit `86c8f95`

Please sign in to comment.