[Agda] example with insertion to list

[G. Allais]

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.

================================================================
aux : (e : E) (es0 : List E) → DecrOrdered es0 → (∃ \h → deg' h ≤ suc e
⊔ (hdExp' es0))

aux e []        _        = (monPol e , leq)  where
                                           leq : suc e ≤ suc e ⊔ 0
                                           leq = proj₁ (both≤⊔ (suc e) 0)
aux e  (e' ∷ es) ord-e'es  with compare e e'
...  | tri> _ _ e>e' =  (pol′ (e ∷ e' ∷ es) ord-ee'se , leq)
                       where
                       leq : suc e ≤ suc e ⊔ (suc e')
                       leq = proj₁ (both≤⊔ (suc e) (suc e'))

                       postulate  ord-ee'se : DecrOrdered (e ∷ e' ∷ es)

... | tri< e<e' _ _ =  (pol′ (e' ∷ esG) ord-e'esG , leq)
                       where
                       ord-es : DecrOrdered es
                       ord-es = tailDecrOrdered ord-e'es

                       esG = Pol.exps (proj₁ (aux e es ord-es))

                       leq :  (suc e') ≤ suc e ⊔ (suc e')
                       leq =  proj₂ (both≤⊔ (suc e) (suc e'))

                       postulate  ord-e'esG : DecrOrdered (e' ∷ esG)

... | tri≈ _ e≡e' _ =  (pol′ (e ∷ es) ord-ees , leq)
                       -- here  e  is contrived
                       where
                       e'es≡ees : e' ∷ es ≡ e ∷ es
                       e'es≡ees = PE.cong (_∷ es) (PE.sym e≡e')

                       ord-ees : DecrOrdered (e ∷ es)
                       ord-ees = PE.subst DecrOrdered e'es≡ees ord-e'es

                       leq : suc e ≤ suc e ⊔ (suc e')
                       leq = proj₁ (both≤⊔ (suc e) (suc e'))



extMon+ : (e : E) → (f : Pol) → (∃ \h → deg' h ≤ (suc e) ⊔ (deg' f))

extMon+ e (pol′ es ord) =  aux e es ord
================================================================

On 07/02/17 20:12, Sergei Meshveliani wrote:
> 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
> 
> 

-------------- 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/20170208/227599d0/attachment.sig>