## Mercurial > cpdt > repo

### comparison src/Equality.v @ 534:ed829eaa91b2

Find changesets by keywords (author, files, the commit message), revision
number or hash, or revset expression.

Builds with Coq 8.5beta2

author | Adam Chlipala <adam@chlipala.net> |
---|---|

date | Wed, 05 Aug 2015 14:46:55 -0400 |

parents | 7d2339cbd39c |

children | d65e9c1c9041 |

comparison

equal
deleted
inserted
replaced

533:8921cfa2f503 | 534:ed829eaa91b2 |
---|---|

1 (* Copyright (c) 2008-2012, Adam Chlipala | 1 (* Copyright (c) 2008-2012, 2015, Adam Chlipala |

2 * | 2 * |

3 * This work is licensed under a | 3 * This work is licensed under a |

4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 | 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 |

5 * Unported License. | 5 * Unported License. |

6 * The license text is available at: | 6 * The license text is available at: |

8 *) | 8 *) |

9 | 9 |

10 (* begin hide *) | 10 (* begin hide *) |

11 Require Import Eqdep JMeq List. | 11 Require Import Eqdep JMeq List. |

12 | 12 |

13 Require Import CpdtTactics. | 13 Require Import Cpdt.CpdtTactics. |

14 | 14 |

15 Set Implicit Arguments. | 15 Set Implicit Arguments. |

16 Set Asymmetric Patterns. | |

16 (* end hide *) | 17 (* end hide *) |

17 | 18 |

18 | 19 |

19 (** %\chapter{Reasoning About Equality Proofs}% *) | 20 (** %\chapter{Reasoning About Equality Proofs}% *) |

20 | 21 |

830 eq_ind_r | 831 eq_ind_r |

831 : forall (A : Type) (x : A) (P : A -> Prop), | 832 : forall (A : Type) (x : A) (P : A -> Prop), |

832 P x -> forall y : A, y = x -> P y | 833 P x -> forall y : A, y = x -> P y |

833 ]] | 834 ]] |

834 | 835 |

835 The corresponding lemma used for [JMeq] in the proof of [pair_cong] is %\index{Gallina terms!internal\_JMeq\_rew\_r}%[internal_JMeq_rew_r], which, confusingly, is defined by [rewrite] as needed, so it is not available for checking until after we apply it. *) | 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 | 837 |

837 Check internal_JMeq_rew_r. | |

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 [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 %\%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 [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]. *) | 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]. *) |

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

852 P x -> forall y : A, y == x -> P y | 852 P x -> forall y : A, y == x -> P y |

853 ]] | 853 ]] |

854 | 854 |

855 Ironically, where in the proof of [fhapp_assoc'] we used [rewrite app_assoc] to make it clear that a use of [JMeq] was actually homogeneously typed, we created a situation where [rewrite] applied the axiom-based [JMeq_ind_r] instead of the axiom-free [internal_JMeq_rew_r]! | 855 Ironically, where in the proof of [fhapp_assoc'] we used [rewrite app_assoc] to make it clear that a use of [JMeq] was actually homogeneously typed, we created a situation where [rewrite] applied the axiom-based [JMeq_ind_r] instead of the axiom-free principle! |

856 | 856 |

857 For another simple example, consider this theorem that applies a heterogeneous equality to prove a congruence fact. *) | 857 For another simple example, consider this theorem that applies a heterogeneous equality to prove a congruence fact. *) |

858 | 858 |

859 Theorem out_of_luck : forall n m : nat, | 859 Theorem out_of_luck : forall n m : nat, |

860 n == m | 860 n == m |

872 (fun n0 : nat => S n0 == S m) n | 872 (fun n0 : nat => S n0 == S m) n |

873 ]] | 873 ]] |

874 *) | 874 *) |

875 apply JMeq_ind_r with (x := m); auto. | 875 apply JMeq_ind_r with (x := m); auto. |

876 | 876 |

877 (** However, we run into trouble trying to get the goal into a form compatible with [internal_JMeq_rew_r.] *) | 877 (** However, we run into trouble trying to get the goal into a form compatible with the alternative principle. *) |

878 | 878 |

879 Undo 2. | 879 Undo 2. |

880 (** %\vspace{-.15in}%[[ | 880 (** %\vspace{-.15in}%[[ |

881 pattern nat, n. | 881 pattern nat, n. |

882 ]] | 882 ]] |