Add begin-irrefl reasoning combinator (#1470)

Author: MatthewDaggitt

CHANGELOG.md

@@ -769,6 +769,30 @@ Non-backwards compatible changes
   IO.Instances
   ```
 
+### Changes to triple reasoning interface
+
+* The module `Relation.Binary.Reasoning.Base.Triple` now takes an extra proof that the strict
+  relation is irreflexive. 
+  
+* This allows the following new proof combinator:
+  ```agda
+  begin-contradiction : (r : x IsRelatedTo x) → {s : True (IsStrict? r)} → A
+  ```
+  that takes a proof that a value is strictly less than itself and then applies the principle of explosion.
+  
+* Specialised versions of this combinator are available in the following derived modules:
+  ```
+  Data.Nat.Properties
+  Data.Nat.Binary.Properties
+  Data.Integer.Properties
+  Data.Rational.Unnormalised.Properties
+  Data.Rational.Properties
+  Data.Vec.Relation.Binary.Lex.Strict
+  Data.Vec.Relation.Binary.Lex.NonStrict
+  Relation.Binary.Reasoning.StrictPartialOrder
+  Relation.Binary.Reasoning.PartialOrder
+  ```
+
 ### Other
 
 * In accordance with changes to the flags in Agda 2.6.3, all modules that previously used
@@ -992,6 +1016,8 @@ Major improvements
 * A new module `Algebra.Lattice.Bundles.Raw` is also introduced.
   * `RawLattice` has been moved from `Algebra.Lattice.Bundles` to this new module.
 
+* In `Relation.Binary.Reasoning.Base.Triple`, added a new parameter `<-irrefl : Irreflexive _≈_ _<_`
+
 Deprecated modules
 ------------------
 

src/Data/Integer/Properties.agda

@@ -365,6 +365,7 @@ i≮i = <-irrefl refl
 module ≤-Reasoning where
   open import Relation.Binary.Reasoning.Base.Triple
     ≤-isPreorder
+    <-irrefl
     <-trans
     (resp₂ _<_)
     <⇒≤

src/Data/List/Relation/Unary/Any/Properties.agda

@@ -254,7 +254,6 @@ Any-×⁻ pq with Prod.map₂ (Prod.map₂ find) (find pq)
 
     (p , q) ∎
 
-
   to∘from : ∀ pq → Any-×⁺ {xs = xs} (Any-×⁻ pq) ≡ pq
   to∘from pq with find pq
       | (λ (f : (proj₁ (find pq) ≡_) ⋐ _) → map∘find pq {f})

src/Data/Nat/Binary/Properties.agda

@@ -38,7 +38,6 @@ open import Relation.Binary.Consequences
 open import Relation.Binary.Morphism
 import Relation.Binary.Morphism.OrderMonomorphism as OrderMonomorphism
 open import Relation.Binary.PropositionalEquality
-import Relation.Binary.Reasoning.Base.Triple as InequalityReasoning
 open import Relation.Nullary using (¬_; yes; no)
 import Relation.Nullary.Decidable as Dec
 open import Relation.Nullary.Negation using (contradiction)
@@ -607,12 +606,18 @@ x ≤? y with <-cmp x y
 ------------------------------------------------------------------------
 -- Equational reasoning for _≤_ and _<_
 
-module ≤-Reasoning = InequalityReasoning
-  ≤-isPreorder
-  <-trans
-  (resp₂ _<_) <⇒≤
-  <-≤-trans ≤-<-trans
-  hiding (step-≈; step-≈˘)
+module ≤-Reasoning where
+
+  open import Relation.Binary.Reasoning.Base.Triple
+    ≤-isPreorder
+    <-irrefl
+    <-trans
+    (resp₂ _<_)
+    <⇒≤
+    <-≤-trans
+    ≤-<-trans
+    public
+    hiding (step-≈; step-≈˘)
 
 ------------------------------------------------------------------------
 -- Properties of _<ℕ_

src/Data/Nat/Properties.agda

@@ -495,6 +495,7 @@ m<1+n⇒m≤n (s≤s m≤n) = m≤n
 module ≤-Reasoning where
   open import Relation.Binary.Reasoning.Base.Triple
     ≤-isPreorder
+    <-irrefl
     <-trans
     (resp₂ _<_)
     <⇒≤

src/Data/Rational/Properties.agda

@@ -713,13 +713,16 @@ _>?_ = flip _<?_
 module ≤-Reasoning where
   import Relation.Binary.Reasoning.Base.Triple
     ≤-isPreorder
+    <-irrefl
     <-trans
     (resp₂ _<_)
     <⇒≤
     <-≤-trans
     ≤-<-trans
     as Triple
-  open Triple public hiding (step-≈; step-≈˘)
+
+  open Triple public
+    hiding (step-≈; step-≈˘)
 
   infixr 2 step-≃ step-≃˘
 
@@ -729,7 +732,6 @@ module ≤-Reasoning where
   syntax step-≃  x y∼z x≃y = x ≃⟨  x≃y ⟩ y∼z
   syntax step-≃˘ x y∼z y≃x = x ≃˘⟨ y≃x ⟩ y∼z
 
-
 ------------------------------------------------------------------------
 -- Properties of Positive/NonPositive/Negative/NonNegative and _≤_/_<_
 

src/Data/Rational/Unnormalised/Properties.agda

@@ -542,13 +542,16 @@ _>?_ = flip _<?_
 module ≤-Reasoning where
   import Relation.Binary.Reasoning.Base.Triple
     ≤-isPreorder
+    <-irrefl
     <-trans
     <-resp-≃
     <⇒≤
     <-≤-trans
     ≤-<-trans
     as Triple
-  open Triple public hiding (step-≈; step-≈˘)
+
+  open Triple public
+    hiding (step-≈; step-≈˘)
 
   infixr 2 step-≃ step-≃˘
 
@@ -558,7 +561,6 @@ module ≤-Reasoning where
   syntax step-≃  x y∼z x≃y = x ≃⟨  x≃y ⟩ y∼z
   syntax step-≃˘ x y∼z y≃x = x ≃˘⟨ y≃x ⟩ y∼z
 
-
 ------------------------------------------------------------------------
 -- Properties of ↥_/↧_
 

src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda

@@ -35,7 +35,6 @@ open import Relation.Binary.Construct.Add.Extrema.Strict _<_ using ([<]-injectiv
 
 import Relation.Binary.Reasoning.StrictPartialOrder as <-Reasoning
 
-
 private
   variable
     v p q : Level
@@ -278,33 +277,33 @@ module _ {V : Value v} where
                                      joinʳ⁺-right⁺ kv lk ku′ bal (Any-insertWith-just ku seg′ pr rp)
 
     -- impossible cases
-    ... | here eq  | tri< k<k′ _ _ = flip contradiction (irrefl⁺ [ k ]) $ begin-strict
+    ... | here eq  | tri< k<k′ _ _ = begin-contradiction
       [ k  ] <⟨ [ k<k′ ]ᴿ ⟩
       [ k′ ] ≈⟨ [ sym eq ]ᴱ ⟩
       [ k  ] ∎
-    ... | here eq  | tri> _ _ k>k′ = flip contradiction (irrefl⁺ [ k ]) $ begin-strict
+    ... | here eq  | tri> _ _ k>k′ = begin-contradiction
       [ k  ] ≈⟨ [ eq ]ᴱ ⟩
       [ k′ ] <⟨ [ k>k′ ]ᴿ ⟩
       [ k  ] ∎
-    ... | left lp  | tri≈ _ k≈k′ _ = flip contradiction (irrefl⁺ [ k ]) $ begin-strict
+    ... | left lp  | tri≈ _ k≈k′ _ = begin-contradiction
       let k″ = Any.lookup lp .key; k≈k″ = lookup-result lp; (_ , k″<k′) = lookup-bounded lp in
       [ k  ] ≈⟨ [ k≈k″ ]ᴱ ⟩
       [ k″ ] <⟨ k″<k′ ⟩
       [ k′ ] ≈⟨ [ sym k≈k′ ]ᴱ ⟩
       [ k  ] ∎
-    ... | left lp  | tri> _ _ k>k′ = flip contradiction (irrefl⁺ [ k ]) $ begin-strict
+    ... | left lp  | tri> _ _ k>k′ = begin-contradiction
       let k″ = Any.lookup lp .key; k≈k″ = lookup-result lp; (_ , k″<k′) = lookup-bounded lp in
       [ k  ] ≈⟨ [ k≈k″ ]ᴱ ⟩
       [ k″ ] <⟨ k″<k′ ⟩
       [ k′ ] <⟨ [ k>k′ ]ᴿ ⟩
       [ k  ] ∎
-    ... | right rp | tri< k<k′ _ _ = flip contradiction (irrefl⁺ [ k ]) $ begin-strict
+    ... | right rp | tri< k<k′ _ _ = begin-contradiction
       let k″ = Any.lookup rp .key; k≈k″ = lookup-result rp; (k′<k″ , _) = lookup-bounded rp in
       [ k  ] <⟨ [ k<k′ ]ᴿ ⟩
       [ k′ ] <⟨ k′<k″ ⟩
       [ k″ ] ≈⟨ [ sym k≈k″ ]ᴱ ⟩
       [ k  ] ∎
-    ... | right rp | tri≈ _ k≈k′ _ = flip contradiction (irrefl⁺ [ k ]) $ begin-strict
+    ... | right rp | tri≈ _ k≈k′ _ = begin-contradiction
       let k″ = Any.lookup rp .key; k≈k″ = lookup-result rp; (k′<k″ , _) = lookup-bounded rp in
       [ k  ] ≈⟨ [ k≈k′ ]ᴱ ⟩
       [ k′ ] <⟨ k′<k″ ⟩

src/Data/Vec/Relation/Binary/Lex/NonStrict.agda

@@ -261,6 +261,7 @@ module ≤-Reasoning  {_≈_ : Rel A ℓ₁} {_≼_ : Rel A ℓ₂}
 
   open import Relation.Binary.Reasoning.Base.Triple
     (≤-isPreorder ≼-po {n})
+    <-irrefl
     (<-trans ≼-po)
     (<-resp₂ isEquivalence ≤-resp-≈)
     <⇒≤

src/Data/Vec/Relation/Binary/Lex/Strict.agda

@@ -326,6 +326,7 @@ module _ {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where
 
 module ≤-Reasoning {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂}
                    (≈-isEquivalence : IsEquivalence _≈_)
+                   (≺-irrefl : Irreflexive _≈_ _≺_)
                    (≺-trans : Transitive _≺_)
                    (≺-resp-≈ : _≺_ Respects₂ _≈_)
                    (n : ℕ)
@@ -336,6 +337,7 @@ module ≤-Reasoning {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂}
 
   open import Relation.Binary.Reasoning.Base.Triple
     (≤-isPreorder ≈-isEquivalence ≺-trans ≺-resp-≈)
+    (<-irrefl ≺-irrefl)
     (<-trans ≈-isPartialEquivalence ≺-resp-≈ ≺-trans)
     (<-respects₂ ≈-isPartialEquivalence ≺-resp-≈)
     (<⇒≤ {m = n})

src/Relation/Binary/Reasoning/Base/Triple.agda

@@ -13,12 +13,13 @@
 open import Relation.Binary.Core using (Rel; _⇒_)
 open import Relation.Binary.Structures using (IsPreorder)
 open import Relation.Binary.Definitions
-  using (Transitive; _Respects₂_; Trans)
+  using (Transitive; _Respects₂_; Trans; Irreflexive)
 
 module Relation.Binary.Reasoning.Base.Triple {a ℓ₁ ℓ₂ ℓ₃} {A : Set a}
   {_≈_ : Rel A ℓ₁} {_≤_ : Rel A ℓ₂} {_<_ : Rel A ℓ₃}
   (isPreorder : IsPreorder _≈_ _≤_)
-  (<-trans : Transitive _<_) (<-resp-≈ : _<_ Respects₂ _≈_) (<⇒≤ : _<_ ⇒ _≤_)
+  (<-irrefl : Irreflexive _≈_ _<_) (<-trans : Transitive _<_) (<-resp-≈ : _<_ Respects₂ _≈_)
+  (<⇒≤ : _<_ ⇒ _≤_)
   (<-≤-trans : Trans _<_ _≤_ _<_) (≤-<-trans : Trans _≤_ _<_ _<_)
   where
 
@@ -27,6 +28,8 @@ open import Function.Base using (case_of_; id)
 open import Level using (Level; _⊔_; Lift; lift)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; refl; sym)
+open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Nullary.Decidable.Core
   using (Dec; yes; no; True; toWitness)
 
@@ -79,7 +82,7 @@ extractEquality (isEquality x≈y) = x≈y
 -- See `Relation.Binary.Reasoning.Base.Partial` for the design decisions
 -- behind these combinators.
 
-infix  1 begin_ begin-strict_ begin-equality_
+infix  1 begin_ begin-strict_ begin-equality_ begin-contradiction_
 infixr 2 step-< step-≤ step-≈ step-≈˘ step-≡ step-≡˘ _≡⟨⟩_
 infix  3 _∎
 
@@ -96,6 +99,13 @@ begin-strict_ r {s} = extractStrict (toWitness s)
 begin-equality_ : ∀ {x y} (r : x IsRelatedTo y) → {s : True (IsEquality? r)} → x ≈ y
 begin-equality_ r {s} = extractEquality (toWitness s)
 
+begin-contradiction_ : ∀ {x} (r : x IsRelatedTo x) {s : True (IsStrict? r)} →
+                      ∀ {a} {A : Set a} → A
+begin-contradiction_ {x} r {s} = contradiction x<x (<-irrefl Eq.refl)
+  where
+  x<x : x < x
+  x<x = extractStrict (toWitness s)
+
 -- Step with the strict relation
 
 step-< : ∀ (x : A) {y z} → y IsRelatedTo z → x < y → x IsRelatedTo z

src/Relation/Binary/Reasoning/PartialOrder.agda

@@ -45,13 +45,16 @@ module Relation.Binary.Reasoning.PartialOrder
   {p₁ p₂ p₃} (P : Poset p₁ p₂ p₃) where
 
 open Poset P
-import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as Strict
+open import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_
+  as Strict
+  using (_<_)
 
 ------------------------------------------------------------------------
 -- Re-export contents of base module
 
 open import Relation.Binary.Reasoning.Base.Triple
   isPreorder
+  Strict.<-irrefl
   (Strict.<-trans isPartialOrder)
   (Strict.<-resp-≈ isEquivalence ≤-resp-≈)
   Strict.<⇒≤

src/Relation/Binary/Reasoning/StrictPartialOrder.agda

@@ -53,9 +53,11 @@ import Relation.Binary.Construct.StrictToNonStrict _≈_ _<_ as NonStrict
 
 open import Relation.Binary.Reasoning.Base.Triple
   (NonStrict.isPreorder₂ isStrictPartialOrder)
+  irrefl
   trans
   <-resp-≈
   NonStrict.<⇒≤
   (NonStrict.<-≤-trans trans <-respʳ-≈)
   (NonStrict.≤-<-trans Eq.sym trans <-respˡ-≈)
   public
+