[Agda] example with insertion to list

[Sergei Meshveliani]

On Tue, 2017-02-07 at 14:35 +0100, G. Allais wrote:
> 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
> ========================================


Guillaume, thank you very much for the fix.

Indeed,  aux  has [] among its patterns.
Further, the goal of  lemma2  is about  (mon+ e f),  which calls for 
(aux (e' ∷ es) ...),
so that the argument for  aux  is given as non-empty.
And I have an impression that the goal lhs 

  Pol.exps (mon+ e f)  

is converted by normalization to

  Pol.exps (mon+ e (pol′ (e' ∷ es) ord-e'es)),

I thought that, hence, the pattern of [] is not needed in  lemma2.
And further normalization must give the goal rhs

  e' ∷ (Pol.exps (mon+ e f')).

Your program is type-checked.
And I do not understand, so far, why the initial program is not
type-checked.
With such intuition, I shall probably have further difficulties in
composing proofs.
Either I need to fix intuition, or Agda needs to fix normalization.

Regards,

------
Sergei

> 
> 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
> > 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda