summaryrefslogtreecommitdiff
path: root/theories/Logic/Eqdep_dec.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Logic/Eqdep_dec.v')
-rw-r--r--theories/Logic/Eqdep_dec.v124
1 files changed, 96 insertions, 28 deletions
diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index 015c7a5f..65011e8e 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -35,6 +35,7 @@ Table of contents:
(** * Streicher's K and injectivity of dependent pair hold on decidable types *)
Set Implicit Arguments.
+(* Set Universe Polymorphism. *)
Section EqdepDec.
@@ -49,12 +50,12 @@ Section EqdepDec.
case u; trivial.
Qed.
- Variable eq_dec : forall x y:A, x = y \/ x <> y.
-
Variable x : A.
+ Variable eq_dec : forall y:A, x = y \/ x <> y.
+
Let nu (y:A) (u:x = y) : x = y :=
- match eq_dec x y with
+ match eq_dec y with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind _ (neqxy u)
end.
@@ -62,17 +63,17 @@ Section EqdepDec.
Let nu_constant : forall (y:A) (u v:x = y), nu u = nu v.
intros.
unfold nu.
- case (eq_dec x y); intros.
+ destruct (eq_dec y) as [Heq|Hneq].
reflexivity.
- case n; trivial.
+ case Hneq; trivial.
Qed.
Let nu_inv (y:A) (v:x = y) : x = y := comp (nu (eq_refl x)) v.
- Remark nu_left_inv : forall (y:A) (u:x = y), nu_inv (nu u) = u.
+ Remark nu_left_inv_on : forall (y:A) (u:x = y), nu_inv (nu u) = u.
Proof.
intros.
case u; unfold nu_inv.
@@ -80,20 +81,20 @@ Section EqdepDec.
Qed.
- Theorem eq_proofs_unicity : forall (y:A) (p1 p2:x = y), p1 = p2.
+ Theorem eq_proofs_unicity_on : forall (y:A) (p1 p2:x = y), p1 = p2.
Proof.
intros.
- elim nu_left_inv with (u := p1).
- elim nu_left_inv with (u := p2).
+ elim nu_left_inv_on with (u := p1).
+ elim nu_left_inv_on with (u := p2).
elim nu_constant with y p1 p2.
reflexivity.
Qed.
- Theorem K_dec :
+ Theorem K_dec_on :
forall P:x = x -> Prop, P (eq_refl x) -> forall p:x = x, P p.
Proof.
intros.
- elim eq_proofs_unicity with x (eq_refl x) p.
+ elim eq_proofs_unicity_on with x (eq_refl x) p.
trivial.
Qed.
@@ -101,27 +102,26 @@ Section EqdepDec.
Let proj (P:A -> Prop) (exP:ex P) (def:P x) : P x :=
match exP with
- | ex_intro x' prf =>
- match eq_dec x' x with
- | or_introl eqprf => eq_ind x' P prf x eqprf
+ | ex_intro _ x' prf =>
+ match eq_dec x' with
+ | or_introl eqprf => eq_ind x' P prf x (eq_sym eqprf)
| _ => def
end
end.
- Theorem inj_right_pair :
+ Theorem inj_right_pair_on :
forall (P:A -> Prop) (y y':P x),
ex_intro P x y = ex_intro P x y' -> y = y'.
Proof.
intros.
cut (proj (ex_intro P x y) y = proj (ex_intro P x y') y).
simpl.
- case (eq_dec x x).
- intro e.
- elim e using K_dec; trivial.
+ destruct (eq_dec x) as [Heq|Hneq].
+ elim Heq using K_dec_on; trivial.
intros.
- case n; trivial.
+ case Hneq; trivial.
case H.
reflexivity.
@@ -129,6 +129,28 @@ Section EqdepDec.
End EqdepDec.
+(** Now we prove the versions that require decidable equality for the entire type
+ rather than just on the given element. The rest of the file uses this total
+ decidable equality. We could do everything using decidable equality at a point
+ (because the induction rule for [eq] is really an induction rule for
+ [{ y : A | x = y }]), but we don't currently, because changing everything
+ would break backward compatibility and no-one has yet taken the time to define
+ the pointed versions, and then re-define the non-pointed versions in terms of
+ those. *)
+
+Theorem eq_proofs_unicity A (eq_dec : forall x y : A, x = y \/ x <> y) (x : A)
+: forall (y:A) (p1 p2:x = y), p1 = p2.
+Proof (@eq_proofs_unicity_on A x (eq_dec x)).
+
+Theorem K_dec A (eq_dec : forall x y : A, x = y \/ x <> y) (x : A)
+: forall P:x = x -> Prop, P (eq_refl x) -> forall p:x = x, P p.
+Proof (@K_dec_on A x (eq_dec x)).
+
+Theorem inj_right_pair A (eq_dec : forall x y : A, x = y \/ x <> y) (x : A)
+: forall (P:A -> Prop) (y y':P x),
+ ex_intro P x y = ex_intro P x y' -> y = y'.
+Proof (@inj_right_pair_on A x (eq_dec x)).
+
Require Import EqdepFacts.
(** We deduce axiom [K] for (decidable) types *)
@@ -181,7 +203,7 @@ Unset Implicit Arguments.
Module Type DecidableType.
- Parameter U:Type.
+ Monomorphic Parameter U:Type.
Axiom eq_dec : forall x y:U, {x = y} + {x <> y}.
End DecidableType.
@@ -249,7 +271,7 @@ End DecidableEqDep.
Module Type DecidableSet.
- Parameter U:Type.
+ Parameter U:Set.
Axiom eq_dec : forall x y:U, {x = y} + {x <> y}.
End DecidableSet.
@@ -272,23 +294,23 @@ Module DecidableEqDepSet (M:DecidableSet).
Theorem eq_dep_eq :
forall (P:U->Type) (p:U) (x y:P p), eq_dep U P p x p y -> x = y.
- Proof N.eq_dep_eq.
+ Proof (eq_rect_eq__eq_dep_eq U eq_rect_eq).
(** Uniqueness of Identity Proofs (UIP) *)
Lemma UIP : forall (x y:U) (p1 p2:x = y), p1 = p2.
- Proof N.UIP.
+ Proof (eq_dep_eq__UIP U eq_dep_eq).
(** Uniqueness of Reflexive Identity Proofs *)
Lemma UIP_refl : forall (x:U) (p:x = x), p = eq_refl x.
- Proof N.UIP_refl.
+ Proof (UIP__UIP_refl U UIP).
(** Streicher's axiom K *)
Lemma Streicher_K :
forall (x:U) (P:x = x -> Prop), P (eq_refl x) -> forall p:x = x, P p.
- Proof N.Streicher_K.
+ Proof (K_dec_type eq_dec).
(** Proof-irrelevance on subsets of decidable sets *)
@@ -318,7 +340,53 @@ Proof.
intros A eq_dec.
apply eq_dep_eq__inj_pair2.
apply eq_rect_eq__eq_dep_eq.
- unfold Eq_rect_eq.
- apply eq_rect_eq_dec.
+ unfold Eq_rect_eq, Eq_rect_eq_on.
+ intros; 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_unit (x : tt = tt) : x = eq_refl tt.
+Proof.
+ change (match tt as b return tt = b -> Prop 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.
+ - 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 (f_equal S (@eq_refl _ n)).
+ rewrite <- IHn; clear IHn.
+ change (match S n as n' return S n = n' -> Prop with
+ | 0 => fun _ => True
+ | S n' => fun x =>
+ x = f_equal S (f_equal pred x)
+ end x).
+ pattern (S n) at 2 3, x.
+ destruct x; reflexivity.
+Defined.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 13:52:46 +0000