# Library Cpdt.Equality

# The 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.

Definition pred' (x : nat) :=

match x with

| O => O

| S n' => let y := n' in y

end.

Theorem reduce_me : pred' 1 = 0.

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-need reduction.

cbv delta.

============================

(fun x : nat => match x with

| 0 => 0

| S n' => let y := n' in y

end) 1 = 0

cbv beta.

============================

match 1 with

| 0 => 0

| S n' => let y := n' in y

end = 0

cbv iota.

============================

(fun n' : nat => let y := n' in y) 0 = 0

cbv beta.

============================

(let y := 0 in y) = 0

cbv zeta.

============================

0 = 0

reflexivity.

Qed.

The beta reduction rule applies to recursive functions as well, and its behavior may be surprising in some instances. For instance, we can run some simple tests using the reduction strategy compute, which applies all applicable rules of the definitional equality.

= fun x : nat => (fix id' (n : nat) : nat := n) x

*the top-level structure of the recursive argument is known*. For id' above, we have only one argument n, so clearly it is the recursive argument, and the top-level structure of n is known when the function is applied to O or to some S e term. The variable x is neither, so reduction is blocked.

Fixpoint addLists (ls1 ls2 : list nat) : list nat :=

match ls1, ls2 with

| n1 :: ls1' , n2 :: ls2' => n1 + n2 :: addLists ls1' ls2'

| _, _ => nil

end.

By default, Coq chooses ls1 as the recursive argument. We can see that ls2 would have been another valid choice. The choice has a critical effect on reduction behavior, as these two examples illustrate:

= fun ls : list nat =>

(fix addLists (ls1 ls2 : list nat) : list nat :=

match ls1 with

| nil => nil

| n1 :: ls1' =>

match ls2 with

| nil => nil

| n2 :: ls2' =>

(fix plus (n m : nat) : nat :=

match n with

| 0 => m

| S p => S (plus p m)

end) n1 n2 :: addLists ls1' ls2'

end

end) ls nil

Fixpoint addLists' (ls1 ls2 : list nat) {struct ls2} : list nat :=

match ls1, ls2 with

| n1 :: ls1' , n2 :: ls2' => n1 + n2 :: addLists' ls1' ls2'

| _, _ => nil

end.

Eval compute in fun ls => addLists' ls nil.

= fun ls : list nat => match ls with

| nil => nil

| _ :: _ => nil

end

*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.

# Heterogeneous Lists Revisited

Section fhlist.

Variable A : Type.

Variable B : A -> Type.

Fixpoint fhlist (ls : list A) : Type :=

match ls with

| nil => unit

| x :: ls' => B x * fhlist ls'

end%type.

Variable elm : A.

Fixpoint fmember (ls : list A) : Type :=

match ls with

| nil => Empty_set

| x :: ls' => (x = elm) + fmember ls'

end%type.

Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=

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

| eq_refl => fst mls

end

| inr idx' => fhget ls' (snd mls) idx'

end

end.

End fhlist.

Arguments fhget [A B elm ls] _ _.

Section fhlist_map.

Variables A : Type.

Variables B C : A -> Type.

Variable f : forall x, B x -> C x.

Fixpoint fhmap (ls : list A) : fhlist B ls -> fhlist C ls :=

match ls return fhlist B ls -> fhlist C ls with

| nil => fun _ => tt

| _ :: _ => fun hls => (f (fst hls), fhmap _ (snd hls))

end.

Arguments fhmap [ls] _.

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, which sets us on a collision course with the problems that are the subject of this chapter.

Variable elm : A.

Theorem fhget_fhmap : forall ls (mem : fmember elm ls) (hls : fhlist B ls),

fhget (fhmap hls) mem = f (fhget hls mem).

induction ls; crush.

a0 : a = elm

============================

match a0 in (_ = a2) return (C a2) with

| eq_refl => f a1

end = f match a0 in (_ = a2) return (B a2) with

| eq_refl => a1

end

destruct a0.

User error: Cannot solve a second-order unification problem

assert (a0 = eq_refl _).

The term "eq_refl ?98" has type "?98 = ?98" while it is expected to have type "a = elm"

case a0.

============================

f a1 = f a1

reflexivity.

Qed.

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 eq_refl => O end.

simple destruct pf; reflexivity.

Qed.

The tactic simple destruct pf is a convenient form for applying case. It runs intro to bring into scope all quantified variables up to its argument.

lemma1 =

fun (x : A) (pf : x = elm) =>

match pf as e in (_ = y) return (0 = match e with

| eq_refl => 0

end) with

| eq_refl => eq_refl 0

end

: forall (x : A) (pf : x = elm), 0 = match pf with

| eq_refl => 0

end

Definition lemma1' (x : A) (pf : x = elm) :=

match pf return (0 = match pf with

| eq_refl => 0

end) with

| eq_refl => eq_refl 0

end.

Surprisingly, what seems at first like a

*simpler*lemma is harder to prove.
Abort.

Nonetheless, we can adapt the last manual proof to handle this theorem.

Definition lemma2 :=

fun (x : A) (pf : x = x) =>

match pf return (0 = match pf with

| eq_refl => 0

end) with

| eq_refl => eq_refl 0

end.

We can try to prove a lemma that would simplify proofs of many facts like lemma2:

Abort.

This time, even our manual attempt fails.

Definition lemma3' :=

fun (x : A) (pf : x = x) =>

match pf as pf' in (_ = x') return (pf' = eq_refl x') with

| eq_refl => eq_refl _

end.
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
Nonetheless, it turns out that, with one catch, we

Definition lemma3' :=

fun (x : A) (pf : x = x) =>

match pf as pf' in (_ = x') return (pf' = eq_refl x') with

| eq_refl => eq_refl _

end.

The term "eq_refl x'" has type "x' = x'" while it is expected to have type "x = x'"

*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.*can*prove this lemma.Lemma lemma3 : forall (x : A) (pf : x = x), pf = eq_refl x.

intros; apply UIP_refl.

Qed.

Check UIP_refl.

UIP_refl

: forall (U : Type) (x : U) (p : x = x), p = eq_refl x

*axiom*, the term eq_rect_eq below.

Print eq_rect_eq.

*** [ eq_rect_eq :

forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),

x = eq_rect p Q x p h ]

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).

= forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),

x = match h in (_ = y) return (Q y) with

| eq_refl => x

end

*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, in a study that also established unprovability of the axiom in CIC.

Check Streicher_K.

Streicher_K

: forall (U : Type) (x : U) (P : x = x -> Prop),

P eq_refl -> forall p : x = x, P p

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.
Sometimes we need to use tricks with equality just to state the theorems that we care about. To illustrate, we start by defining a concatenation function for fhlists.

# Type-Casts in Theorem Statements

Section fhapp.

Variable A : Type.

Variable B : A -> Type.

Fixpoint fhapp (ls1 ls2 : list A)

: fhlist B ls1 -> fhlist B ls2 -> fhlist B (ls1 ++ ls2) :=

match ls1 with

| nil => fun _ hls2 => hls2

| _ :: _ => fun hls1 hls2 => (fst hls1, fhapp _ _ (snd hls1) hls2)

end.

Arguments fhapp [ls1 ls2] _ _.

We might like to prove that fhapp is associative.

Theorem fhapp_assoc : 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.
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

Theorem fhapp_assoc : 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.

The term "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)"

*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_assoc : 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

| 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

| eq_refl => fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3

end
We can try what worked in previous examples.

case pf.
It seems we have reached another case where it is unclear how to use a dependent match to implement case analysis on our proof. The UIP_refl theorem can come to our rescue again.

============================

fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 =

match pf in (_ = ls) return (fhlist B ls) with

| eq_refl => fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3

end

case pf.

User error: Cannot solve a second-order unification problem

rewrite (UIP_refl _ _ pf).

============================

fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 =

fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3

reflexivity.

Our second subgoal is trickier.

pf : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3

============================

(a0,

fhapp (ls1:=ls1) (ls2:=ls2 ++ ls3) b

(fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3)) =

match pf in (_ = ls) return (fhlist B ls) with

| eq_refl =>

(a0,

fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)

(fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)

end

rewrite (UIP_refl _ _ pf).
We can only apply UIP_refl on proofs of equality with syntactically equal operands, which is not the case of pf here. We will need to manipulate the form of this subgoal to get us to a point where we may use UIP_refl. A first step is obtaining a proof suitable to use in applying the induction hypothesis. Inversion on the structure of pf is sufficient for that.

pf : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3

============================

(a0,

fhapp (ls1:=ls1) (ls2:=ls2 ++ ls3) b

(fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3)) =

match pf in (_ = ls) return (fhlist B ls) with

| eq_refl =>

(a0,

fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)

(fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)

end

rewrite (UIP_refl _ _ pf).

The term "pf" has type "a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3" while it is expected to have type "?556 = ?556"

injection pf; intro pf'.

pf : a :: (ls1 ++ ls2) ++ ls3 = a :: ls1 ++ ls2 ++ ls3

pf' : (ls1 ++ ls2) ++ ls3 = ls1 ++ ls2 ++ ls3

============================

(a0,

fhapp (ls1:=ls1) (ls2:=ls2 ++ ls3) b

(fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3)) =

match pf in (_ = ls) return (fhlist B ls) with

| 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

| 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

| eq_refl =>

(a0,

fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)

(fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)

end

*does not matter what the result of the call is*. In other words, the subgoal should remain true if we replace this fhapp call with a fresh variable. The generalize tactic helps us do exactly that.

forall f : fhlist B ((ls1 ++ ls2) ++ ls3),

(a0,

match pf' in (_ = ls) return (fhlist B ls) with

| eq_refl => f

end) =

match pf in (_ = ls) return (fhlist B ls) with

| eq_refl => (a0, f)

end

generalize pf pf'.

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

| eq_refl => f

end) =

match pf0 in (_ = ls) return (fhlist B ls) with

| eq_refl => (a0, f)

end

*may be rewritten as well*. In particular, the final masterstroke is rewriting everywhere in our goal using associativity of list append.

rewrite app_assoc.

============================

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

| eq_refl => f

end) =

match pf0 in (_ = ls) return (fhlist B ls) with

| eq_refl => (a0, f)

end

intros.

rewrite (UIP_refl _ _ pf0).

rewrite (UIP_refl _ _ pf'0).

reflexivity.

Qed.

End fhapp.

Arguments fhapp [A B ls1 ls2] _ _.

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.
There is another equality predicate, defined in the JMeq module of the standard library, implementing

# Heterogeneous Equality

*heterogeneous equality*.Print JMeq.

Inductive JMeq (A : Type) (x : A) : forall B : Type, B -> Prop :=

JMeq_refl : JMeq x x

*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).

Definition UIP_refl' (A : Type) (x : A) (pf : x = x) : pf == eq_refl x :=

match pf return (pf == eq_refl _) with

| eq_refl => JMeq_refl _

end.

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 eq_refl => O end.

intros; rewrite (UIP_refl' pf); reflexivity.

Qed.

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.

JMeq_eq

: forall (A : Type) (x y : A), x == y -> x = y

This time, the naive theorem statement type-checks.

Theorem fhapp_assoc' : 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.

Even better, crush discharges the first subgoal automatically. The second subgoal is:

============================

(a0, fhapp b (fhapp hls2 hls3)) == (a0, fhapp (fhapp b hls2) hls3)
It looks like one rewrite with the inductive hypothesis should be enough to make the goal trivial. Here is what happens when we try that in Coq 8.2:

rewrite IHls1.
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.

============================

(a0, fhapp b (fhapp hls2 hls3)) == (a0, fhapp (fhapp b hls2) hls3)

rewrite IHls1.

Error: Impossible to unify "fhlist B ((ls1 ++ ?1572) ++ ?1573)" with "fhlist B (ls1 ++ ?1572 ++ ?1573)"

============================

forall (f : fhlist B (ls1 ++ ls2 ++ ls3))

(f0 : fhlist B ((ls1 ++ ls2) ++ ls3)), f == f0 -> (a0, f) == (a0, f0)

rewrite app_assoc.

============================

forall f f0 : fhlist B (ls1 ++ ls2 ++ ls3), f == f0 -> (a0, f) == (a0, f0)

This example illustrates a general pattern: heterogeneous equality often simplifies theorem statements, but we still need to do some work to line up some dependent pattern matches that tactics will generate for us.
The proof we have found relies on the JMeq_eq axiom, which we can verify with a command that we will discuss more in two chapters.

Axioms:

JMeq_eq : forall (A : Type) (x y : A), x == y -> x = y

Lemma pair_cong : forall A1 A2 B1 B2 (x1 : A1) (x2 : A2) (y1 : B1) (y2 : B2),

x1 == x2

-> y1 == y2

-> (x1, y1) == (x2, y2).

intros until y2; intros Hx Hy; rewrite Hx; rewrite Hy; reflexivity.

Qed.

Hint Resolve pair_cong.

Section fhapp''.

Variable A : Type.

Variable B : A -> Type.

Theorem fhapp_assoc'' : 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.

Qed.

End fhapp''.

Print Assumptions fhapp_assoc''.

Closed under the global context

Check eq_ind_r.

eq_ind_r

: forall (A : Type) (x : A) (P : A -> Prop),

P x -> forall y : A, y = x -> P y

internal_JMeq_rew_r

: forall (A : Type) (x : A) (B : Type) (b : B)

(P : forall B0 : Type, B0 -> Type), P B b -> x == b -> P A x

*its type*. In other words, the predicate must be

*polymorphic*in y's type; any type must make sense, from a type-checking standpoint. There may be cases where the former rearrangement is easy to do in a type-correct way, but the second rearrangement done naively leads to a type error.

Check JMeq_ind_r.

JMeq_ind_r

: forall (A : Type) (x : A) (P : A -> Prop),

P x -> forall y : A, y == x -> P y

Applying JMeq_ind_r is easy, as the pattern tactic will transform the goal into an application of an appropriate fun to a term that we want to abstract. (In general, pattern abstracts over a term by introducing a new anonymous function taking that term as argument.)

pattern n.

apply JMeq_ind_r with (x := m); auto.

However, we run into trouble trying to get the goal into a form compatible with the alternative principle.

Undo 2.

pattern nat, n.

Error: The abstracted term "fun (P : Set) (n0 : P) => S n0 == S m" is not well typed. Illegal application (Type Error): The term "S" of type "nat -> nat" cannot be applied to the term "n0" : "P" This term has type "P" which should be coercible to "nat".

Abort.

Why did we not run into this problem in our proof of fhapp_assoc''? The reason is that the pair constructor is polymorphic in the types of the pair components, while functions like S are not polymorphic at all. Use of such non-polymorphic functions with JMeq tends to push toward use of axioms. The example with nat here is a bit unrealistic; more likely cases would involve functions that have

*some*polymorphism, but not enough to allow abstractions of the sort we attempted above with pattern. For instance, we might have an equality between two lists, where the goal only type-checks when the terms involved really are lists, though everything is polymorphic in the types of list data elements. The Heq library builds up a slightly different foundation to help avoid such problems.# Equivalence of Equality Axioms

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 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 = 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 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.

Theorem JMeq_refl' : forall (A : Type) (x : A), x === x.

intros; unfold JMeq'; exists (eq_refl A); reflexivity.

Qed.

The proof of an analogue to JMeq_eq is a little more interesting, but most of the action is in appealing to UIP_refl.

H : exists pf : A = A,

x = match pf in (_ = T) return T with

| eq_refl => y

end

============================

x = y

destruct H.

x0 : A = A

H : x = match x0 in (_ = T) return T with

| eq_refl => y

end

============================

x = y

rewrite H.

rewrite (UIP_refl _ _ x0); reflexivity.

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 interconvert 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.

# Equality of Functions

Theorem two_funs : (fun n => n) = (fun n => n + 0).

*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.

Require Import FunctionalExtensionality.

About functional_extensionality.

functional_extensionality :

forall (A B : Type) (f g : A -> B), (forall x : A, f x = g x) -> f = g

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

| S _ => True

end)

= (forall _ : nat, True).

There are no immediate opportunities to apply functional_extensionality, but we can use change to fix that problem.

change ((forall x : nat, (fun x => match x with

| 0 => True

| S _ => True

end) x) = (nat -> True)).

rewrite (functional_extensionality (fun x => match x with

| 0 => True

| S _ => True

end) (fun _ => True)).

2 subgoals

============================

(nat -> True) = (nat -> True)

subgoal 2 is:

forall x : nat, match x with

| 0 => True

| S _ => True

end = True

reflexivity.

destruct x; constructor.

Qed.

Unlike in the case of eq_rect_eq, we have no way of deriving this axiom of

*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.