[Agda] proof for insertion to a list

[G. Allais]

Hi Sergei,

Here's what I understand: `compare e e'` and `compare e' e`
only show up in the goal's type *after* the values of `compare e e₁`
and `compare e' e₁` have been uncovered and `add` has been able
to reduce by one step.

So here you can't simply compute all the comparisons in parallel:
you need cascading `with` blocks. The type of each one of these
block being different from the previous thanks to the computations
that happened.

I think that this is the sort of structure you're looking for:

==========================================================
add-comm (a , e) (b , e') ((c , e₁) ∷ mons)
         with compare e e₁ | compare e' e₁

... | tri> _ _ e>e₁ | tri> _ _ e'>e₁
         with compare e e' | compare e' e

... | tri> _ _ e>e' | tri< _ _ _  = {!!}

add-comm _ _  _ | _             | _           = anything
==========================================================

Now, in that new goal `compare e' e₁` shows up again. So you
probably want to use inspect [1] to remember its value.

Cheers,

[1]
http://agda.github.io/agda-stdlib/Relation.Binary.PropositionalEquality.html#5150

On 14/02/17 18:33, Sergei Meshveliani wrote:
> I am sorry for confusing files.
> Please, see now the attached  Feb14-2017.agda.
> 
> ------
> Sergei
> 
> 
> On Mon, 2017-02-13 at 20:21 +0300, Sergei Meshveliani wrote:
>> Who can tell, please: 
>>                                                                                 
>> why the following proof for  add-comm  is rejected by Agda 2.5.2 ? 
>>                                                                                 
>> (see the attached  .agda  file, it is about 30 nonempty lines).
>>                                                                                 
>> It is about certain insertion  add  of a pair to a pair list, 
>> with add-comm  meaning
>>
>>      add (a , e) ∘ add (b , e') ≗ add (b , e') ∘ add (a , e).
>>
>> And it is only for the case of  e > e' > e₁,
>>
>> with other cases postulated in the code by `anything'.
>>                                                                                 
>> I expect that for the last  PE.refl,  normalization of LHS and RHS 
>> yields the same term 
>>                      (a , e) ∷ (b , e') ∷ (c , e₁) ∷ mons.       
>>                                                                                 
>> But Agda reports  
>>
>> e != e' of type ℕ                              
>> when checking that the expression PE.refl has type  
>> add (a , e) (add (b , e') ((c , e₁) ∷ mons) | tri> .¬a₁ .¬b₁ e'>e₁)
>> ≡ add (b , e') (add (a , e) ((c , e₁) ∷ mons) | tri> .¬a .¬b e>e₁) 
>>
>>
>> Thanks,
>>
>> ------
>> Sergei
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170214/9c120437/attachment.sig>