Added Irreflexivity and Asymmetry of WellFounded Relations (#2119)

Author: jmarkakis

CHANGELOG.md

@@ -3764,6 +3764,11 @@ This is a full list of proofs that have changed form to use irrelevant instance
 * Added new proof to `Induction.WellFounded`
   ```agda
   Acc-resp-flip-≈ : _<_ Respectsʳ (flip _≈_) → (Acc _<_) Respects _≈_
+
+  acc⇒asym : Acc _<_ x → x < y → ¬ (y < x)
+  wf⇒asym : WellFounded _<_ → Asymmetric _<_
+  wf⇒irrefl : _<_ Respects₂ _≈_ → Symmetric _≈_ →
+              WellFounded _<_ → Irreflexive _≈_ _<_
   ```
 
 * Added new file `Relation.Binary.Reasoning.Base.Apartness`

src/Induction/WellFounded.agda

@@ -8,15 +8,18 @@
 
 module Induction.WellFounded where
 
-open import Data.Product.Base using (Σ; _,_; proj₁)
+open import Data.Product.Base using (Σ; _,_; proj₁; proj₂)
 open import Function.Base using (_∘_; flip; _on_)
 open import Induction
 open import Level using (Level; _⊔_)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions
-  using (Symmetric; _Respectsʳ_; _Respects_)
+  using (Symmetric; Asymmetric; Irreflexive; _Respects₂_; 
+    _Respectsʳ_; _Respects_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
+open import Relation.Binary.Consequences using (asym⇒irr)
 open import Relation.Unary
+open import Relation.Nullary.Negation.Core using (¬_)
 
 private
   variable
@@ -116,6 +119,21 @@ module FixPoint
   unfold-wfRec : ∀ {x} → wfRec P f x ≡ f x λ _ → wfRec P f _
   unfold-wfRec {x} = f-ext x wfRecBuilder-wfRec
 
+------------------------------------------------------------------------
+-- Well-founded relations are asymmetric and irreflexive.
+
+module _ {_<_ : Rel A r} where
+  acc⇒asym : ∀ {x y} → Acc _<_ x → x < y → ¬ (y < x)
+  acc⇒asym {x} hx =
+    Some.wfRec (λ x → ∀ {y} → x < y → ¬ (y < x)) (λ _ hx x<y y<x → hx y<x y<x x<y) _ hx
+
+  wf⇒asym : WellFounded _<_ → Asymmetric _<_
+  wf⇒asym wf = acc⇒asym (wf _)
+
+  wf⇒irrefl : {_≈_ : Rel A ℓ} → _<_ Respects₂ _≈_ → 
+              Symmetric _≈_ → WellFounded _<_ → Irreflexive _≈_ _<_
+  wf⇒irrefl r s wf = asym⇒irr r s (wf⇒asym wf)
+
 ------------------------------------------------------------------------
 -- It might be useful to establish proofs of Acc or Well-founded using
 -- combinators such as the ones below (see, for instance,