diff options
| -rw-r--r-- | theories/Logic/EqdepFacts.v | 23 | ||||
| -rw-r--r-- | theories/Logic/Eqdep_dec.v | 8 |
2 files changed, 31 insertions, 0 deletions
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index a22f286eda..0e9f39f6b4 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -325,6 +325,29 @@ Section Equivalences. End Equivalences. +(** UIP_refl is downward closed (a short proof of the key lemma of Voevodsky's + proof of inclusion of h-level n into h-level n+1; see hlevelntosn + in https://github.com/vladimirias/Foundations.git). *) + +Theorem UIP_shift : forall U, UIP_refl_ U -> forall x:U, UIP_refl_ (x = x). +Proof. + intros X UIP_refl x y. + rewrite (UIP_refl x y). + intros z. + assert (UIP:forall y' y'' : x = x, y' = y''). + { intros. apply eq_trans with (eq_refl x). apply UIP_refl. + symmetry. apply UIP_refl. } + transitivity (eq_trans (eq_trans (UIP (eq_refl x) (eq_refl x)) z) + (eq_sym (UIP (eq_refl x) (eq_refl x)))). + - destruct z. unfold e. destruct (UIP _ _). reflexivity. + - change + (match eq_refl x as y' in _ = x' return y' = y' -> Type with + | eq_refl => fun z => z = (eq_refl (eq_refl x)) + end (eq_trans (eq_trans (UIP (eq_refl x) (eq_refl x)) z) + (eq_sym (UIP (eq_refl x) (eq_refl x))))). + destruct z. unfold e. destruct (UIP _ _). reflexivity. +Qed. + Section Corollaries. Variable U:Type. diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v index 16c50b410a..ea5b16517d 100644 --- a/theories/Logic/Eqdep_dec.v +++ b/theories/Logic/Eqdep_dec.v @@ -326,6 +326,14 @@ Qed. (** Examples of short direct proofs of unicity of reflexivity proofs on specific domains *) +Lemma UIP_refl_unit (x : tt = tt) : x = eq_refl tt. +Proof. + change (match tt as b return tt = b -> Type with + | tt => fun x => x = eq_refl tt + end x). + destruct x; reflexivity. +Defined. + Lemma UIP_refl_bool (b:bool) (x : b = b) : x = eq_refl. Proof. destruct b. |