[Agda] example with insertion to list

[Sergei Meshveliani]

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
> > 
> > 
> 

-------------- next part --------------
open import Function using (_∘_; case_of_)
open import Algebra.FunctionProperties using (Op₂)
open import Relation.Binary using (Rel; Tri; DecTotalOrder; StrictTotalOrder)
open import Relation.Binary.PropositionalEquality as PE using (_≡_)
open import Data.Empty      using (⊥-elim) 
open import Data.Sum        using (_⊎_)
open import Data.Product    using (_×_; _,_; proj₁; proj₂; ∃)
open import Data.List       using (List; []; _∷_; map) 
open import Data.List.All   using (All) renaming ([] to []a; _∷_ to _∷a_)
open import Data.Nat as Nat using (ℕ; suc; _≤_; _<_; _>_) 
open import Data.Nat.Properties as NatProp using ()


--****************************************************************************
natSTO = NatProp.strictTotalOrder 
open StrictTotalOrder natSTO using (compare) 

data DecrOrdered :  List ℕ → Set 
     where
     nil    : DecrOrdered []
     single : (x : ℕ) → DecrOrdered (x ∷ [])
     prep2  : (x y : ℕ) → (xs : List ℕ) → x > y → DecrOrdered (y ∷ xs) →
                                                  DecrOrdered (x ∷ y ∷ xs)

tailOrdered :  ∀ {x xs} → DecrOrdered (x ∷ xs) → DecrOrdered xs
tailOrdered (single _)                = nil
tailOrdered (prep2 x y xs _ ord-y:xs) = ord-y:xs

consOrdered :  ∀ {x xs} → DecrOrdered xs → All (x >_) xs →
                                                         DecrOrdered (x ∷ xs)
consOrdered {x} {[]}     _       _             = single x
consOrdered {x} {y ∷ xs} ord-yxs (x>y ∷a x>xs) = prep2 x y xs x>y ord-yxs


------------------------------------------------------------------------------
record Pol :  Set where constructor pol′

                        field  exps    : List ℕ
                               ordered : DecrOrdered exps   -- e1 > ... > en 

monPol : ℕ → Pol
monPol e =  pol′ (e ∷ []) (DecrOrdered.single e)

open Tri

------------------------------------------------------------------------------
mon+ : ℕ → Pol → Pol
mon+ e (pol′ es ord) =  aux es ord
  where
  aux : (es : List ℕ) → DecrOrdered es → Pol

  aux []        _         = monPol e
  aux (e' ∷ es) ord-e'es  with compare e e'
  ...
      | tri> _ _ e>e' =  pol′ (e ∷ e' ∷ es) ord-ee'se 
                         where
                         postulate  ord-ee'se : DecrOrdered (e ∷ e' ∷ es)
                         ---------
                         
  ... | tri< e<e' _ _ =  pol′ (e' ∷ esG) ord-e'esG 
                         where
                         ord-es : DecrOrdered es
                         ord-es = tailOrdered ord-e'es

                         esG = Pol.exps (aux es ord-es)

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

  ... | tri≈ _ e≡e' _ =  pol′ (e ∷ es) ord-ees
                         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


------------------------------------------------------------------------------
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')