[Agda] Need a hand with a proof

[Jason -Zhong Sheng- Hu]

Hi Jacques,

you just need to generalize over the two fields of the tuple, and then the inductive hypothesis will just work. I think  the reason why it fails by matching on `left-inv (n , xs)`  directly is the direction of the equality. If the function is `x ≡ blah` then the inductive hypothesis seems directly applicable.

     left-inv : (x : Σ ℕ (Vec A)) → (length (toList (proj₂ x)) , fromList (toList (proj₂ x))) ≡ x
     left-inv (0 , [])         = refl
     left-inv (suc n , x ∷ xs)
       with length (toList xs) | fromList (toList xs) | left-inv (n , xs)
     ... | _ | _ | refl = refl


Thanks,
Jason Hu
https://hustmphrrr.github.io/
________________________________
From: Agda <agda-bounces at lists.chalmers.se> on behalf of Jacques Carette <carette at mcmaster.ca>
Sent: December 17, 2019 11:02 PM
To: agda <agda at lists.chalmers.se>
Subject: [Agda] Need a hand with a proof

Self-contained code with one hole.  The main theorem 'List A ↔ Σ ℕ (Vec
A)' ought to be obvious. Certainly the two functions that witness it
are; the problem is to prove left-inverse. The right-inverse is already
in Data.Vec.Properties. I've tried many ideas, to no avail.

Jacques

module help where

open import Data.List using (List; _∷_; []; length)
open import Data.Vec using (Vec; _∷_; []; fromList; toList)
open import Data.Vec.Properties using (toList∘fromList; ∷-injective)
open import Data.Product using (Σ; _,_; proj₁; proj₂)

open import Function using (_∘_; _↔_; _$_)

open import Relation.Binary.PropositionalEquality
   using (_≡_; refl; subst; cong; sym; trans)

private
   variable
     a : Level
     A : Set a

forgetting-length : {a : Level} {A : Set a} → List A ↔ Σ ℕ (Vec A)
forgetting-length = record
   { f = λ xs → length xs , fromList xs
   ; f⁻¹ = toList ∘ proj₂
   ; cong₁ = λ { refl → refl }
   ; cong₂ = λ { refl → refl }
   ; inverse = left-inv , toList∘fromList
   }
   where
     length-stable : (x : Σ ℕ (Vec A)) → length (toList (proj₂ x)) ≡ proj₁ x
     length-stable (0 , []) = refl
     length-stable (suc i , x ∷ xs) = cong suc (length-stable (i , xs))

     left-inv : (x : Σ ℕ (Vec A)) → (length (toList (proj₂ x)) ,
fromList (toList (proj₂ x))) ≡ x
     left-inv (0 , []) = refl
     left-inv (suc n , x ∷ xs) = {!!}

_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20191218/a889858f/attachment.html>