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

comparison src/Equality.v @ 426:5f25705a10ea

Pass through DataStruct, to incorporate new coqdoc features; globally replace [refl_equal] with [eq_refl]

author	Adam Chlipala <adam@chlipala.net>
date	Wed, 25 Jul 2012 18:10:26 -0400
parents	ff0aef0f33a5
children	5e6b76ca14de

comparison

equal deleted inserted replaced

-:6ed5ee4845e4
+:5f25705a10ea
 match ls return fhlist ls -> fmember ls -> B elm with
 | nil => fun _ idx => match idx with end
 | _ :: ls' => fun mls idx =>
 match idx with
 | inl pf => match pf with
-| refl_equal => fst mls
+| eq_refl => fst mls
 end
 | inr idx' => fhget ls' (snd mls) idx'
 end
 end.
 End fhlist.
 Part of our single remaining subgoal is:
 [[
 a0 : a = elm
 ============================
 match a0 in (_ = a2) return (C a2) with
-| refl_equal => f a1
+| eq_refl => f a1
 end = f match a0 in (_ = a2) return (B a2) with
-| refl_equal => a1
+| eq_refl => a1
 end
 ]]
-This seems like a trivial enough obligation.  The equality proof [a0] must be [refl_equal], since that is the only constructor of [eq].  Therefore, both the [match]es reduce to the point where the conclusion follows by reflexivity.
+This seems like a trivial enough obligation.  The equality proof [a0] must be [eq_refl], since that is the only constructor of [eq].  Therefore, both the [match]es reduce to the point where the conclusion follows by reflexivity.
 [[
 destruct a0.
 ]]
 <<
 User error: Cannot solve a second-order unification problem
 >>
 This is one of Coq's standard error messages for informing us that its heuristics for attempting an instance of an undecidable problem about dependent typing have failed.  We might try to nudge things in the right direction by stating the lemma that we believe makes the conclusion trivial.
 [[
-assert (a0 = refl_equal _).
+assert (a0 = eq_refl _).
 ]]
 <<
-The term "refl_equal ?98" has type "?98 = ?98"
+The term "eq_refl ?98" has type "?98 = ?98"
 while it is expected to have type "a = elm"
 >>
 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!
 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.
+Lemma lemma1 : forall x (pf : x = elm), O = match pf with eq_refl => O end.
 (* begin thide *)
 simple destruct pf; reflexivity.
 Qed.
 (* end thide *)
 Print lemma1.
 (** %\vspace{-.15in}% [[
 lemma1 =
 fun (x : A) (pf : x = elm) =>
 match pf as e in (_ = y) return (0 = match e with
-| refl_equal => 0
+| eq_refl => 0
 end) with
-| refl_equal => refl_equal 0
+| eq_refl => eq_refl 0
 end
 : forall (x : A) (pf : x = elm), 0 = match pf with
-| refl_equal => 0
+| eq_refl => 0
 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
+| eq_refl => 0
 end) with
-| refl_equal => refl_equal 0
+| eq_refl => eq_refl 0
 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 refl_equal => O end.
+Lemma lemma2 : forall (x : A) (pf : x = x), O = match pf with eq_refl => O end.
 (* begin thide *)
 (** %\vspace{-.25in}%[[
 simple destruct pf.
 ]]
 (* begin thide *)
 Definition lemma2 :=
 fun (x : A) (pf : x = x) =>
 match pf return (0 = match pf with
-| refl_equal => 0
+| eq_refl => 0
 end) with
-| refl_equal => refl_equal 0
+| eq_refl => eq_refl 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.
+Lemma lemma3 : forall (x : A) (pf : x = x), pf = eq_refl x.
 (* begin thide *)
 (** %\vspace{-.25in}%[[
 simple destruct pf.
 ]]
 (** This time, even our manual attempt fails.
 [[
 Definition lemma3' :=
 fun (x : A) (pf : x = x) =>
-match pf as pf' in (_ = x') return (pf' = refl_equal x') with
+match pf as pf' in (_ = x') return (pf' = eq_refl x') with
-| refl_equal => refl_equal _
+| eq_refl => eq_refl _
 end.
 ]]
 <<
-The term "refl_equal x'" has type "x' = x'" while it is expected to have type
+The term "eq_refl x'" has type "x' = x'" while it is expected to have type
 "x = x'"
 >>
 The type error comes from our [return] annotation.  In that annotation, the [as]-bound variable [pf'] has type [x = x'], referring to the [in]-bound variable [x'].  To do a dependent [match], we _must_ choose a fresh name for the second argument of [eq].  We are just as constrained to use the %``%#"#real#"#%''% value [x] for the first argument.  Thus, within the [return] clause, the proof we are matching on _must_ equate two non-matching terms, which makes it impossible to equate that proof with reflexivity.
 Nonetheless, it turns out that, with one catch, we _can_ prove this lemma. *)
-Lemma lemma3 : forall (x : A) (pf : x = x), pf = refl_equal x.
+Lemma lemma3 : forall (x : A) (pf : x = x), pf = eq_refl x.
 intros; apply UIP_refl.
 Qed.
 Check UIP_refl.
 (** %\vspace{-.15in}% [[
 UIP_refl
-: forall (U : Type) (x : U) (p : x = x), p = refl_equal x
+: forall (U : Type) (x : U) (p : x = x), p = eq_refl x
 ]]
 The theorem %\index{Gallina terms!UIP\_refl}%[UIP_refl] comes from the [Eqdep] module of the standard library.  Do the Coq authors know of some clever trick for building such proofs that we have not seen yet?  If they do, they did not use it for this proof.  Rather, the proof is based on an _axiom_. *)
 Print eq_rect_eq.
 (* end thide *)
 (** %\vspace{-.15in}% [[
 Streicher_K =
 fun U : Type => UIP_refl__Streicher_K U (UIP_refl U)
 : forall (U : Type) (x : U) (P : x = x -> Prop),
-P (refl_equal x) -> forall p : x = x, P p
+P (eq_refl x) -> forall p : x = x, P p
 ]]
 This is the unfortunately named %\index{axiom K}``%#"#Streicher's axiom K,#"#%''% which says that a predicate on properly typed equality proofs holds of all such proofs if it holds of reflexivity. *)
 End fhlist_map.
 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)
 = match pf in (_ = ls) return fhlist _ ls with
-| refl_equal => fhapp (fhapp hls1 hls2) hls3
+| eq_refl => fhapp (fhapp hls1 hls2) hls3
 end.
 induction ls1; crush.
 (** The first remaining subgoal looks trivial enough:
 [[
 ============================
 fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 =
 match pf in (_ = ls) return (fhlist B ls) with
-| refl_equal => fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3
+| eq_refl => fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3
 end
 ]]
 We can try what worked in previous examples.
 [[
 ============================
 (a0,
 fhapp (ls1:=ls1) (ls2:=ls2 ++ ls3) b
 (fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3)) =
 match pf in (_ = ls) return (fhlist B ls) with
-| refl_equal =>
+| eq_refl =>
 (a0,
 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
 end
 ============================
 (a0,
 fhapp (ls1:=ls1) (ls2:=ls2 ++ ls3) b
 (fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3)) =
 match pf in (_ = ls) return (fhlist B ls) with
-| refl_equal =>
+| eq_refl =>
 (a0,
 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
 end
 ]]
 rewrite (IHls1 _ _ pf').
 (** [[
 ============================
 (a0,
 match pf' in (_ = ls) return (fhlist B ls) with
-| refl_equal =>
+| eq_refl =>
 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3
 end) =
 match pf in (_ = ls) return (fhlist B ls) with
-| refl_equal =>
+| eq_refl =>
 (a0,
 fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
 (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
 end
 ]]
 generalize (fhapp (fhapp b hls2) hls3).
 (** [[
 forall f : fhlist B ((ls1 ++ ls2) ++ ls3),
 (a0,
 match pf' in (_ = ls) return (fhlist B ls) with
-| refl_equal => f
+| eq_refl => f
 end) =
 match pf in (_ = ls) return (fhlist B ls) with
-| refl_equal => (a0, f)
+| eq_refl => (a0, f)
 end
 ]]
 The conclusion has gotten markedly simpler.  It seems counterintuitive that we can have an easier time of proving a more general theorem, but that is exactly the case here and for many other proofs that use dependent types heavily.  Speaking informally, the reason why this kind of activity helps is that [match] annotations only support variables in certain positions.  By reducing more elements of a goal to variables, built-in tactics can have more success building [match] terms under the hood.
 forall (pf0 : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3)
 (pf'0 : (ls1 ++ ls2) ++ ls3 = ls1 ++ ls2 ++ ls3)
 (f : fhlist B ((ls1 ++ ls2) ++ ls3)),
 (a0,
 match pf'0 in (_ = ls) return (fhlist B ls) with
-| refl_equal => f
+| eq_refl => f
 end) =
 match pf0 in (_ = ls) return (fhlist B ls) with
-| refl_equal => (a0, f)
+| eq_refl => (a0, f)
 end
 ]]
 To an experienced dependent types hacker, the appearance of this goal term calls for a celebration.  The formula has a critical property that indicates that our problems are over.  To get our proofs into the right form to apply [UIP_refl], we need to use associativity of list append to rewrite their types.  We could not do that before because other parts of the goal require the proofs to retain their original types.  In particular, the call to [fhapp] that we generalized must have type [(ls1 ++ ls2) ++ ls3], for some values of the list variables.  If we rewrite the type of the proof used to type-cast this value to something like [ls1 ++ ls2 ++ ls3 = ls1 ++ ls2 ++ ls3], then the lefthand side of the equality would no longer match the type of the term we are trying to cast.
 forall (pf0 : a :: ls1 ++ ls2 ++ ls3 = a :: ls1 ++ ls2 ++ ls3)
 (pf'0 : ls1 ++ ls2 ++ ls3 = ls1 ++ ls2 ++ ls3)
 (f : fhlist B (ls1 ++ ls2 ++ ls3)),
 (a0,
 match pf'0 in (_ = ls) return (fhlist B ls) with
-| refl_equal => f
+| eq_refl => f
 end) =
 match pf0 in (_ = ls) return (fhlist B ls) with
-| refl_equal => (a0, f)
+| eq_refl => (a0, f)
 end
 ]]
 We can see that we have achieved the crucial property: the type of each generalized equality proof has syntactically equal operands.  This makes it easy to finish the proof with [UIP_refl]. *)
 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 *)
+(* EX: Prove UIP_refl' : forall (A : Type) (x : A) (pf : x = x), pf == eq_refl x *)
 (* begin thide *)
-Definition UIP_refl' (A : Type) (x : A) (pf : x = x) : pf == refl_equal x :=
+Definition UIP_refl' (A : Type) (x : A) (pf : x = x) : pf == eq_refl x :=
-match pf return (pf == refl_equal _) with
+match pf return (pf == eq_refl _) with
-| refl_equal => JMeq_refl _
+| eq_refl => 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 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.
+O = match pf with eq_refl => O end.
 (* begin thide *)
 intros; rewrite (UIP_refl' pf); reflexivity.
 Qed.
 (* end thide *)
 (* 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 of 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.
+Lemma UIP_refl'' : forall (A : Type) (x : A) (pf : x = x), pf = eq_refl x.
 intros; rewrite (UIP_refl' pf); reflexivity.
 Qed.
 (** The other direction is perhaps more interesting.  Assume that we only have the axiom of the [Eqdep] module available.  We can define [JMeq] in a way that satisfies the same interface as the combination of the [JMeq] module's inductive definition and axiom. *)
 Definition JMeq' (A : Type) (x : A) (B : Type) (y : B) : Prop :=
-exists pf : B = A, x = match pf with refl_equal => y end.
+exists pf : B = A, x = match pf with eq_refl => y end.
 Infix "===" := JMeq' (at level 70, no associativity).
 (** We say that, by definition, [x] and [y] are equal if and only if there exists a proof [pf] that their types are equal, such that [x] equals the result of casting [y] with [pf].  This statement can look strange from the standpoint of classical math, where we almost never mention proofs explicitly with quantifiers in formulas, but it is perfectly legal Coq code.
 We can easily prove a theorem with the same type as that of the [JMeq_refl] constructor of [JMeq]. *)
 (** remove printing exists *)
 Theorem JMeq_refl' : forall (A : Type) (x : A), x === x.
-intros; unfold JMeq'; exists (refl_equal A); reflexivity.
+intros; unfold JMeq'; exists (eq_refl A); reflexivity.
 Qed.
 (** printing exists $\exists$ *)
 (** The proof of an analogue to [JMeq_eq] is a little more interesting, but most of the action is in appealing to [UIP_refl]. *)
 x === y -> x = y.
 unfold JMeq'; intros.
 (** [[
 H : exists pf : A = A,
 x = match pf in (_ = T) return T with
-| refl_equal => y
+| eq_refl => y
 end
 ============================
 x = y
 ]]
 *)
 destruct H.
 (** [[
 x0 : A = A
 H : x = match x0 in (_ = T) return T with
-| refl_equal => y
+| eq_refl => y
 end
 ============================
 x = y
 ]]
 *)
 rewrite H.
 (** [[
 x0 : A = A
 ============================
 match x0 in (_ = T) return T with
-| refl_equal => y
+| eq_refl => y
 end = y
 ]]
 *)
 rewrite (UIP_refl _ _ x0); reflexivity.

Mercurial > cpdt > repo

comparison src/Equality.v @ 426:5f25705a10ea