[Agda] example with insertion to list

[Andrea Vezzosi]

You can get the version with the inequality proof to accept the
PE.refl proof by not using "se" in the type of aux.

There's an analysis that tries to figure out whether aux depends on
the extra arguments it gets by being defined inside extMon+, and the
use of "se" is fooling the analysis here.

This should be reported as a bug, but I will try to shrink the test case first.

Best,
Andrea

On Wed, Feb 8, 2017 at 10:12 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:
> On Wed, 2017-02-08 at 14:56 +0100, G. Allais wrote:
>> You're right! If we hoist the definition of `aux` out of the where
>> clause then the PE.refl proof without pattern-matching goes through.
>> It's very strange.
>> [..]
>
>
> Please, see a simplified version  Debug-feb8-2017.agda  attached.
> It avoids adding the inequality proof.
> And there Agda type-checks the proof for lemma2 that does not match
> against the list:
>
> --------------------------------------------------------------------
> lemma2 : ∀ e e' es → (ord-e'es : DecrOrdered (e' ∷ es)) → e < e' →
>                 let
>                   f = pol′ (e' ∷ es) ord-e'es
>
>                   ord-es : DecrOrdered es
>                   ord-es = tailOrdered ord-e'es
>
>                   f' = pol′ es ord-es
>                 in
>                 Pol.exps (mon+ e f) ≡ e' ∷ (Pol.exps (mon+ e f'))
>
> lemma2 e e' es ord-e'es e<e'  with compare e e'
> ...
>     | tri< _    _ _ = PE.refl
> ... | tri≈ e≮e' _ _ = ⊥-elim (e≮e' e<e')
> ... | tri> e≮e' _ _ = ⊥-elim (e≮e' e<e')
> --------------------------------------------------------------------
>
> I do not understand why does not it type-check
> Debug-feb4-2017.agda  similarly.
>
>
>
>> > 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
>> >
>> >
>>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>