35 lines
No EOL
1,020 B
Agda
35 lines
No EOL
1,020 B
Agda
module equality where
|
|
-- in this module we define propositional equality and some helper syntax.
|
|
|
|
infix 4 _≡_
|
|
data _≡_ {A : Set} (a : A) : A → Set where
|
|
instance refl : a ≡ a
|
|
{-# BUILTIN EQUALITY _≡_ #-}
|
|
|
|
-- ≡ is a equivalence relation
|
|
sym : ∀ {A : Set} {x y : A} → x ≡ y → y ≡ x
|
|
sym refl = refl
|
|
|
|
trans : ∀ {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
|
|
trans refl refl = refl
|
|
|
|
cong : ∀ {A B : Set} (f : A → B) {x y} → x ≡ y → f x ≡ f y
|
|
cong f refl = refl
|
|
|
|
-- Equational reasoning
|
|
infix 3 _∎
|
|
infixr 2 _≡⟨⟩_ step-≡
|
|
infix 1 begin_
|
|
begin_ : ∀ {A : Set} {x y : A} → x ≡ y → x ≡ y
|
|
begin x = x
|
|
|
|
_≡⟨⟩_ : ∀ {A : Set} (x y : A) → x ≡ y → x ≡ y
|
|
_ ≡⟨⟩ _ = λ x → x
|
|
|
|
_∎ : ∀ {A : Set} (x : A) → x ≡ x
|
|
_ ∎ = refl
|
|
|
|
step-≡ : ∀ {A : Set} (x {y z} : A) → y ≡ z → x ≡ y → x ≡ z
|
|
step-≡ _ y≡z x≡y = trans x≡y y≡z
|
|
|
|
syntax step-≡ x eq1 eq2 = x ≡⟨ eq2 ⟩ eq1 |