diff options
| -rw-r--r-- | theories/Logic/Eqdep_dec.v | 43 |
1 files changed, 43 insertions, 0 deletions
diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v index 3a6f6a2363..16c50b410a 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. |