DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Add a lemma about chains of length h+1

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2023-09-16 00:23:30 -07:00
parent 266c3dd81e
commit 866bc9124a
1 changed files with 8 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
Chain.agda
View File

@ -7,8 +7,10 @@ module Chain {a} {A : Set a}
(R-≈-cong : ∀ {a₁ a₁' a₂ a₂'} → a₁ ≈ a₁' → a₂ ≈ a₂' → a₁ R a₂ → a₁' R a₂') where (R-≈-cong : ∀ {a₁ a₁' a₂ a₂'} → a₁ ≈ a₁' → a₂ ≈ a₂' → a₁ R a₂ → a₁' R a₂') where
open import Data.Nat as Nat using (ℕ; suc; _+_; _≤_) open import Data.Nat as Nat using (ℕ; suc; _+_; _≤_)
open import Data.Nat.Properties using (+-comm; m+1+n≰m)
open import Data.Product using (_×_; Σ; _,_) open import Data.Product using (_×_; Σ; _,_)
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
open import Data.Empty using (⊥)
open IsEquivalence ≈-equiv open IsEquivalence ≈-equiv
@ -36,5 +38,11 @@ module _ where
Bounded : ℕ → Set a Bounded : ℕ → Set a
Bounded bound = ∀ {a₁ a₂ : A} {n : ℕ} → Chain a₁ a₂ n → n ≤ bound Bounded bound = ∀ {a₁ a₂ : A} {n : ℕ} → Chain a₁ a₂ n → n ≤ bound
Bounded-suc-n : ∀ {a₁ a₂ : A} {n : ℕ} → Bounded n → Chain a₁ a₂ (suc n) → ⊥
Bounded-suc-n {a₁} {a₂} {n} bounded c = (m+1+n≰m n n+1≤n)
where
n+1≤n : n + 1 ≤ n
n+1≤n rewrite (+-comm n 1) = bounded c
Height : ℕ → Set a Height : ℕ → Set a
Height height = (Σ (A × A) (λ (a₁ , a₂) → Chain a₁ a₂ height) × Bounded height) Height height = (Σ (A × A) (λ (a₁ , a₂) → Chain a₁ a₂ height) × Bounded height)