×-wellFounded' without symmetry of _≈₁_

[jwaldmann]

Hi.

I needed a version of ×-wellFounded' from https://agda.github.io/agda-stdlib/Data.Product.Relation.Binary.Lex.Strict.html#6946 that does not have the symmetry requirement on ≈₁ . Transitivity is enough to get the theorem, and I don't have symmetry in my application (relative termination).

So I cobbled together this version of the code: https://gitlab.imn.htwk-leipzig.de/waldmann/pure-matchbox/-/blob/d75cbfd1bb364a2e2b48ff7af2ba75be35e0b1b4/cert/R.agda#L208 (application: see end of that file).

I'm sure my code looks terrible (as I am learning the language as I go along) but perhaps you can use it somehow (or tell me how to rewrite it so that you can use it).

[jamesmckinna]

Johannes, Thanks for drawing attention to this!

It seems like a clear win, to be able to simplify a theorem/proof in the library.

It would be great if you were to submit it as a PR (see HACKING.md), but if you're learning Agda as you go, that might be too much to ask for.

If you're not confident about doing so, though, then I'll see what I can do. UPDATED: I did it anyway;-)

[jamesmckinna]

And: your code doesn't look "terrible"!
UPDATED: See below for a tidied up list of possible library imports. Other suggestions available on request ;-)

[jamesmckinna]

@jwaldmann Suggest that you look at the PR #2077 I just opened,and see if it does what you want (it's the bare bones for the time being). Other improvements might be possible, but let's start with this?
As you will see,I took the liberty of renaming your weak lemma on Accessibility in Induction.WellFounded, but otherwise, it's your code (and its various consequences, for eg Data.Vec.Relation.Binary.Lex.Strict)...

[Seiryn21]

Aahh, Acc-resp-weak-≈ is nice, sorry i didn't thought about it when writing this proof.

[jamesmckinna]

No problem! We advance slowly, and can only see further by standing on one another's shoulders... giants or not!

[jamesmckinna]

For the rest of your associated development, @jwaldmann you may wish to also see Relation.Binary.Rewriting in the library since commit e86b564 (2019-04-29).

Elsewhere, I've looked at the imports in your development R.agda, and as far as I can tell, the following should suffice:

-- for initial imports, sufficient to use agda-stdlib-v.1.7.2

open import Data.List renaming ( _∷_  to  _::_ )
open import Data.Bool using (Bool; false; true) 
open import Data.Nat renaming  ( ℕ to Nat ; _≥_ to _>=_)
  -- hiding ( _/_ ) -- now exported by Data.Nat.DivMod
open import Data.Nat.Properties

open import Data.Nat.Solver using (module +-*-Solver)
open +-*-Solver using (solve; _:*_; _:+_; con; _:=_)

open import Data.Product renaming ( _×_ to _X_ )
open import Data.Product.Relation.Binary.Lex.Strict as Strict using (×-Lex)
open import Data.Product.Relation.Binary.Pointwise.NonDependent as Pointwise
  using (Pointwise)

open import Data.Sum.Base using (inj₁; inj₂) renaming (_-⊎-_  to union)

open import Function.Base using ( _on_ ; flip )

open import Induction.WellFounded
  using (Acc; acc; WellFounded; WfRec; module Subrelation)

open import Level using (Level)

open import Relation.Binary.Construct.Closure.ReflexiveTransitive
  renaming ( ε to start ;   _◅_ to step ; _◅◅_ to append )
open import Relation.Binary.Construct.On as On
open import Relation.Binary.Core
open import Relation.Binary.Definitions
open import Relation.Binary.PropositionalEquality.Core as ≡ renaming ( _≡_ to _==_ )
open import Relation.Binary.Rewriting renaming (StronglyNormalizing to SN)

-- well-foundedness of > on Nat

open import Data.Nat.Induction using (<-wellFounded)

_<N_ : Nat -> Nat -> Set
x <N y = x < y

wf<N : WellFounded _<N_
wf<N = <-wellFounded

and that the sharper lemma you proved, and which is now in #2077 can in fact be inlined (but that's fiddly to do, and the sharpening should be in stdlib)...

[MatthewDaggitt]

Fixed by #2077