{-# OPTIONS --cubical-compatible --safe #-}
{-# OPTIONS --warn=noUserWarning #-}
module Data.Fin.Induction where
open import Data.Fin.Base using (Fin; zero; suc; _<_; toℕ; inject₁;
_≥_; _>_; fromℕ; _≺_)
open import Data.Fin.Properties using (toℕ-inject₁; ≤-refl; <-cmp;
toℕ≤n; toℕ-injective; toℕ-fromℕ; toℕ-lower₁; inject₁-lower₁;
pigeonhole; ≺⇒<′)
open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _∸_; s≤s)
open import Data.Nat.Properties using (n<1+n; ≤⇒≯)
import Data.Nat.Induction as ℕ
import Data.Nat.Properties as ℕ
open import Data.Product.Base using (_,_)
open import Data.Vec.Base as Vec using (Vec; []; _∷_)
open import Data.Vec.Relation.Unary.Linked as Linked using (Linked; [-]; _∷_)
import Data.Vec.Relation.Unary.Linked.Properties as Linked
open import Function.Base using (flip; _$_)
open import Induction using (RecStruct)
open import Induction.WellFounded as WF using (WellFounded; WfRec;
module Subrelation)
open import Level using (Level)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Bundles using (StrictPartialOrder)
open import Relation.Binary.Structures using (IsPartialOrder; IsStrictPartialOrder)
open import Relation.Binary.Definitions using (Decidable)
import Relation.Binary.Construct.Flip.EqAndOrd as EqAndOrd
import Relation.Binary.Construct.Flip.Ord as Ord
import Relation.Binary.Construct.NonStrictToStrict as ToStrict
import Relation.Binary.Construct.On as On
open import Relation.Binary.Definitions using (Tri; tri<; tri≈; tri>)
open import Relation.Binary.PropositionalEquality.Core
using (_≡_; refl; sym; subst; trans; cong)
open import Relation.Nullary.Decidable using (yes; no)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Unary using (Pred)
private
variable
ℓ : Level
n : ℕ
open WF public using (Acc; acc)
<-wellFounded : WellFounded {A = Fin n} _<_
<-wellFounded = On.wellFounded toℕ ℕ.<-wellFounded
<-weakInduction-startingFrom : ∀ (P : Pred (Fin (suc n)) ℓ) →
∀ {i} → P i →
(∀ j → P (inject₁ j) → P (suc j)) →
∀ {j} → j ≥ i → P j
<-weakInduction-startingFrom P {i} Pi Pᵢ⇒Pᵢ₊₁ {j} j≥i = induct (<-wellFounded _) (<-cmp i j) j≥i
where
induct : ∀ {j} → Acc _<_ j → Tri (i < j) (i ≡ j) (i > j) → j ≥ i → P j
induct (acc rs) (tri≈ _ refl _) i≤j = Pi
induct (acc rs) (tri> _ _ i>sj) i≤j with () ← ≤⇒≯ i≤j i>sj
induct {suc j} (acc rs) (tri< (s≤s i≤j) _ _) _ = Pᵢ⇒Pᵢ₊₁ j P[1+j]
where
toℕj≡toℕinjJ = sym $ toℕ-inject₁ j
P[1+j] = induct (rs (s≤s (subst (ℕ._≤ toℕ j) toℕj≡toℕinjJ ≤-refl)))
(<-cmp i $ inject₁ j) (subst (toℕ i ℕ.≤_) toℕj≡toℕinjJ i≤j)
<-weakInduction : (P : Pred (Fin (suc n)) ℓ) →
P zero →
(∀ i → P (inject₁ i) → P (suc i)) →
∀ i → P i
<-weakInduction P P₀ Pᵢ⇒Pᵢ₊₁ i = <-weakInduction-startingFrom P P₀ Pᵢ⇒Pᵢ₊₁ ℕ.z≤n
private
acc-map : ∀ {x : Fin n} → Acc ℕ._<_ (n ∸ toℕ x) → Acc _>_ x
acc-map (acc rs) = acc λ y>x → acc-map (rs (ℕ.∸-monoʳ-< y>x (toℕ≤n _)))
>-wellFounded : WellFounded {A = Fin n} _>_
>-wellFounded {n} x = acc-map (ℕ.<-wellFounded (n ∸ toℕ x))
>-weakInduction : (P : Pred (Fin (suc n)) ℓ) →
P (fromℕ n) →
(∀ i → P (suc i) → P (inject₁ i)) →
∀ i → P i
>-weakInduction {n = n} P Pₙ Pᵢ₊₁⇒Pᵢ i = induct (>-wellFounded i)
where
induct : ∀ {i} → Acc _>_ i → P i
induct {i} (acc rec) with n ℕ.≟ toℕ i
... | yes n≡i = subst P (toℕ-injective (trans (toℕ-fromℕ n) n≡i)) Pₙ
... | no n≢i = subst P (inject₁-lower₁ i n≢i) (Pᵢ₊₁⇒Pᵢ _ Pᵢ₊₁)
where Pᵢ₊₁ = induct (rec (ℕ.≤-reflexive (cong suc (sym (toℕ-lower₁ i n≢i)))))
module _ {_≈_ : Rel (Fin n) ℓ} where
spo-wellFounded : ∀ {r} {_⊏_ : Rel (Fin n) r} →
IsStrictPartialOrder _≈_ _⊏_ → WellFounded _⊏_
spo-wellFounded {_} {_⊏_} isSPO i = go n pigeon where
module ⊏ = IsStrictPartialOrder isSPO
go : ∀ m {i} →
({xs : Vec (Fin n) m} → Linked (flip _⊏_) (i ∷ xs) → WellFounded _⊏_) →
Acc _⊏_ i
go zero k = k [-] _
go (suc m) k = acc λ j⊏i → go m λ i∷xs↑ → k (j⊏i ∷ i∷xs↑)
pigeon : {xs : Vec (Fin n) n} → Linked (flip _⊏_) (i ∷ xs) → WellFounded _⊏_
pigeon {xs} i∷xs↑ =
let (i₁ , i₂ , i₁<i₂ , xs[i₁]≡xs[i₂]) = pigeonhole (n<1+n n) (Vec.lookup (i ∷ xs)) in
let xs[i₁]⊏xs[i₂] = Linked.lookup⁺ (Ord.transitive _⊏_ ⊏.trans) i∷xs↑ i₁<i₂ in
let xs[i₁]⊏xs[i₁] = ⊏.<-respʳ-≈ (⊏.Eq.reflexive xs[i₁]≡xs[i₂]) xs[i₁]⊏xs[i₂] in
contradiction xs[i₁]⊏xs[i₁] (⊏.irrefl ⊏.Eq.refl)
po-wellFounded : ∀ {r} {_⊑_ : Rel (Fin n) r} →
IsPartialOrder _≈_ _⊑_ → WellFounded (ToStrict._<_ _≈_ _⊑_)
po-wellFounded isPO =
spo-wellFounded (ToStrict.<-isStrictPartialOrder _≈_ _ isPO)
spo-noetherian : ∀ {r} {_⊏_ : Rel (Fin n) r} →
IsStrictPartialOrder _≈_ _⊏_ → WellFounded (flip _⊏_)
spo-noetherian isSPO = spo-wellFounded (EqAndOrd.isStrictPartialOrder isSPO)
po-noetherian : ∀ {r} {_⊑_ : Rel (Fin n) r} → IsPartialOrder _≈_ _⊑_ →
WellFounded (flip (ToStrict._<_ _≈_ _⊑_))
po-noetherian isPO =
spo-noetherian (ToStrict.<-isStrictPartialOrder _≈_ _ isPO)
≺-Rec : RecStruct ℕ ℓ ℓ
≺-Rec = WfRec _≺_
≺-wellFounded : WellFounded _≺_
≺-wellFounded = Subrelation.wellFounded ≺⇒<′ ℕ.<′-wellFounded
module _ {ℓ} where
open WF.All ≺-wellFounded ℓ public
renaming
( wfRecBuilder to ≺-recBuilder
; wfRec to ≺-rec
)
hiding (wfRec-builder)
{-# WARNING_ON_USAGE ≺-Rec
"Warning: ≺-Rec was deprecated in v2.0.
Please use <-Rec instead."
#-}
{-# WARNING_ON_USAGE ≺-wellFounded
"Warning: ≺-wellFounded was deprecated in v2.0.
Please use <-wellFounded instead."
#-}
{-# WARNING_ON_USAGE ≺-recBuilder
"Warning: ≺-recBuilder was deprecated in v2.0.
Please use <-recBuilder instead."
#-}
{-# WARNING_ON_USAGE ≺-rec
"Warning: ≺-rec was deprecated in v2.0.
Please use <-rec instead."
#-}