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

comparison src/Equality.v @ 437:8077352044b2

A pass over all formatting, after big pile of coqdoc changes

author	Adam Chlipala <adam@chlipala.net>
date	Fri, 27 Jul 2012 16:47:28 -0400
parents	5d5e44f905c7
children	0d66f1a710b8

comparison

equal deleted inserted replaced

-:5d5e44f905c7
+:8077352044b2
 | n1 :: ls1' , n2 :: ls2' => n1 + n2 :: addLists' ls1' ls2'
 | _, _ => nil
 end.
 (* begin hide *)
-Definition foo := @eq.
+(* begin thide *)
+Definition foo := (@eq, plus).
+(* end thide *)
 (* end hide *)
 Eval compute in fun ls => addLists' ls nil.
 (** %\vspace{-.15in}%[[
 = fun ls : list nat => match ls with
 End fhlist.
 Implicit Arguments fhget [A B elm ls].
 (* begin hide *)
+(* begin thide *)
 Definition map := O.
+(* end thide *)
 (* end hide *)
 (** We can define a [map]-like function for [fhlist]s. *)
 Section fhlist_map.
 end.
 Implicit Arguments fhmap [ls].
 (* begin hide *)
+(* begin thide *)
 Definition ilist := O.
 Definition get := O.
 Definition imap := O.
+(* end thide *)
 (* end hide *)
 (** For the inductive versions of the [ilist] definitions, we proved a lemma about the interaction of [get] and [imap].  It was a strategic choice not to attempt such a proof for the definitions that we just gave, because that sets us on a collision course with the problems that are the subject of this chapter. *)
 Variable elm : A.
 (* end thide *)
 (** We can try to prove a lemma that would simplify proofs of many facts like [lemma2]: *)
 (* begin hide *)
+(* begin thide *)
 Definition lemma3' := O.
+(* end thide *)
 (* end hide *)
 Lemma lemma3 : forall (x : A) (pf : x = x), pf = eq_refl x.
 (* begin thide *)
 (** %\vspace{-.25in}%[[
 ]]
 The axiom %\index{Gallina terms!eq\_rect\_eq}%[eq_rect_eq] states a "fact" that seems like common sense, once the notation is deciphered.  The term [eq_rect] is the automatically generated recursion principle for [eq].  Calling [eq_rect] is another way of [match]ing on an equality proof.  The proof we match on is the argument [h], and [x] is the body of the [match].  The statement of [eq_rect_eq] just says that [match]es on proofs of [p = p], for any [p], are superfluous and may be removed.  We can see this intuition better in code by asking Coq to simplify the theorem statement with the [compute] reduction strategy (which, by the way, applies all applicable rules of the definitional equality presented in this chapter's first section). *)
 (* begin hide *)
+(* begin thide *)
 Definition False' := False.
+(* end thide *)
 (* end hide *)
 Eval compute in (forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
 x = eq_rect p Q x p h).
 (** %\vspace{-.15in}%[[
 Perhaps surprisingly, we cannot prove [eq_rect_eq] from within Coq.  This proposition is introduced as an %\index{axioms}%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 _inconsistent_ 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%~\cite{AxiomK}%, in a study that also established unprovability of the axiom in CIC.
 This axiom is equivalent to another that is more commonly known and mentioned in type theory circles. *)
 (* begin hide *)
-Definition Streicher_K' := (Streicher_K, UIP_refl__Streicher_K).
+(* begin thide *)
+Definition Streicher_K' := UIP_refl__Streicher_K.
+(* end thide *)
 (* end hide *)
 Print Streicher_K.
 (* end thide *)
 (** %\vspace{-.15in}% [[
 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.
 (* begin hide *)
+(* begin thide *)
 Require Eqdep_dec.
+(* end thide *)
 (* end hide *)
 (** 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.  To simplify presentation, we will stick with the axiom version in the rest of this chapter. *)

Mercurial > cpdt > repo

comparison src/Equality.v @ 437:8077352044b2