# Equality in Coq

*formal proofs*of the corresponding statements ─ data structures that can be inspected to build other proofs. It is not a coincidence that function types and logical implication use the same notation, A -> B, because proofs of implication in Coq

*are*functions: they take proofs of the precondition as inputs and return a proof of the consequent as the output. Such proofs are written with the same language we use for programming in Coq; tactics are but scripts that build such programs for us. A proof that implication is transitive, for example, amounts to function composition.

Definition implication_is_transitive (A B C : Prop) :

(A -> B) -> (B -> C) -> (A -> C) :=

fun HAB HBC HA => HBC (HAB HA).

Definition or_false_r (A : Prop) : A \/ False -> A :=

fun (H : A \/ False) =>

match H with

| or_introl HA => HA

| or_intror contra => match contra with end

end.

## Defining equality

Inductive eq (T : Type) (x : T) : T -> Prop :=

| eq_refl : eq T x x.

*non-uniform*indexed proposition ─ that is, the value of its last argument is not fixed for the whole declaration, but depends on the constructor used. (This non-uniformity is what allows us to put two occurrences of x on the type of eq_refl.)

Definition rewriting

(T : Type) (P : T -> Prop) (x y : T) (p : x = y) (H : P x) : P y :=

match p in _ = z return P z with

| eq_refl => H

end.

Definition etrans {T} {x y z : T} (p : x = y) (q : y = z) : x = z :=

match p in _ = w return w = z -> x = z with

| eq_refl => fun q' : x = z => q'

end q.

Definition esym {T} {x y : T} (p : x = y) : y = x :=

match p in _ = z return z = x with

| eq_refl => eq_refl

end.

*convoy pattern*, a term coined by Adam Chlipala in his CDPT book.

Definition eq_Sn_m (n m : nat) (p : S n = m) :=

match p in _ = k return match k with

| 0 => False

| S m' => n = m'

end with

| eq_refl => eq_refl

end.

Definition succ_not_zero n : S n <> 0 :=

eq_Sn_m n 0.

Definition succ_inj n m : S n = S m -> n = m :=

eq_Sn_m n (S m).

## Mixing proofs and computation

From mathcomp Require Import seq.

Definition first {T} (s : seq T) (Hs : s <> [::]) : T :=

match s return s <> [::] -> T with

| [::] => fun Hs : [::] <> [::] => match Hs eq_refl with end

| x :: _ => fun _ => x

end Hs.

Definition first' {T} (s : {s : seq T | s <> [::]}) : T :=

match s with

| exist s Hs => first s Hs

end.

*proof irrelevance*axiom without compromising its soundness. This axiom says that any two proofs of the same proposition are equal.

Axiom proof_irrelevance : forall (P : Prop) (p q : P), p = q.

## Proof irrelevance and equality

*provided that*T has decidable equality. Many useful properties can be expressed in this way; in particular, any boolean function f : S -> bool can be seen as a predicate S -> Prop defined as fun x : S => f x = true. Thus, if we restrict subset types to

*computable*predicates, we do not need to worry about the proofs that appear in its elements.

Section Irrelevance.

Variable T : Type.

Implicit Types x y : T.

Definition almost_irrelevance :

(forall x (p : x = x), p = eq_refl x) ->

(forall x y (p q : x = y), p = q) :=

fun H x y p q =>

match q in _ = z return forall p' : x = z, p' = q with

| eq_refl => fun p' => H x p'

end p.

Fail Definition irrelevance x (p : x = x) : p = eq_refl x :=

match p in _ = y return p = eq_refl x with

| eq_refl => eq_refl

end.

*univalence principle*that says that proofs of equality between two types correspond to isomorphisms between them. Since there are often many different isomorphisms between two types, irrelevance cannot hold in full generality.

Hypothesis eq_dec : forall x y, x = y \/ x <> y.

Definition normalize {x y} (p : x = y) : x = y :=

match eq_dec x y with

| or_introl e => e

| or_intror _ => p

end.

Lemma normalize_const {x y} (p q : x = y) : normalize p = normalize q.

Proof. by rewrite /normalize; case: (eq_dec x y). Qed.

Notation "p * q" := (etrans p q).

Notation "p ^-1" := (esym p)

(at level 3, left associativity, format "p ^-1").

Definition denormalize {x y} (p : x = y) := p * (normalize (eq_refl y))^-1.

Definition etransK x y (p : x = y) : p * p^-1 = eq_refl x :=

match p in _ = y return p * p^-1 = eq_refl x with

| eq_refl => eq_refl (eq_refl x)

end.

Definition normalizeK x y (p : x = y) :

normalize p * (normalize (eq_refl y))^-1 = p :=

match p in _ = y return normalize p * (normalize (eq_refl y))^-1 = p with

| eq_refl => etransK x x (normalize (eq_refl x))

end.

Lemma irrelevance x y (p q : x = y) : p = q.

Proof.

by rewrite -[LHS]normalizeK -[RHS]normalizeK (normalize_const p q).

Qed.

End Irrelevance.