Skip to content

Refactoring Data.Vec.Properties.lookup-inject≤-take #2090

@jamesmckinna

Description

@jamesmckinna

@JacquesCarette 's PR #2056 permits a drastic simplification in the proof of this (obscure! ... it's used nowhere in the library, for example, so example uses in the wild might be welcome) lemma

lookup-inject≤-take :  m (m≤m+n : m ≤ m + n) (i : Fin m) (xs : Vec A (m + n)) 
                      lookup xs (Fin.inject≤ i m≤m+n) ≡ lookup (take m xs) i

Towards further simplification, an easy observation to make is that the explicit argument m could be taken to be implicit here (as n already is); it's inferrable from the type/form of i...

... But in fact, there's a strong argument for deprecation of this lemma, in favour of a version not only with m implicit, but also one whose argument positions are positionally correlated with those of both lookup and inject≤, and with a more 'orthodox' naming scheme/order of equation, viz.: UPDATED see #2101

lookup-take : (xs : Vec A (m + n)) (i : Fin m) (m≤m+n : m ≤ m + n) 
              lookup (take m xs) i ≡ lookup xs (Fin.inject≤ i m≤m+n)
lookup-take (x ∷ xs) zero    _       = refl
lookup-take (x ∷ xs) (suc i) Sm≤Sm+n = lookup-take xs i (≤-pred Sm≤Sm+n)

NB some delicacy is required over this last term ≤-pred Sm≤Sm+n; various refactorings (including mine!) of Data.Fin.Base and hence of Data.Fin.Base.inject≤ mean that this can't typecheck as it stands (hence the proof actually relies on pattern matching Sm≤Sm+n@(s≤s m≤m+n)...) but I think this will be fixable by eg. work as part of #2000 (an unwieldy mess that should probably be broken up into smaller, more digestible, parts). After such (further) refactoring, the argument m≤m+n could then even be marked as irrelevant... which might actually make this lemma useful/used ;-)

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions