Hi!
pnil : Prefix nil bs
What is bs doing in the pnil case? nil is a prefix of any list?
I don't see why this is an absurd suggestion; if I had a function to calculate all possible prefixes of a given list I would expect the empty prefix to appear each time i ran it. In epigram that function might well return elements of this 'Prefix xs xsys' type, each saying 'xs' is a prefix of the list 'xsys' which is the list you gave. If we were feeling more adventurous we might build a 'Concat xs ys xsys' relation which would pack the remainder of the list after the prefix it may well have the constructor:
nilconc : Concat nil ys ys
I changed it to 'as' just to see what happens and everything remained green!
Of course, 'as' is more general than 'pnil' so the new construtor will work in more cases not less, in no way are we exploiting the information contained in proofs of prefixivity so we can't see how this new definition fails to capture the right meaning.
It is absurd however to claim that [4] is a prefix of [1,2,3].
takewhileaux asbs (yes a) (tw as p q) => tw ? (pcons p ?) (lcons a q)
The confusion arose when I tried to fill in the question marks in the
definition of takewhileaux. VFL says you can use ? if Epigram can figure
out what goes there...but I couldn't!
Yes you could, this is almost the right answer:
Tried
1. (pcons p a) from the typing of (pcons): its yellow
But Epigram has twarted you by calling the proof that the head of the target list satisfies the predicate 'a' when you'd rather that the head itself was called 'a' and the proof something else entirely. Fix? You need to get the code in emacs and replace that line with:
takewhileaux asbs _ P _ a (yes Pa) (tw as p q) => tw (cons a as) (pcons p a) (lcons Pa q)
This explicity tells the system that you want the head of the list to be called 'a' and the proof 'Pa', it's a horrible thing to have to do, we know.
and I concluded that ?s should not remain after elaboration!
Yup, it's on the list, I think there should be two kinds of question mark one that Epigram replaces with the right term and one that behaves as now
Is there
any way of convincing epigram to spit back the term it found appropriate
instead of the ??
No, unfortunately not (unless you count this list :)
And could I please have an example which demonstrates
it works: inspect takewhile ?????.
Certainly, I'm not sure which version of this you have so forgive me if i call things by the wrong name but if you define IsZero like this:
------------------------------------------------------------------------------
( p : zero = (suc n) !
let !---------------------!
! kill p : False )
kill p <= case p
------------------------------------------------------------------------------
( n : Nat !
let !----------------------------!
! IsZero n : Dec (zero = n) )
IsZero n <= case n
{ IsZero zero => yes refl
IsZero (suc n) => no kill
}
------------------------------------------------------------------------------
(That is to say IsZero is a proof that we can decide whether a given Nat is zero or not)
We can then ask the system:
inspect takewhile IsZero (cons zero (cons zero (cons zero (cons (suc zero) nil))))
A more useful thing would be 'takewhile IsNotZero':
------------------------------------------------------------------------------
( dp : Dec P !
let !----------------------!
! Opp dp : Dec (Not P) )
Opp dp <= case dp
{ Opp (yes a) => no (lam f => f a)
Opp (no f) => yes f
}
------------------------------------------------------------------------------
(If I can decide whether something is true I can also decide whether it is false :)
inspect takewhile (lam n : Nat => Opp (IsZero n))
(cons (suc zero) (cons (suc (suc zero)) (cons zero (cons (suc zero) nil))))
I won't spoil the suprise as to the answer to these inspects
Cheers
Peter
RSS Feed