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

comparison src/Equality.v @ 124:57eaceb085f6

Templatize Equality

author	Adam Chlipala <adamc@hcoop.net>
date	Mon, 20 Oct 2008 09:11:54 -0400
parents	9ccd215e5112
children	0bfc75502498

comparison

equal deleted inserted replaced

-:9ccd215e5112
+:57eaceb085f6
 | O => O
 | S n' => let y := n' in y
 end.
 Theorem reduce_me : pred' 1 = 0.
+(* begin thide *)
 (** CIC follows the traditions of lambda calculus in associating reduction rules with Greek letters.  Coq can certainly be said to support the familiar alpha reduction rule, which allows capture-avoiding renaming of bound variables, but we never need to apply alpha explicitly, since Coq uses a de Bruijn representation that encodes terms canonically.
 The delta rule is for unfolding global definitions.  We can use it here to unfold the definition of [pred'].  We do this with the [cbv] tactic, which takes a list of reduction rules and makes as many call-by-value reduction steps as possible, using only those rules.  There is an analogous tactic [lazy] for call-by-name reduction. *)
 cbv delta.
 0 = 0
 ]] *)
 reflexivity.
 Qed.
+(* end thide *)
 (** The standard [eq] relation is critically dependent on the definitional equality.  [eq] is often called a %\textit{%#<i>#propositional equality#</i>#%}%, 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, we will introduce effective proof methods for goals that use proofs of the standard propositional equality "as data." *)
 Variable elm : A.
 Theorem get_imap : forall ls (mem : fmember elm ls) (hls : fhlist B ls),
 fhget (fhmap hls) mem = f (fhget hls mem).
+(* begin thide *)
 induction ls; crush.
 (** Part of our single remaining subgoal is:
 [[
 It seems that [destruct] was trying to be too smart for its own good. *)
 reflexivity.
 Qed.
+(* end thide *)
 (** It will be helpful to examine the proof terms generated by this sort of strategy.  A simpler example illustrates what is going on. *)
 Lemma lemma1 : forall x (pf : x = elm), O = match pf with refl_equal => O end.
+(* begin thide *)
 simple destruct pf; reflexivity.
 Qed.
+(* end thide *)
 (** [simple destruct pf] is a convenient form for applying [case].  It runs [intro] to bring into scope all quantified variables up to its argument. *)
 Print lemma1.
 end
 ]]
 Using what we know about shorthands for [match] annotations, we can write this proof in shorter form manually. *)
+(* begin thide *)
 Definition lemma1' :=
 fun (x : A) (pf : x = elm) =>
 match pf return (0 = match pf with
 | refl_equal => 0
 end) with
 | refl_equal => refl_equal 0
 end.
+(* end thide *)
 (** Surprisingly, what seems at first like a %\textit{%#<i>#simpler#</i>#%}% lemma is harder to prove. *)
 Lemma lemma2 : forall (x : A) (pf : x = x), O = match pf with refl_equal => O end.
+(* begin thide *)
 (** [[
 simple destruct pf.
 [[
 ]] *)
 Abort.
 (** Nonetheless, we can adapt the last manual proof to handle this theorem. *)
-Definition lemma2' :=
+(* begin thide *)
+Definition lemma2 :=
 fun (x : A) (pf : x = x) =>
 match pf return (0 = match pf with
 | refl_equal => 0
 end) with
 | refl_equal => refl_equal 0
 end.
+(* end thide *)
 (** We can try to prove a lemma that would simplify proofs of many facts like [lemma2]: *)
 Lemma lemma3 : forall (x : A) (pf : x = x), pf = refl_equal x.
+(* begin thide *)
 (** [[
 simple destruct pf.
 [[
 Perhaps surprisingly, we cannot prove [eq_rect_eq] from within Coq.  This proposition is introduced as an axiom; that is, a proposition asserted as true without proof.  We cannot assert just any statement without proof.  Adding [False] as an axiom would allow us to prove any proposition, for instance, defeating the point of using a proof assistant.  In general, we need to be sure that we never assert %\textit{%#<i>#inconsistent#</i>#%}% sets of axioms.  A set of axioms is inconsistent if its conjunction implies [False].  For the case of [eq_rect_eq], consistency has been verified outside of Coq via "informal" metatheory.
 This axiom is equivalent to another that is more commonly known and mentioned in type theory circles. *)
 Print Streicher_K.
+(* end thide *)
 (** [[
 Streicher_K =
 fun U : Type => UIP_refl__Streicher_K U (UIP_refl U)
 : forall (U : Type) (x : U) (P : x = x -> Prop),
 | nil => fun _ hls2 => hls2
 | _ :: _ => fun hls1 hls2 => (fst hls1, fhapp _ _ (snd hls1) hls2)
 end.
 Implicit Arguments fhapp [ls1 ls2].
+(* EX: Prove that fhapp is associative. *)
+(* begin thide *)
 (** We might like to prove that [fhapp] is associative.
 [[
 intros.
 rewrite (UIP_refl _ _ pf0).
 rewrite (UIP_refl _ _ pf'0).
 reflexivity.
 Qed.
+(* end thide *)
 End fhapp.
 Implicit Arguments fhapp [A B ls1 ls2].
 [JMeq] stands for "John Major equality," a name coined by Conor McBride 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] %\textit{%#<i>#on arguments of different types#</i>#%}%.  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 *)
 Definition UIP_refl' (A : Type) (x : A) (pf : x = x) : pf == refl_equal x :=
 match pf return (pf == refl_equal _) with
 | refl_equal => JMeq_refl _
 end.
+(* end thide *)
 (** There is no quick way to write such a proof by tactics, but the underlying proof term that we want is trivial.
 Suppose that we want to use [UIP_refl'] to establish another lemma of the kind of we have run into several times so far. *)
 Lemma lemma4 : forall (A : Type) (x : A) (pf : x = x),
 O = match pf with refl_equal => O end.
+(* begin thide *)
 intros; rewrite (UIP_refl' pf); reflexivity.
 Qed.
+(* end thide *)
 (** All in all, refreshingly straightforward, but there really is no such thing as a free lunch.  The use of [rewrite] is implemented in terms of an axiom: *)
 Check JMeq_eq.
 (** [[
 Variable A : Type.
 Variable B : A -> Type.
 (** This time, the naive theorem statement type-checks. *)
+(* EX: Prove [fhapp] associativity using [JMeq]. *)
+(* begin thide *)
 Theorem fhapp_ass' : forall ls1 ls2 ls3
 (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
 fhapp hls1 (fhapp hls2 hls3) == fhapp (fhapp hls1 hls2) hls3.
 induction ls1; crush.
 From this point, the goal is trivial. *)
 intros f f0 H; rewrite H; reflexivity.
 Qed.
+(* end thide *)
 End fhapp'.
 (** * Equivalence of Equality Axioms *)
+(* EX: Show that the approaches based on K and JMeq are equivalent logically. *)
+(* begin thide *)
 (** Assuming axioms (like axiom K and [JMeq_eq]) is a hazardous business.  The due diligence associated with it is necessarily global in scope, since two axioms may be consistent alone but inconsistent together.  It turns out that all of the major axioms proposed for reasoning about equality in Coq are logically equivalent, so that we only need to pick one to assert without proof.  In this section, we demonstrate this by showing how each the previous two sections' approaches reduces to the other logically.
 To show that [JMeq] and its axiom let us prove [UIP_refl], we start from the lemma [UIP_refl'] from the previous section.  The rest of the proof is trivial. *)
 Lemma UIP_refl'' : forall (A : Type) (x : A) (pf : x = x), pf = refl_equal x.
 Qed.
 (** We see that, in a very formal sense, we are free to switch back and forth between the two styles of proofs about equality proofs.  One style may be more convenient than the other for some proofs, but we can always intercovert between our results.  The style that does not use heterogeneous equality may be preferable in cases where many results do not require the tricks of this chapter, since then the use of axioms is avoided altogether for the simple cases, and a wider audience will be able to follow those "simple" proofs.  On the other hand, heterogeneous equality often makes for shorter and more readable theorem statements.
 It is worth remarking that it is possible to avoid axioms altogether for equalities on types with decidable equality.  The [Eqdep_dec] module of the standard library contains a parametric proof of [UIP_refl] for such cases. *)
+(* end thide *)
 (** * 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).
 Unfortunately, this theorem is not provable in CIC without additional axioms.  None of the definitional equality rules force function equality to be %\textit{%#<i>#extensional#</i>#%}%.  That is, the fact that two functions return equal results on equal inputs does not imply that the functions are equal.  We %\textit{%#<i>#can#</i>#%}% assert function extensionality as an axiom. *)
+(* begin thide *)
 Axiom ext_eq : forall A B (f g : A -> B),
 (forall x, f x = g x)
 -> f = g.
+(* end thide *)
 (** 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).
+(* begin thide *)
 apply ext_eq; reflexivity.
 Qed.
+(* end thide *)
 (** The same axiom can help us prove equality of types, where we need to "reason under quantifiers." *)
 Theorem forall_eq : (forall x : nat, match x with
 | O => True
 end)
 = (forall _ : nat, True).
 (** There are no immediate opportunities to apply [ext_eq], but we can use [change] to fix that. *)
+(* 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
 reflexivity.
 destruct x; constructor.
 Qed.
+(* end thide *)

Mercurial > cpdt > repo

comparison src/Equality.v @ 124:57eaceb085f6