## 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 |

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), |