[Agda] example with insertion to list

[G. Allais]

Hi Sergei,

For your proof to be accepted you need `aux` to reduce. You can
achieve that by pattern-matching on `es` like so:

========================================
lemma2 e e' es ord-e'es e<e' with compare e e'
lemma2 e e' []         ord-e'es e<e' | tri< _ _ _ = PE.refl
lemma2 e e' (e'' ∷ es) ord-e'es e<e' | tri< _ _ _ = PE.refl
... | _ = anything
========================================

Cheers,

--
gallais

On 07/02/17 14:21, Sergei Meshveliani wrote:
> On Tue, 2017-02-07 at 15:20 +0300, Sergei Meshveliani wrote:
>> Please,
>>
>> can anybody fix the proof for  lemma2  in the attached code 
>> (about 140 lines) ?
>>
>> It is about a certain insertion of a natural into a decreasingly ordered
>> list of naturals. Such a list is called  Pol.
>> Insertion of  e  into  es  is according to _>_, and it is without
>> copying, that is when  es  contains any  e' ≡ e,  the result is  es.
>>
>> Insertion is called  mon+. 
>> lemma1 and lemma2  are certain two very simple statements about
>> insertion of  e  into  (e' ∷ es)  for  e < e'.
>>
>> lemma1  is for the case of  es = [].  And it is proved trivially.
>>
>> And a similar proof for  lemma2  is not type-checked (in Agda 2.5.2).
>> Moreover, I do not find any proof to satisfy Agda.
>>
>> Maybe, this is a bug in Agda?
> 
> 
> In this code, the  Max  structure and inequality are brought there to
> mon+ and extMon+  in order to prove termination. 
> This complicates  mon+,  and proof search for its properties.
>   
> mon+  can be greatly simplified by introducing `insert' for insertion of
> e  into  es  without providing a proof in recursion,
> and then, by adding a proof for 
>                       DecrOrdered es -> DecrOrdered (insert e es).
> 
> I hope, there  lemma2  will be easier to prove. 
> 
> Still:  what can be a proof for Agda for the original implementation of
> mon+ ?
> 
> Regards,
> 
> ------
> Sergei
> 
> _______________________________________________
> 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/20170207/16bd79ca/attachment.sig>