From 866bc9124aa2ba4d7120e3f7b15f4d9537b92745 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 16 Sep 2023 00:23:30 -0700 Subject: [PATCH] Add a lemma about chains of length h+1 Signed-off-by: Danila Fedorin --- Chain.agda | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/Chain.agda b/Chain.agda index b1778d4..8aaf247 100644 --- a/Chain.agda +++ b/Chain.agda @@ -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 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 Relation.Binary.PropositionalEquality as Eq using (_≡_; refl) +open import Data.Empty using (⊥) open IsEquivalence ≈-equiv @@ -36,5 +38,11 @@ module _ where Bounded : ℕ → Set a 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 height = (Σ (A × A) (λ (a₁ , a₂) → Chain a₁ a₂ height) × Bounded height)