[Agda] example with insertion to list

[Andrea Vezzosi]

Here's the issue
https://github.com/agda/agda/issues/2455

On Fri, Feb 10, 2017 at 6:37 PM, Andrea Vezzosi <sanzhiyan at gmail.com> wrote:
> 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
>>