[Agda] a version for Fin

[Sergei Meshveliani]

People,

This is about Fin and `lookup' of Standard library.

I am trying to prove the following simple lemma:

 ... (i : Fin (length xs)) → lookup xs i ≡ lookup (xs ++ [ y ]) i

Only the last occurrence of  i  needs to be replaced with
i' = (inject≤ i length-xs-≤-length-xs++y).

This proof occurs difficult for me.

Then I replace  Fin  with

  Fin' : ℕ → Set
  Fin' n =  Σ ℕ (_< n)

And succeed with a proof for the corresponding lookup' and lemma'.

Is  Fin'  better?
Can people, please, provide a reasonably looking proof for `lemma' with
Fin ?

I attach a small source containing first the version (II) with Fin',
and then the formulation for version (I).

Thanks,

------
Sergei

-------------- next part --------------
{-
This is about Fin and `lookup' of Standard library.

Prove the following simple lemma:
  
  ... (i : Fin (length xs)) → 
                       lookup xs i ≡ lookup (xs ++ [ y ]) i

Only the last occurrence of  i  needs to be replaced with
i' = (inject≤ i length-xs-≤-length-xs++y).

This proof occurs difficult for me.

Then I replace  Fin  with

  Fin' : ℕ → Set
  Fin' n =  Σ ℕ (_< n)
  
And succeed with a proof for the corresponding lookup' and lemma'.

Is  Fin'  better?
Can people provide a resonably looking proof for `lemma' with Fin ? 
-}


module FinVersion where

open import Relation.Nullary using (¬_) 
open import Relation.Nullary.Negation using (contradiction) 
open import Relation.Binary.PropositionalEquality as PE using 
                                    (_≡_; refl; sym; trans; subst)
open PE.≡-Reasoning
open import Data.Product using (_,_; Σ)
open import Data.List using (List; []; _∷_; length; _++_; 
                                             [_]; lookup)
open import Data.List.Properties using (length-++)
open import Data.Nat using (ℕ; suc; _+_; _≤_; _<_; s≤s)
open import Data.Nat.Properties using 
            (≤-trans; ≤-refl; <-trans; m≤m+n; n≤1+n; ≤-reflexive;
             pred-mono; +-comm; module ≤-Reasoning)
open ≤-Reasoning using () 
                 renaming (begin_ to ≤begin_; _∎ to _≤end;
                           _≡⟨_⟩_ to _≡≤[_]_; _≤⟨_⟩_ to _≤[_]_)
open import Data.Fin using (Fin; inject≤)



------------------------ a common Prelude -------------
≮0 : {n : ℕ} → ¬ n < 0  
≮0 ()

length-xs≤length-xs++ys :                     
          ∀ {α} {A : Set α} (xs : List A) {ys : List A} → 
                            length xs ≤ length (xs ++ ys)

length-xs≤length-xs++ys {_} {_} xs {ys} = 
       ≤begin 
         length xs               ≤[ m≤m+n (length xs) (length ys) ] 
         length xs + length ys  ≡≤[ sym (length-++ xs) ] 
         length (xs ++ ys)
       ≤end 
--------------------------------------------------------



--- Two usage versions for  Fin and `lookup' ---------------------------


-- Version II.
-- Use another definitions for Fin
-- and the corresponding version of `lookup':

Fin' : ℕ → Set
Fin' n =
       Σ ℕ (_< n)

inject'≤ :  {m n : ℕ} → Fin' m → m ≤ n → Fin' n
inject'≤ (i , i<m) m≤n =
                       (i , ≤-trans i<m m≤n)


lookup' :  ∀ {α} {A : Set α} (xs : List A) → Fin' (length xs) → A
lookup' []       ()
lookup' (x ∷ _)  (0 , _)              =  x
lookup' (x ∷ xs) (suc n , 1+n<1+|xs|) =  
                          lookup' xs (n , pred-mono 1+n<1+|xs|)


lookup'-irrel :  ∀ {α} {A : Set α} (xs : List A) (k : ℕ)  
                       (lt lt' : k < length xs) → 
                       lookup' xs (k , lt) ≡ lookup' xs (k , lt')

lookup'-irrel []       _       () 
lookup'-irrel (_ ∷ _)  0       _       _        =  refl
lookup'-irrel (x ∷ xs) (suc k) 1+k<1+l 1+k<'1+l =  
                               lookup'-irrel xs k k<l k<'l
                               where
                               k<l  = pred-mono 1+k<1+l
                               k<'l = pred-mono 1+k<'1+l

-----------------------------------------------------------
-- Prove the `lemma' version:

lemma' : 
  (y : ℕ) (xs : List ℕ) 
  (let ys = xs ++ [ y ];  l = length xs;  l' = length ys) →            
  0 < l → (i : Fin' l) → 
  (let 
     l≤l' = length-xs≤length-xs++ys xs
     i'   = inject'≤ i l≤l'
  ) → 
  lookup' xs i ≡ lookup' (xs ++ [ y ]) i'


lemma' _ (_ ∷ _)  _ (0 ,     _    ) =  refl
lemma' _ (_ ∷ []) _ (suc k , 1+k<1) =  
                                 contradiction (pred-mono 1+k<1) ≮0

lemma' y (x ∷ x' ∷ xs) _ i@(suc k , 1+k<|xx'xs|) = 
  begin
    lookup' (x ∷ x'xs) (suc k , 1+k<|xx'xs|)  ≡⟨ refl ⟩
    lookup' (x' ∷ xs) (k , k<|x'xs|)         
                    ≡⟨ lemma' y (x' ∷ xs) 0<|x'xs| (k , k<|x'xs|)  
                     ⟩
    lookup' (x'xs ++ [ y ]) (k , k<|x'xs:y|)      
                     ≡⟨ lookup'-irrel x'xs:y k k<|x'xs:y| 
                                             (pred-mono 1+k<|ys|) 
                      ⟩
    lookup' x'xs:y (k , pred-mono 1+k<|ys|)      ≡⟨ refl ⟩
    lookup' ((x ∷ x'xs) ++ [ y ]) i'
  ∎
  where
  x'xs     = x' ∷ xs
  xx'xs    = x ∷ x'xs
  ys       = xx'xs ++ [ y ]
  |x'xs|   = length x'xs
  |xx'xs|  = length xx'xs 
  |ys|     = length ys
  x'xs:y   = x'xs ++ [ y ]
  |x'xs|≤|x'xs:y| =  length-xs≤length-xs++ys x'xs
  |xx'xs|≤|ys|    =  length-xs≤length-xs++ys xx'xs

  i'         =  inject'≤ i |xx'xs|≤|ys|
  k<|x'xs|   =  pred-mono 1+k<|xx'xs|
  0<|x'xs|   =  m≤m+n 1 (length xs)
  1+k<|ys|   =  ≤-trans 1+k<|xx'xs| |xx'xs|≤|ys|  
  k<|x'xs:y| =  ≤-trans k<|x'xs| |x'xs|≤|x'xs:y| 




--==================================================================
-- Version I.

lemma : (y : ℕ) (xs : List ℕ) 
        (let ys = xs ++ [ y ];  l = length xs;  l' = length ys) →            
        0 < l → (i : Fin l) → 
        (let 
           l≤l' = length-xs≤length-xs++ys xs
           i'   = inject≤ i l≤l'
        ) → 
        lookup xs i ≡ lookup (xs ++ [ y ]) i'


lemma y (x ∷ _) _ Fin.zero =  refl   -- ??

... ?