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