Wellfounded proof for sum relations (#1920)

Author: Seiryn21

CHANGELOG.md

@@ -2254,6 +2254,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`:

src/Data/Sum/Relation/Binary/LeftOrder.agda

@@ -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
@@ -78,6 +79,20 @@ 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₂ ℓ₄}

src/Data/Sum/Relation/Binary/Pointwise.agda

@@ -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)
@@ -74,6 +75,19 @@ 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