Mercurial > cpdt > repo

comparison src/Equality.v @ 465:4320c1a967c2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Spell check
author Adam Chlipala <adam@chlipala.net>
date Wed, 29 Aug 2012 18:26:26 -0400
parents 848bf35f7f6c
children 1fd4109f7b31
comparison
equal deleted inserted replaced
464:e53d051681b0 465:4320c1a967c2
689 (** %\vspace{-.15in}% [[ 689 (** %\vspace{-.15in}% [[
690 Inductive JMeq (A : Type) (x : A) : forall B : Type, B -> Prop := 690 Inductive JMeq (A : Type) (x : A) : forall B : Type, B -> Prop :=
691 JMeq_refl : JMeq x x 691 JMeq_refl : JMeq x x
692 ]] 692 ]]
693 693
694 The identitifer [JMeq] stands for %\index{John Major equality}%"John Major equality," a name coined by Conor McBride%~\cite{JMeq}% as a sort of pun about British politics. The definition [JMeq] starts out looking a lot like the definition of [eq]. The crucial difference is that we may use [JMeq] _on arguments of different types_. For instance, a lemma that we failed to establish before is trivial with [JMeq]. It makes for prettier theorem statements to define some syntactic shorthand first. *) 694 The identifier [JMeq] stands for %\index{John Major equality}%"John Major equality," a name coined by Conor McBride%~\cite{JMeq}% as a sort of pun about British politics. The definition [JMeq] starts out looking a lot like the definition of [eq]. The crucial difference is that we may use [JMeq] _on arguments of different types_. For instance, a lemma that we failed to establish before is trivial with [JMeq]. It makes for prettier theorem statements to define some syntactic shorthand first. *)
695 695
696 Infix "==" := JMeq (at level 70, no associativity). 696 Infix "==" := JMeq (at level 70, no associativity).
697 697
698 (* EX: Prove UIP_refl' : forall (A : Type) (x : A) (pf : x = x), pf == eq_refl x *) 698 (* EX: Prove UIP_refl' : forall (A : Type) (x : A) (pf : x = x), pf == eq_refl x *)
699 (* begin thide *) 699 (* begin thide *)
840 internal_JMeq_rew_r 840 internal_JMeq_rew_r
841 : forall (A : Type) (x : A) (B : Type) (b : B) 841 : forall (A : Type) (x : A) (B : Type) (b : B)
842 (P : forall B0 : Type, B0 -> Type), P B b -> x == b -> P A x 842 (P : forall B0 : Type, B0 -> Type), P B b -> x == b -> P A x
843 ]] 843 ]]
844 844
845 The key difference is that, where the [eq] lemma is parametrized 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 [internal_JMeq_rew_r], 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 naively leads to a type error. 845 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 [internal_JMeq_rew_r], 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 naively leads to a type error.
846 846
847 When [rewrite] cannot figure out how to apply [internal_JMeq_rew_r] 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]. *) 847 When [rewrite] cannot figure out how to apply [internal_JMeq_rew_r] 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]. *)
848 848
849 Check JMeq_ind_r. 849 Check JMeq_ind_r.
850 (** %\vspace{-.15in}%[[ 850 (** %\vspace{-.15in}%[[