-- The equality precidate: data _==_ : ∀ {A : Set} -> A -> A -> Set where refl : ∀ {A : Set} -> ∀ {x : A} -> x == x -- Things we still need to talk about: -- -- * Better notation for equality ✓ -- * Theorems, such as transitivity, symmetry, and other properties of equality -- * How to prove inequality -- * More convenient syntactic sugar for equality proofs -- Symmetry of equality is a theorem. symm : ∀ {A : Set} -> ∀ {x y : A} -> x == y -> y == x symm {A} {x} {.x} refl = refl -- A dot pattern, such as .x, means that it is an argument to a -- function which Agda already knows must be equal to x. -- Transitivity is also a theorem. trans : ∀ {A : Set} -> ∀ {x y z : A} -> x == y -> y == z -> x == z trans {A} {x} {.x} {.x} refl refl = refl -- Replacing equals by equals in an equation. "If x == y, then f x == -- f y for any context f" context : ∀ {A B : Set} -> ∀ {x y : A} -> ∀ (f : A -> B) -> x == y -> f x == f y context {A} {B} {x} {.x} f refl = refl -- Replacing equals by equals in a predicate. "If x == y, then you can -- substitute y for x in any predicate". subst : ∀ {A : Set} -> ∀ (C : A -> Set) -> ∀ {x y : A} -> x == y -> C x -> C y subst {A} C {x} {.x} refl hyp-c = hyp-c -- C-c C-f: move the cursor to the next goal ("forward") -- C-c C-b: move the cursor to the previous goal ("back") -- For example, if you know x == y, and you need to prove succ x == succ y, -- "context" is the way to prove it. -- context : a == b -> f a == f b -- commutative : x + y == y + x -- -- lemma : (x + y) + z == (y + x) + z -- lemma = context (\a -> a + z) commutative -- subst : a == b -> C a -> C b