diff options
Diffstat (limited to 'theories/Logic/Eqdep_dec.v')
-rw-r--r-- | theories/Logic/Eqdep_dec.v | 124 |
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. |