Templatize Equality

src/Equality.v

@@ -34,6 +34,7 @@ Definition pred' (x : nat) :=
   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. *)
@@ -89,6 +90,7 @@ Theorem reduce_me : pred' 1 = 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.
 
@@ -153,6 +155,7 @@ Section fhlist_map.
 
   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:
@@ -206,12 +209,15 @@ The term "refl_equal ?98" has type "?98 = ?98"
 
     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. *)
 
@@ -233,6 +239,7 @@ 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
@@ -240,10 +247,12 @@ end
                            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.
@@ -256,17 +265,20 @@ User error: Cannot solve a second-order unification problem
 
   (** 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.
@@ -326,6 +338,7 @@ fun U : Type => Eq_rect_eq.eq_rect_eq U
       This axiom is equivalent to another that is more commonly known and mentioned in type theory circles. *)
 
   Print Streicher_K.
+(* end thide *)
 (** [[
 
 Streicher_K = 
@@ -356,6 +369,9 @@ Section fhapp.
 
   Implicit Arguments fhapp [ls1 ls2].
 
+  (* EX: Prove that fhapp is associative. *)
+(* begin thide *)
+
   (** We might like to prove that [fhapp] is associative.
 
      [[
@@ -543,6 +559,7 @@ The term "pf" has type "a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3"
     rewrite (UIP_refl _ _ pf'0).
     reflexivity.
   Qed.
+(* end thide *)
 End fhapp.
 
 Implicit Arguments fhapp [A B ls1 ls2].
@@ -563,10 +580,13 @@ Inductive JMeq (A : Type) (x : A) : forall B : Type, B -> Prop :=
 
 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.
 
@@ -574,8 +594,10 @@ Definition UIP_refl' (A : Type) (x : A) (pf : x = x) : pf == refl_equal x :=
 
 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: *)
 
@@ -596,6 +618,9 @@ Section fhapp'.
 
   (** 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.
@@ -653,11 +678,15 @@ Error: Impossible to unify "fhlist B ((ls1 ++ ?1572) ++ ?1573)" with
 
     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. *)
@@ -726,6 +755,7 @@ 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 *)
@@ -736,15 +766,19 @@ Qed.
 
    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." *)
 
@@ -756,6 +790,7 @@ Theorem forall_eq : (forall x : nat, match x with
 
   (** 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
@@ -783,4 +818,4 @@ subgoal 2 is:
 
   destruct x; constructor.
 Qed.
-
+(* end thide *)