Equality Rules

There are rules for both definitionally equality and propositional equality

Rules for Definitionally Equality

The rules must be normalising so,

As an example, a rule for symmetry x=y -> y=x can't be a definitionally equality rule and so must be a propositional equality rule because:

Rules for Propositional Equality

The rules are used to prove equality so its harder to have some automatic algorithm and so the programmer needs to apply the rules as required to do the proof.

Substitution

There seems to be at least 2 sorts of rules we can apply to equations:

If we substitute, in a term M all occurrences of
context variable x by a term N of the same type
as x, then the result is the same type - it will remain true.

Γright adjointN:σ Γ,x:σ, Δright adjointM
Γ,Δ[N/x]right adjointM[N/x]

example where:

  • N= y+1
  • M = a x² + b x + c
subst

Substitution happens in function application (that is, when deconstructing a function.

See β-reduction in λ-calulus.

(λ x:σ.N) M

Definition of 'subst'.

subst takes T x to T y.

We can think of T x as being an expression in x. So subst takes an expression in x to an expression in y.

right adjointq:(x=y)right adjointT : A -> Typeright adjointt :T x
subst q T t : T y
subst

Below is the computational rule where the two values are already definitionaly equal. Here refl (propositional equality) is embedded into this definitionaly equality.

(subst (refl x x) T t)=t : T x

subst

Also we can replace like for like in equations (is this substitution?).

Rewriting in Logic

Rewriting an expression into a logically equivalent one.

example: ¬A /\ ¬B -> ¬(A \/ B)

Computation rule

Refl disappears when properties are definitionaly equal.

subst (Refl P)=P

 

Substitution in Agda
id:{A: Set}->A->A
_==_:{A: Set}->A->A->Set
 subst:{A: Set} (C:A->Set) {x y:A}->x==y->C x->C y
 
subst : forall {x y} -> x == y -> x -> y
subst refl x = x

 

Substitution in Idris (replace)
||| Perform substitution in a term according to some equality.
replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y
replace Refl prf = prf

 

Substitution as a fibration

subst
example subst

 


metadata block
see also:
Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

flag flag flag flag flag flag Computation and Reasoning - This book is about type theory. Although it is very technical it is aimed at computer scientists, so it has more discussion than a book aimed at pure mathematicians. It is especially useful for the coverage of dependant types.

 

Terminology and Notation

Specific to this page here:

 

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2022 Martin John Baker - All rights reserved - privacy policy.