[Agda] strange let-in-case-let

Sergei Meshveliani mechvel at botik.ru
Tue Jan 24 14:46:30 CET 2017


On Mon, 2017-01-23 at 13:19 -0800, Martin Stone Davis wrote:
> That does look like strange behavior yet I'm guessing this is not a bug. 
> Would you revise the problem example to be as small as possible and only 
> relying on the Agda.Builtin.*?
> 

See the .agda file attached.

------
Sergei




> On 01/23/2017 03:35 AM, Sergei Meshveliani wrote:
> > People,
> > I have further problems with matching in let+case+let.
> > Consider the following two fragments.
> >
> > open OfMax natDTO using (Maximum; maximum′; maximum ...)
> > open Maximum using (max; all≤max)
> >                     -- Maximum is a record with constructor maximum′
> > ...
> > --------------------------------------------------------- (I) ---
> >   ; (tri≈ _ e≡e' _) →
> >         let
> >           es       = map proj₂ mons
> >           maxStruc = maximum e (e' ∷ es)   -- : Maximum (e ∷ e' ∷ es)
> >           m        = max     maxStruc
> >           ee'es≤m  = all≤max maxStruc
> >           e'es≡ees = PE.sym $ PE.cong (_∷ es) e≡e'
> >           ord-ees  = PE.subst DecrOrderedList e'es≡ees ord-e'es
> >                                                                                  
> >           ees≤m : All (_≤ m) (e ∷ es)
> >           ees≤m = DPrelude.anything
> >         in
> >         ((pol′ ((a + b , e) ∷ mons) ord-ees) , ees≤m)
> > ------------------------------------------------------------------
> >
> > ----------------------------------------------------------- (II) ---
> > ...
> >   ; (tri≈ _ e≡e' _) →
> >         let
> >           es = map proj₂ mons
> >         in
> >         case maximum e (e' ∷ es)
> >         of \
> >         { (maximum′ m _ ee'es≤m) →
> >               let
> >                 e'es≡ees = PE.sym $ PE.cong (_∷ es) e≡e'
> >                 ord-ees  = PE.subst DecrOrderedList e'es≡ees ord-e'es
> >
> >                 ees≤m : All (_≤ m) (e ∷ es)
> >                 ees≤m = DPrelude.anything
> >
> >                 debug : All (_≤ m) (e ∷ e' ∷ es)    -- for more testing
> >                 debug = ee'es≤m
> >               in
> >               ((pol′ ((a + b , e) ∷ mons) ord-ees) , ees≤m)
> >         }
> > ----------------------------------------------------------------------
> >
> > The difference is that in (I) the fields of the result of `maximum' are
> > extracted explicitly, by applying their labels. And in (II) their values
> > are found by matching against the record of the result.
> >
> > (I) is type-checked.
> > And (II) leads to the report
> >
> > ------------------------
> > Cannot instantiate the metavariable _295 to solution All (λ section
> > → section ≤ m) (e ∷ map proj₂ mons) since it contains the variable
> > m which is not in scope of the metavariable or irrelevant in the
> > metavariable but relevant in the solution
> > when checking that the expression ees≤m has type
> > _B_295 upComR a e b e' mons ord-e'es .¬a e≡e' .¬c
> > (pol′ ((a + b , e) ∷ mons)
> >   (PE.subst DecrOrderedList
> >    (PE.sym $ PE.cong (λ section → section ∷ map proj₂ mons) e≡e')
> >    ord-e'es))
> > ------------------------
> >
> > in Agda 2.5.2.
> >
> > This report refers to the line after last "in".
> > I also add the two "debug" lines to make sure that the value of  m
> > is valid in the body of "in".
> >
> > Does this effect show a bug in Agda?
> >
> > (Generally, matching against a record makes many programs nicer).
> >
> > Thank you in advance for explanation,
> >
> > ------
> > 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 Level    using (Level; _⊔_)
open import Function using (flip; _$_; _∘_; case_of_)
open import Algebra.FunctionProperties using (Op₂)
open import Relation.Binary using (DecSetoid; DecTotalOrder; Tri;
                                                             StrictTotalOrder)
open import Relation.Binary.PropositionalEquality as PE using (_≡_)
open import Data.Product using (_×_; _,_; proj₁; proj₂; ∃) 
open import Data.List    using (List; []; _∷_; map)
open import Data.List.All as AllM using (All) 
                                  renaming ([] to []a; _∷_ to _∷a_)
open import Data.List.Any                  using (Any; module Membership)
open import Data.Nat as Nat                using (ℕ; _≤_; _>_) 
open import Data.Nat.Properties as NatProp using () 

                               


--****************************************************************************
postulate anything : ∀ {a} {A : Set a} → A

natDTO       = Nat.decTotalOrder
natSTO       = NatProp.strictTotalOrder
natDecSetoid = DecTotalOrder.Eq.decSetoid natDTO
natSetoid    = DecSetoid.setoid natDecSetoid

open StrictTotalOrder natSTO using (_<_; compare) renaming (trans to <-trans)
open DecTotalOrder    natDTO using ()
                             renaming (refl to ≤refl; trans to ≤trans)
open Any
open Tri
open Membership natSetoid using (_∈_)

record Maximum (xs : List ℕ) : Set 
       where
       constructor maximum′

       field max     : ℕ
             max∈    : max ∈ xs
             all≤max : All (_≤ max) xs


maximum : (x : ℕ) → (xs : List ℕ) → Maximum (x ∷ xs)

maximum x [] =  record{ max = x;  max∈ = here PE.refl;  all≤max = all≤ }
                where
                all≤ : All (_≤ x) (x ∷ [])
                all≤ = x≤x ∷a []a  where  x≤x = ≤refl

maximum x (y ∷ xs) =  anything


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

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

>tail-inDecrOrdered :  ∀ {x xs} → DecrOrderedList (x ∷ xs) → All (x >_) xs
>tail-inDecrOrdered (single _)                 =  []a
>tail-inDecrOrdered (prep2 x y zs x>y ord-yzs) =  anything

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



-------------------------------------------------------------------------------
module _ {α} (C : Set α) 
  where
  Pair = C × ℕ

  Monomial :  Set _
  Monomial =  Pair

  record Pol :  Set α 
    where
    constructor pol′

    field  mons : List Monomial
    -----

    coefs : List C
    coefs = map proj₁ mons

    exps : List ℕ
    exps = map proj₂ mons

    field  expsAreOrdered : DecrOrderedList exps
    -----
           
  monPol : Monomial → Pol
  monPol (c , e) =  pol′ ((c , e) ∷ []) (DecrOrderedList.single e)

  open Maximum

  ----------------------------------------------------------------------------
  addMon : (mon : Monomial) → (f : Pol) → 
           let e = proj₂ mon
               m = max $ maximum e (Pol.exps f) 
           in
           (∃ \ (s : Pol) → All (_≤ m) (Pol.exps s))

  addMon (a , e) (pol′ [] _)  =  (monPol (a , e) , (≤refl ∷a []a))

  addMon (a , e) (pol′ ((_ , e') ∷ mons) ord-e'es) = 
     case 
         compare e e'
     of \ 
     { (tri≈ _ e≡e' _) →  
{-
           let es = map proj₂ mons                  -- (I)
           in  
           case maximum e (e' ∷ es)
           of \ 
           { (maximum′ m _ ee'es≤m) → 
               let
                 e'es≡ees = PE.sym $ PE.cong (_∷ es) e≡e' 
                 ord-ees  = PE.subst DecrOrderedList e'es≡ees ord-e'es

                 ees≤m : All (_≤ m) (e ∷ es)
                 ees≤m = anything 

                 debug : All (_≤ m) (e ∷ e' ∷ es)
                 debug = ee'es≤m
               in
               ((pol′ ((a , e) ∷ mons) ord-ees) , ees≤m)
           }
-}
           let es       = map proj₂ mons            -- (II)
               maxStruc = maximum e (e' ∷ es)                               
               m        = max     maxStruc                                  
               ee'es≤m  = all≤max maxStruc                                  
               e'es≡ees = PE.sym $ PE.cong (_∷ es) e≡e'                     
               ord-ees  = PE.subst DecrOrderedList e'es≡ees ord-e'es        

               ees≤m : All (_≤ m) (e ∷ es) 
               ees≤m = anything            
           in                                                               
           ((pol′ ((a , e) ∷ mons) ord-ees) , ees≤m)

     ; _ → anything
     }


More information about the Agda mailing list