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})