Skip to content

Wellfounded proof for sum relations #1920

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Feb 20, 2023
Merged

Wellfounded proof for sum relations #1920

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
34cdc89
Wellfounded proof for sum relations
Seiryn21 Feb 3, 2023
815d5fe
Formatting correction
Seiryn21 Feb 3, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2198,6 +2198,15 @@ Other minor changes
map f (map g h) ∘ assocʳ ≗ assocʳ ∘ map (map f g) h
```

* Adden new proof in `Data.Sum.Relation.Binary.LeftOrder` :
```
⊎-<-WellFounded : WellFounded ∼₁ → WellFounded ∼₂ → WellFounded (∼₁ ⊎-< ∼₂)
```
* Adden new proof in `Data.Sum.Relation.Binary.Pointwise` :
```
⊎-WellFounded : WellFounded ∼₁ → WellFounded ∼₂ → WellFounded (Pointwise ∼₁ ∼₂)
```

* Made `Map` public in `Data.Tree.AVL.IndexedMap`

* Added new definitions in `Data.Vec.Base`:
Expand Down
12 changes: 12 additions & 0 deletions src/Data/Sum/Relation/Binary/LeftOrder.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ open import Data.Sum.Relation.Binary.Pointwise as PW
open import Data.Product
open import Data.Empty
open import Function
open import Induction.WellFounded
open import Level
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
Expand Down Expand Up @@ -78,6 +79,17 @@ module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂}
⊎-<-decidable dec₁ dec₂ (inj₂ x) (inj₁ y) = no λ()
⊎-<-decidable dec₁ dec₂ (inj₂ x) (inj₂ y) = Dec.map′ ₂∼₂ drop-inj₂ (dec₂ x y)

⊎-<-WellFounded : WellFounded ∼₁ → WellFounded ∼₂ → WellFounded (∼₁ ⊎-< ∼₂)
⊎-<-WellFounded wf₁ wf₂ x = acc (⊎-<-acc x)
where ⊎-<-acc₁ : ∀ {x} → Acc ∼₁ x → WfRec (∼₁ ⊎-< ∼₂) (Acc (∼₁ ⊎-< ∼₂)) (inj₁ x)
⊎-<-acc₁ (acc rec) (inj₁ y) (₁∼₁ x∼₁y) = acc (⊎-<-acc₁ (rec y x∼₁y))
⊎-<-acc₂ : ∀ {x} → Acc ∼₂ x → WfRec (∼₁ ⊎-< ∼₂) (Acc (∼₁ ⊎-< ∼₂)) (inj₂ x)
⊎-<-acc₂ (acc rec) (inj₁ y) ₁∼₂ = acc (⊎-<-acc₁ (wf₁ y))
⊎-<-acc₂ (acc rec) (inj₂ y) (₂∼₂ x∼₂y) = acc (⊎-<-acc₂ (rec y x∼₂y))
⊎-<-acc : ∀ x → WfRec (∼₁ ⊎-< ∼₂) (Acc (∼₁ ⊎-< ∼₂)) x
⊎-<-acc (inj₁ x) = ⊎-<-acc₁ (wf₁ x)
⊎-<-acc (inj₂ x) = ⊎-<-acc₂ (wf₂ x)

module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂}
{ℓ₁ ℓ₂} {∼₁ : Rel A₁ ℓ₁} {≈₁ : Rel A₁ ℓ₂}
{ℓ₃ ℓ₄} {∼₂ : Rel A₂ ℓ₃} {≈₂ : Rel A₂ ℓ₄}
Expand Down
11 changes: 11 additions & 0 deletions src/Data/Sum/Relation/Binary/Pointwise.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ module Data.Sum.Relation.Binary.Pointwise where
open import Data.Product using (_,_)
open import Data.Sum.Base as Sum
open import Data.Sum.Properties
open import Induction.WellFounded
open import Level using (_⊔_)
open import Function.Base using (_∘_; id)
open import Function.Inverse using (Inverse)
Expand Down Expand Up @@ -74,6 +75,16 @@ module _ {a₁ a₂ ℓ₁ ℓ₂} {A₁ : Set a₁} {A₂ : Set a₂}
⊎-decidable _≟₁_ _≟₂_ (inj₂ x) (inj₁ y) = no λ()
⊎-decidable _≟₁_ _≟₂_ (inj₂ x) (inj₂ y) = Dec.map′ inj₂ drop-inj₂ (x ≟₂ y)

⊎-WellFounded : WellFounded ∼₁ → WellFounded ∼₂ → WellFounded (Pointwise ∼₁ ∼₂)
⊎-WellFounded wf₁ wf₂ x = acc (⊎-acc x)
where ⊎-acc₁ : ∀ {x} → Acc ∼₁ x → WfRec (Pointwise ∼₁ ∼₂) (Acc (Pointwise ∼₁ ∼₂)) (inj₁ x)
⊎-acc₁ (acc rec) (inj₁ y) (inj₁ x∼₁y) = acc (⊎-acc₁ (rec y x∼₁y))
⊎-acc₂ : ∀ {x} → Acc ∼₂ x → WfRec (Pointwise ∼₁ ∼₂) (Acc (Pointwise ∼₁ ∼₂)) (inj₂ x)
⊎-acc₂ (acc rec) (inj₂ y) (inj₂ x∼₂y) = acc (⊎-acc₂ (rec y x∼₂y))
⊎-acc : ∀ x → WfRec (Pointwise ∼₁ ∼₂) (Acc (Pointwise ∼₁ ∼₂)) x
⊎-acc (inj₁ x) = ⊎-acc₁ (wf₁ x)
⊎-acc (inj₂ x) = ⊎-acc₂ (wf₂ x)

module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂}
{ℓ₁ ℓ₂} {∼₁ : Rel A₁ ℓ₁} {≈₁ : Rel A₁ ℓ₂}
{ℓ₃ ℓ₄} {∼₂ : Rel A₂ ℓ₃} {≈₂ : Rel A₂ ℓ₄} where
Expand Down