latte-prelude.equal

The formal definition of equality, and its basic properties.

decompose-equal-type

(decompose-equal-type def-env ctx t)

eq-cong

(eq-cong [f (==> T U)] [eq (equal x y)])

Proves (equal (f x) (f y)) by congruence of equal, cf. eq-cong-prop.

eq-cong-prop

(eq-cong-prop [f (==> T U)] [x T] [y T])

(==> (equal x y) (equal (f x) (f y)))

Theorem: Congruence property of equality.

eq-intro

(eq-intro [x ?T] [y ?T])

Introduction rule for equal. The type parameter T is implicit, cf. eq-intro-thm for the explicit version.

eq-intro-thm

(eq-intro-thm [T :type] [x T] [y T])

(==> (forall [P (==> T :type)] (<=> (P x) (P y))) (equal x y))

Theorem: Introduction rule for equal. This is useful because equality is opaque by default.

eq-refl

(eq-refl [x ?T])

Equality is reflexive, cf. eq-refl-thm.

eq-refl-thm

(eq-refl-thm [T :type] [x T])

(equal x x)

Theorem: The reflexivity property of equality.

eq-subst

(eq-subst [P (==> T :type)] [eq (equal x y)] [Px (P x)])

Proves (P y) given the fact that (equal x y) and (P x)

This is thanks to substitutivity of equal, cf. eq-subst-prop.

eq-subst-prop

(eq-subst-prop [P (==> T :type)] [x T] [y T])

(==> (equal x y) (P x) (P y))

Theorem: Substitutivity property of equality. This is the main elimination rule.

eq-sym

(eq-sym [eq-proof (equal x y)])

Proves (equal y x) from eq-proof by symmetry of equality, cf. eq-sym-thm.

eq-sym-thm

(eq-sym-thm [T :type] [x T] [y T])

(==> (equal x y) (equal y x))

Theorem: The symmetry property of equality.

eq-trans

(eq-trans [eq1 (equal x y)] [eq2 (equal y z)])

Proves (equal x z) from eq1 and eq2 by transitivity of equal, cf. eq-trans-thm.

eq-trans*

(eq-trans* [eq1 (equal x1 x2)] [eq2 (equal x2 x3)] ... [eqN (equal xN_1 xN)])

Transitivity of equal, a n-ary version of eq-trans.

For example:

(eq-trans* eq1 eq2)
==> (eq-trans eq1 eq2)

(eq-trans* eq1 eq2 eq3)
==> (eq-trans (eq-trans eq1 eq2) eq3)

(eq-trans* eq1 eq2 eq3 eq4)
==> (eq-trans (eq-trans (eq-trans eq1 eq2) eq3) eq4)

etc. `

eq-trans-thm

(eq-trans-thm [T :type] [x T] [y T] [z T])

(==> (equal x y) (equal y z) (equal x z))

Theorem: The transitivity property of equality.

equal

Equality of x and y (which must be of the same type T). This is an implicit version of equality.

equality

(equality [T :type] [x T] [y T])

(forall [P (==> T :type)] (<=> (P x) (P y)))

Definition: The intuitionistic, second-order definition of equality. This corresponds to Leibniz’s indiscernibility of identicals.

nrewrite

(nrewrite n-th [Px (P x)] [eq (equal x y)])

Proves (P y) from proofs of (P x) and (equal x y). The difference with eq-subst is that we try to infer the property P.

This method rewrites the n-th occurrence of (type type of) x in P (in prefix ordering), starting from 1.

The method (rewrite <Px> <eq-xy>) is the same as (and is preferable to) (nrewrite 1 <Px> <eq-xy>)

nrewrite-impl

(nrewrite-impl def-env ctx n [Px Px-type] [eq-xy eq-xy-type])

Core implementation of rewriting.

rewrite

(rewrite [Px (P x)] [eq (equal x y)])