Mercurial > cpdt > repo

comparison src/Equality.v @ 536:d65e9c1c9041

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Touch-ups in 8.4
author Adam Chlipala <adam@chlipala.net>
date Wed, 05 Aug 2015 18:07:57 -0400
parents ed829eaa91b2
children 81d63d9c1cc5
comparison
equal deleted inserted replaced
535:dac7a2705b00 536:d65e9c1c9041
831 eq_ind_r 831 eq_ind_r
832 : forall (A : Type) (x : A) (P : A -> Prop), 832 : forall (A : Type) (x : A) (P : A -> Prop),
833 P x -> forall y : A, y = x -> P y 833 P x -> forall y : A, y = x -> P y
834 ]] 834 ]]
835 835
836 The corresponding lemma used for [JMeq] in the proof of [pair_cong] is defined internally by [rewrite as needed, but its type happens to be the following. *) 836 The corresponding lemma used for [JMeq] in the proof of [pair_cong] is defined internally by [rewrite] as needed, but its type happens to be the following. *)
837 837
838 (** %\vspace{-.15in}%[[ 838 (** %\vspace{-.15in}%[[
839 internal_JMeq_rew_r 839 internal_JMeq_rew_r
840 : forall (A : Type) (x : A) (B : Type) (b : B) 840 : forall (A : Type) (x : A) (B : Type) (b : B)
841 (P : forall B0 : Type, B0 -> Type), P B b -> x == b -> P A x 841 (P : forall B0 : Type, B0 -> Type), P B b -> x == b -> P A x
842 ]] 842 ]]
843 843
844 The key difference is that, where the [eq] lemma is parameterized on a predicate of type [A -> Prop], the [JMeq] lemma is parameterized on a predicate of type more like [forall A : Type, A -> Prop]. To apply [eq_ind_r] with a proof of [x = y], it is only necessary to rearrange the goal into an application of a [fun] abstraction to [y]. In contrast, to apply the alternative principle, it is necessary to rearrange the goal to an application of a [fun] abstraction to both [y] and _its type_. In other words, the predicate must be _polymorphic_ in [y]'s type; any type must make sense, from a type-checking standpoint. There may be cases where the former rearrangement is easy to do in a type-correct way, but the second rearrangement done %\%naive%{}%ly leads to a type error. 844 The key difference is that, where the [eq] lemma is parameterized on a predicate of type [A -> Prop], the [JMeq] lemma is parameterized on a predicate of type more like [forall A : Type, A -> Prop]. To apply [eq_ind_r] with a proof of [x = y], it is only necessary to rearrange the goal into an application of a [fun] abstraction to [y]. In contrast, to apply the alternative principle, it is necessary to rearrange the goal to an application of a [fun] abstraction to both [y] and _its type_. In other words, the predicate must be _polymorphic_ in [y]'s type; any type must make sense, from a type-checking standpoint. There may be cases where the former rearrangement is easy to do in a type-correct way, but the second rearrangement done %\%naive%{}%ly leads to a type error.
845 845
846 When [rewrite] cannot figure out how to apply the alternative principle for [x == y] where [x] and [y] have the same type, the tactic can instead use an alternate theorem, which is easy to prove as a composition of [eq_ind_r] and [JMeq_eq]. *) 846 When [rewrite] cannot figure out how to apply the alternative principle for [x == y] where [x] and [y] have the same type, the tactic can instead use a different theorem, which is easy to prove as a composition of [eq_ind_r] and [JMeq_eq]. *)
847 847
848 Check JMeq_ind_r. 848 Check JMeq_ind_r.
849 (** %\vspace{-.15in}%[[ 849 (** %\vspace{-.15in}%[[
850 JMeq_ind_r 850 JMeq_ind_r
851 : forall (A : Type) (x : A) (P : A -> Prop), 851 : forall (A : Type) (x : A) (P : A -> Prop),