[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