<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>
</head>
<body dir="ltr">
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
Hi Jacques,</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
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 `<span style="font-family: "Courier New", monospace;">left-inv (n , xs)</span>` directly is the
direction of the equality. If the function is `<span style="font-family: "Courier New", monospace">x ≡ blah</span>` then the inductive hypothesis seems directly applicable.<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
<span style="font-family: "Courier New", monospace;"> left-inv : (x : Σ ℕ (Vec A)) → (length (toList (proj₂ x)) , fromList (toList (proj₂ x))) ≡ x</span><span><br>
</span>
<div><span style="font-family: "Courier New", monospace;"> left-inv (0 , []) = refl</span><br>
</div>
<div><span style="font-family: "Courier New", monospace;"> left-inv (suc n , x ∷ xs)</span><br>
</div>
<div><span style="font-family: "Courier New", monospace;"> with length (toList xs) | fromList (toList xs) | left-inv (n , xs)</span><br>
</div>
<div><span style="font-family: "Courier New", monospace;"> ... | _ | _ | refl = refl</span><br>
</div>
<span></span><br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div id="Signature">
<div></div>
<div id="divtagdefaultwrapper" dir="ltr" style="font-size: 12pt; color: rgb(0, 0, 0); font-family: Calibri, Arial, Helvetica, sans-serif;">
<font size="3"><b>Thanks,</b></font></div>
<div dir="ltr" style="font-size: 12pt; color: rgb(0, 0, 0); font-family: Calibri, Arial, Helvetica, sans-serif;">
<font size="3"><b>Jason Hu</b></font></div>
<div dir="ltr" style="font-size: 12pt; color: rgb(0, 0, 0); font-family: Calibri, Arial, Helvetica, sans-serif;">
<font size="3"><b><a href="https://hustmphrrr.github.io/" style="">https://hustmphrrr.github.io/</a></b></font><br>
<font size="3"><b></b></font><font style="font-size:12pt" size="3"><span style="color: rgb(69, 129, 142);"><span style="font-family:trebuchet ms,sans-serif"><b><a target="_blank" style=""></a></b></span></span></font></div>
</div>
<div id="appendonsend"></div>
<hr style="display:inline-block;width:98%" tabindex="-1">
<div id="divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" style="font-size:11pt" color="#000000"><b>From:</b> Agda <agda-bounces@lists.chalmers.se> on behalf of Jacques Carette <carette@mcmaster.ca><br>
<b>Sent:</b> December 17, 2019 11:02 PM<br>
<b>To:</b> agda <agda@lists.chalmers.se><br>
<b>Subject:</b> [Agda] Need a hand with a proof</font>
<div> </div>
</div>
<div class="BodyFragment"><font size="2"><span style="font-size:11pt;">
<div class="PlainText">Self-contained code with one hole. The main theorem 'List A ↔ Σ ℕ (Vec
<br>
A)' ought to be obvious. Certainly the two functions that witness it <br>
are; the problem is to prove left-inverse. The right-inverse is already <br>
in Data.Vec.Properties. I've tried many ideas, to no avail.<br>
<br>
Jacques<br>
<br>
module help where<br>
<br>
open import Data.List using (List; _∷_; []; length)<br>
open import Data.Vec using (Vec; _∷_; []; fromList; toList)<br>
open import Data.Vec.Properties using (toList∘fromList; ∷-injective)<br>
open import Data.Product using (Σ; _,_; proj₁; proj₂)<br>
<br>
open import Function using (_∘_; _↔_; _$_)<br>
<br>
open import Relation.Binary.PropositionalEquality<br>
using (_≡_; refl; subst; cong; sym; trans)<br>
<br>
private<br>
variable<br>
a : Level<br>
A : Set a<br>
<br>
forgetting-length : {a : Level} {A : Set a} → List A ↔ Σ ℕ (Vec A)<br>
forgetting-length = record<br>
{ f = λ xs → length xs , fromList xs<br>
; f⁻¹ = toList ∘ proj₂<br>
; cong₁ = λ { refl → refl }<br>
; cong₂ = λ { refl → refl }<br>
; inverse = left-inv , toList∘fromList<br>
}<br>
where<br>
length-stable : (x : Σ ℕ (Vec A)) → length (toList (proj₂ x)) ≡ proj₁ x<br>
length-stable (0 , []) = refl<br>
length-stable (suc i , x ∷ xs) = cong suc (length-stable (i , xs))<br>
<br>
left-inv : (x : Σ ℕ (Vec A)) → (length (toList (proj₂ x)) , <br>
fromList (toList (proj₂ x))) ≡ x<br>
left-inv (0 , []) = refl<br>
left-inv (suc n , x ∷ xs) = {!!}<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
Agda@lists.chalmers.se<br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div>
</span></font></div>
</body>
</html>