blob: 56a2c7792232929800bbde3566a050f09c85c9a9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
{-# OPTIONS --without-K --safe #-}
module Cfe.Fin.Properties where
open import Cfe.Fin.Base
open import Data.Fin using (zero; suc; toℕ)
open import Data.Nat using (suc; pred)
open import Relation.Binary.PropositionalEquality
inject<!-cong : ∀ {n i j k l} → toℕ< {i = i} k ≡ toℕ< {i = j} l → inject<! {n} k ≡ inject<! l
inject<!-cong {suc _} {k = zero} {zero} _ = refl
inject<!-cong {suc _} {k = suc k} {suc l} k≡l = cong suc (inject<!-cong (cong pred k≡l))
raise>-cong : ∀ {n i j k l} → toℕ> {i = i} k ≡ toℕ> {i = j} l → raise> {n} k ≡ raise> l
raise>-cong {suc _} {k = zero} {zero} _ = refl
raise>-cong {suc _} {k = suc k} {suc l} k≡l = cong suc (raise>-cong (cong pred k≡l))
raise>-cong {suc _} {k = suc k} {inj l} k≡l = cong suc (raise>-cong (cong pred k≡l))
raise>-cong {suc _} {k = inj k} {suc l} k≡l = cong suc (raise>-cong (cong pred k≡l))
raise>-cong {suc _} {k = inj k} {inj l} k≡l = cong suc (raise>-cong (cong pred k≡l))
toℕ>-suc> : ∀ {n} j → toℕ> (suc> {suc n} j) ≡ toℕ> (suc j)
toℕ>-suc> zero = refl
toℕ>-suc> (suc j) = cong suc (toℕ>-suc> j)
toℕ<-inject<! : ∀ {n i} j → toℕ (inject<! {n} {i} j) ≡ toℕ< j
toℕ<-inject<! {suc n} zero = refl
toℕ<-inject<! {suc n} (suc j) = cong suc (toℕ<-inject<! j)
toℕ>-cast>-inject<! : ∀ {n i} j k → toℕ> k ≡ toℕ> (cast>-inject<! {n} {i} j k)
toℕ>-cast>-inject<! zero zero = refl
toℕ>-cast>-inject<! zero (suc k) = cong suc (toℕ>-cast>-inject<! zero k)
toℕ>-cast>-inject<! {suc n} zero (inj k) = cong suc (toℕ>-cast>-inject<! zero k)
toℕ>-cast>-inject<! {suc n} (suc j) (inj k) = cong suc (toℕ>-cast>-inject<! j k)
|
