blob: ba7560647293f4ae63d27956edc6bc4a9b7fd72b (
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
34
35
36
37
38
39
40
41
|
{-# OPTIONS --without-K --safe #-}
module Cfe.Vec.Relation.Binary.Pointwise.Inductive where
open import Data.Fin using (toℕ; zero; suc)
open import Data.Nat using (ℕ; suc; _≟_; pred)
open import Data.Vec using (Vec; insert; remove)
open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise; []; _∷_)
open import Function using (_|>_)
open import Level using (Level)
open import Relation.Binary using (REL; Antisym)
open import Relation.Binary.PropositionalEquality using (cong)
open import Relation.Nullary.Decidable using (True; toWitness; fromWitness)
private
variable
a b ℓ : Level
A : Set a
B : Set b
_∼_ : REL A B ℓ
m n : ℕ
antisym :
∀ {P : REL A B ℓ} {Q : REL B A ℓ} {R : REL A B ℓ} →
Antisym P Q R → Antisym (Pointwise P {m} {n}) (Pointwise Q) (Pointwise R)
antisym anti [] [] = []
antisym anti (x ∷ xs) (y ∷ ys) = anti x y ∷ antisym anti xs ys
Pointwise-insert :
∀ {xs : Vec A m} {ys : Vec B n} → ∀ i j {i≡j : True (toℕ i ≟ toℕ j)} {x y} →
x ∼ y → Pointwise _∼_ xs ys → Pointwise _∼_ (insert xs i x) (insert ys j y)
Pointwise-insert zero zero x xs = x ∷ xs
Pointwise-insert (suc i) (suc j) {i≡j} x (y ∷ xs) =
y ∷ Pointwise-insert i j {i≡j |> toWitness |> cong pred |> fromWitness} x xs
Pointwise-remove :
∀ {xs : Vec A (suc m)} {ys : Vec B (suc n)} → ∀ i j {i≡j : True (toℕ i ≟ toℕ j)} →
Pointwise _∼_ xs ys → Pointwise _∼_ (remove xs i) (remove ys j)
Pointwise-remove zero zero (_ ∷ xs) = xs
Pointwise-remove (suc i) (suc j) {i≡j} (x ∷ y ∷ xs) =
x ∷ Pointwise-remove i j {i≡j |> toWitness |> cong pred |> fromWitness} (y ∷ xs)
|
