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

comparison src/Equality.v @ 407:ff0aef0f33a5

Typesetting pass over Equality

author	Adam Chlipala <adam@chlipala.net>
date	Fri, 08 Jun 2012 14:45:22 -0400
parents	05efde66559d
children	5f25705a10ea

comparison

equal deleted inserted replaced

-:fc03a67810e8
+:ff0aef0f33a5
 (** 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. *)
 (** * 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.
+(** 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.
 The %\index{tactics!cbv}%[cbv] tactic will help us illustrate the rules of Coq's definitional equality.  We redefine the natural number predecessor function in a somewhat convoluted way and construct a manual proof that it returns [0] when applied to [1]. *)
 Definition pred' (x : nat) :=
 match x with
 Recall that co-recursive definitions have a dual rule: a co-recursive call only simplifies when it is the discriminee of a [match].  This condition is built into the beta rule for %\index{Gallina terms!cofix}%[cofix], the anonymous form of [CoFixpoint].
 %\medskip%
-The standard [eq] relation is critically dependent on the definitional equality.  The relation [eq] is often called a %\index{propositional equality}%_propositional equality_, because it reifies definitional equality as a proposition that may or may not hold.  Standard axiomatizations of an equality predicate in first-order logic define equality in terms of properties it has, like reflexivity, symmetry, and transitivity.  In contrast, for [eq] in Coq, those properties are implicit in the properties of the definitional equality, which are built into CIC's metatheory and the implementation of Gallina.  We could add new rules to the definitional equality, and [eq] would keep its definition and methods of use.
+The standard [eq] relation is critically dependent on the definitional equality.  The relation [eq] is often called a%\index{propositional equality}% _propositional equality_, because it reifies definitional equality as a proposition that may or may not hold.  Standard axiomatizations of an equality predicate in first-order logic define equality in terms of properties it has, like reflexivity, symmetry, and transitivity.  In contrast, for [eq] in Coq, those properties are implicit in the properties of the definitional equality, which are built into CIC's metatheory and the implementation of Gallina.  We could add new rules to the definitional equality, and [eq] would keep its definition and methods of use.
 This all may make it sound like the choice of [eq]'s definition is unimportant.  To the contrary, in this chapter, we will see examples where alternate definitions may simplify proofs.  Before that point, I will introduce proof methods for goals that use proofs of the standard propositional equality %``%#"#as data.#"#%''% *)
 (** * Heterogeneous Lists Revisited *)
 In retrospect, the problem is not so hard to see.  Reflexivity proofs only show [x = x] for particular values of [x], whereas here we are thinking in terms of a proof of [a = elm], where the two sides of the equality are not equal syntactically.  Thus, the essential lemma we need does not even type-check!
 Is it time to throw in the towel?  Luckily, the answer is %``%#"#no.#"#%''%  In this chapter, we will see several useful patterns for proving obligations like this.
-For this particular example, the solution is surprisingly straightforward.  [destruct] has a simpler sibling [case] which should behave identically for any inductive type with one constructor of no arguments.
+For this particular example, the solution is surprisingly straightforward.  The [destruct] tactic has a simpler sibling [case] which should behave identically for any inductive type with one constructor of no arguments.
 [[
 case a0.
 ============================
 f a1 = f a1
 "fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3) (fhapp (ls1:=ls1) (ls2:=ls2) hls1 hls2)
 hls3" has type "fhlist B ((ls1 ++ ls2) ++ ls3)"
 while it is expected to have type "fhlist B (ls1 ++ ls2 ++ ls3)"
 >>
-This first cut at the theorem statement does not even type-check.  We know that the two [fhlist] types appearing in the error message are always equal, by associativity of normal list append, but this fact is not apparent to the type checker.  This stems from the fact that Coq's equality is %\index{intensional type theory}%_intensional_, in the sense that type equality theorems can never be applied after the fact to get a term to type-check.  Instead, we need to make use of equality explicitly in the theorem statement. *)
+This first cut at the theorem statement does not even type-check.  We know that the two [fhlist] types appearing in the error message are always equal, by associativity of normal list append, but this fact is not apparent to the type checker.  This stems from the fact that Coq's equality is%\index{intensional type theory}% _intensional_, in the sense that type equality theorems can never be applied after the fact to get a term to type-check.  Instead, we need to make use of equality explicitly in the theorem statement. *)
 Theorem fhapp_ass : forall ls1 ls2 ls3
 (pf : (ls1 ++ ls2) ++ ls3 = ls1 ++ (ls2 ++ ls3))
 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
 fhapp hls1 (fhapp hls2 hls3)
 (** This proof strategy was cumbersome and unorthodox, from the perspective of mainstream mathematics.  The next section explores an alternative that leads to simpler developments in some cases. *)
 (** * Heterogeneous Equality *)
-(** There is another equality predicate, defined in the %\index{Gallina terms!JMeq}%[JMeq] module of the standard library, implementing %\index{heterogeneous equality}%_heterogeneous equality_. *)
+(** There is another equality predicate, defined in the %\index{Gallina terms!JMeq}%[JMeq] module of the standard library, implementing%\index{heterogeneous equality}% _heterogeneous equality_. *)
 Print JMeq.
 (** %\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.  [JMeq] starts out looking a lot like [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 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. *)
 Infix "==" := JMeq (at level 70, no associativity).
 (* EX: Prove UIP_refl' : forall (A : Type) (x : A) (pf : x = x), pf == refl_equal x *)
 (* begin thide *)
 <<
 Error: Impossible to unify "fhlist B ((ls1 ++ ?1572) ++ ?1573)" with
 "fhlist B (ls1 ++ ?1572 ++ ?1573)"
 >>
-Coq 8.3 currently gives an error message about an uncaught exception.  Perhaps that will be fixed soon.  In any case, it is educational to consider a more explicit approach.
+Coq 8.4 currently gives an error message about an uncaught exception.  Perhaps that will be fixed soon.  In any case, it is educational to consider a more explicit approach.
 We see that [JMeq] is not a silver bullet.  We can use it to simplify the statements of equality facts, but the Coq type-checker uses non-trivial heterogeneous equality facts no more readily than it uses standard equality facts.  Here, the problem is that the form [(e1, e2)] is syntactic sugar for an explicit application of a constructor of an inductive type.  That application mentions the type of each tuple element explicitly, and our [rewrite] tries to change one of those elements without updating the corresponding type argument.
 We can get around this problem by another multiple use of [generalize].  We want to bring into the goal the proper instance of the inductive hypothesis, and we also want to generalize the two relevant uses of [fhapp]. *)
 (** * Equality of Functions *)
 (** The following seems like a reasonable theorem to want to hold, and it does hold in set theory. [[
-Theorem S_eta : S = (fun n => S n).
+Theorem two_identities : (fun n => n) = (fun n => n + 0).
 ]]
-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. *)
+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. *)
-(* begin thide *)
+Require Import FunctionalExtensionality.
-Axiom ext_eq : forall A B (f g : A -> B),
+About functional_extensionality.
-(forall x, f x = g x)
+(** %\vspace{-.15in}%[[
--> f = g.
+functional_extensionality :
-(* end thide *)
+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 [S_eta] is trivial. *)
-Theorem S_eta : S = (fun n => S n).
+Theorem two_identities : (fun n => n) = (fun n => n + 0).
 (* begin thide *)
-apply ext_eq; reflexivity.
+apply functional_extensionality; crush.
 Qed.
 (* end thide *)
 (** The same axiom can help us prove equality of types, where we need to %``%#"#reason under quantifiers.#"#%''% *)
 (* begin thide *)
 change ((forall x : nat, (fun x => match x with
 | 0 => True
 | S _ => True
 end) x) = (nat -> True)).
-rewrite (ext_eq (fun x => match x with
+rewrite (functional_extensionality (fun x => match x with
 | 0 => True
 | S _ => True
 end) (fun _ => True)).
 (** [[
 2 subgoals
 ============================
 (nat -> True) = (nat -> True)
 destruct x; constructor.
 Qed.
 (* end thide *)
-(** Unlike in the case of [eq_rect_eq], we have no way of deriving this axiom of %\index{functional extensionality}%_functional extensionality_ for types with decidable equality.  To allow equality reasoning without axioms, it may be worth rewriting a development to replace functions with alternate representations, such as finite map types for which extensionality is derivable in CIC. *)
+(** Unlike in the case of [eq_rect_eq], we have no way of deriving this axiom of%\index{functional extensionality}% _functional extensionality_ for types with decidable equality.  To allow equality reasoning without axioms, it may be worth rewriting a development to replace functions with alternate representations, such as finite map types for which extensionality is derivable in CIC. *)

Mercurial > cpdt > repo

comparison src/Equality.v @ 407:ff0aef0f33a5