Certified Programming with Dependent Types: src/Equality.v comparison

comparison src/Equality.v @ 456:848bf35f7f6c

Proofreading pass through Chapter 10

author	Adam Chlipala <adam@chlipala.net>
date	Tue, 28 Aug 2012 11:48:06 -0400
parents	0d66f1a710b8
children	4320c1a967c2

comparison

equal deleted inserted replaced

-:df0a45de158a
+:848bf35f7f6c
 (* end hide *)
 (** %\chapter{Reasoning About Equality Proofs}% *)
-(** In traditional mathematics, the concept of equality is usually taken as a given.  On the other hand, in type theory, equality is a very contentious subject.  There are at least three different notions of equality that are important, and researchers are actively investigating new definitions of what it means for two terms to be equal.  Even once we fix a notion of equality, there are inevitably tricky issues that arise in proving properties of programs that manipulate equality proofs explicitly.  In this chapter, I will focus on design patterns for circumventing these tricky issues, and I will introduce the different notions of equality as they are germane. *)
+(** In traditional mathematics, the concept of equality is usually taken as a given.  On the other hand, in type theory, equality is a very contentious subject.  There are at least three different notions of equality that are important in Coq, and researchers are actively investigating new definitions of what it means for two terms to be equal.  Even once we fix a notion of equality, there are inevitably tricky issues that arise in proving properties of programs that manipulate equality proofs explicitly.  In this chapter, I will focus on design patterns for circumventing these tricky issues, and I will introduce the different notions of equality as they are germane. *)
 (** * The Definitional Equality *)
 (** We have seen many examples so far where proof goals follow "by computation."  That is, we apply computational reduction rules to reduce the goal to a normal form, at which point it follows trivially.  Exactly when this works and when it does not depends on the details of Coq's%\index{definitional equality}% _definitional equality_.  This is an untyped binary relation appearing in the formal metatheory of CIC.  CIC contains a typing rule allowing the conclusion [E : T] from the premise [E : T'] and a proof that [T] and [T'] are definitionally equal.
 ]]
 Using what we know about shorthands for [match] annotations, we can write this proof in shorter form manually. *)
 (* begin thide *)
-Definition lemma1' :=
+Definition lemma1' (x : A) (pf : x = elm) :=
-fun (x : A) (pf : x = elm) =>
+match pf return (0 = match pf with
-match pf return (0 = match pf with
+| eq_refl => 0
-| eq_refl => 0
+end) with
-end) with
+| eq_refl => eq_refl 0
-| eq_refl => eq_refl 0
+end.
-end.
 (* end thide *)
 (** Surprisingly, what seems at first like a _simpler_ lemma is harder to prove. *)
 Lemma lemma2 : forall (x : A) (pf : x = x), O = match pf with eq_refl => O end.
 (** %\vspace{-.15in}% [[
 Inductive JMeq (A : Type) (x : A) : forall B : Type, B -> Prop :=
 JMeq_refl : JMeq x x
 ]]
-The identity [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. *)
+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. *)
 Infix "==" := JMeq (at level 70, no associativity).
 (* EX: Prove UIP_refl' : forall (A : Type) (x : A) (pf : x = x), pf == eq_refl x *)
 (* begin thide *)
 Print Assumptions fhapp_ass''.
 (** <<
 Closed under the global context
 >>
-One might wonder exactly which elements of a proof involving [JMeq] imply that [JMeq_eq] must be used.  For instance, above we noticed that [rewrite] had brought [JMeq_eq] into the proof of [fhap_ass'], yet here we have also used [rewrite] with [JMeq] hypotheses while avoiding axioms!  One illuminating exercise is comparing the types of the lemmas that [rewrite] uses under the hood to implement the rewrites.  Here is the normal lemma for [eq] rewriting:%\index{Gallina terms!eq\_ind\_r}% *)
+One might wonder exactly which elements of a proof involving [JMeq] imply that [JMeq_eq] must be used.  For instance, above we noticed that [rewrite] had brought [JMeq_eq] into the proof of [fhapp_ass'], yet here we have also used [rewrite] with [JMeq] hypotheses while avoiding axioms!  One illuminating exercise is comparing the types of the lemmas that [rewrite] uses under the hood to implement the rewrites.  Here is the normal lemma for [eq] rewriting:%\index{Gallina terms!eq\_ind\_r}% *)
 Check eq_ind_r.
 (** %\vspace{-.15in}%[[
 eq_ind_r
 : forall (A : Type) (x : A) (P : A -> Prop),
 (** * Equality of Functions *)
 (** The following seems like a reasonable theorem to want to hold, and it does hold in set theory.
 %\vspace{-.15in}%[[
-Theorem two_identities : (fun n => n) = (fun n => n + 0).
+Theorem two_funs : (fun n => n) = (fun n => n + 0).
 ]]
 %\vspace{-.15in}%Unfortunately, this theorem is not provable in CIC without additional axioms.  None of the definitional equality rules force function equality to be%\index{extensionality of function equality}% _extensional_.  That is, the fact that two functions return equal results on equal inputs does not imply that the functions are equal.  We _can_ assert function extensionality as an axiom, and indeed the standard library already contains that axiom. *)
 Require Import FunctionalExtensionality.
 About functional_extensionality.
 functional_extensionality :
 forall (A B : Type) (f g : A -> B), (forall x : A, f x = g x) -> f = g
 ]]
 *)
-(** This axiom has been verified metatheoretically to be consistent with CIC and the two equality axioms we considered previously.  With it, the proof of [two_identities] is trivial. *)
+(** This axiom has been verified metatheoretically to be consistent with CIC and the two equality axioms we considered previously.  With it, the proof of [two_funs] is trivial. *)
-Theorem two_identities : (fun n => n) = (fun n => n + 0).
+Theorem two_funs : (fun n => n) = (fun n => n + 0).
 (* begin thide *)
 apply functional_extensionality; crush.
 Qed.
 (* end thide *)
 | O => True
 | S _ => True
 end)
 = (forall _ : nat, True).
-(** There are no immediate opportunities to apply [ext_eq], but we can use %\index{tactics!change}%[change] to fix that. *)
+(** There are no immediate opportunities to apply [functional_extensionality], but we can use %\index{tactics!change}%[change] to fix that problem. *)
 (* begin thide *)
 change ((forall x : nat, (fun x => match x with
 | 0 => True
 | S _ => True

Mercurial > cpdt > repo

comparison src/Equality.v @ 456:848bf35f7f6c