Sized Types [Re: [Agda] proving termination trouble again]

[Andreas Abel]

This must be a freshly introduced bug in Agda-2.2.7

z : ∀ {size} → (n : Nat {↑ size}) → (zero {size} < n) → ∃  
{Nat {size}} (λ m → m < n)
z {i} (zero .{i}) ()
z (suc n) _ = n , (≤-refl (suc n))

produces the same error message

size' != size of type Size
when checking that the pattern zero {.i} has type Nat {↑ size}

It is completely obscure to me what size' should be, and why i is not  
mentioned instead.  Anyway, there should not be an error in the first  
place.

Andreas

On Mar 21, 2010, at 5:27 PM, Ruben Henner Zilibowitz wrote:

> This is an old thread. Nevertheless I tried the file  
> ZilibowitzRubenHenner2.agda with stdlib 0.2 and it still didn't  
> work. Here is the error.
>
> ZilibowitzRubenHenner2.agda:38,3-7
> size' != size of type Size
> when checking that the pattern zero has type Nat
>
> Ruben
>
> On 18/01/2010, at 10:45 PM, Andreas Abel wrote:
>
>> That is an issue with universe polymorphism.
>> I am using stdlib 0.2 without uni poly.
>>
>> Probably there is just a level argument (to Rel) missing?!
>>
>> Cheers,
>> Andreas
>>
>> On Jan 17, 2010, at 12:24 AM, Ruben Henner Zilibowitz wrote:
>>
>>> Hi Andreas,
>>>
>>> Thanks, but it doesn't work. I'm using agda 2.2.6 with standard  
>>> lib 0.3 by the way.
>>>
>>> ZilibowitzRubenHenner2.agda:26,12-25
>>> (ℓ : .Level.Level) → Set (.Level._⊔_ .Level.zero (.Level.suc  
>>> ℓ))
>>> !=< _18 of type Setω
>>> when checking that the expression Rel (Nat {∞}) has type _18
>>>
>>> Ruben
>>>
>>> On 16/01/2010, at 12:07 PM, Andreas Abel wrote:
>>>
>>>> Hi Ruben,
>>>>
>>>> here is a translation of your code into something very similiar  
>>>> that uses a sized type of natural numbers.  Unfortunately, sized  
>>>> types are not well integrated into Agda yet, so a sizes have to  
>>>> be declared explicitely, and the standard library, which does not  
>>>> use sized types, is not usable.
>>>>
>>>> <ZilibowitzRubenHenner2.agda>
>>>>
>>>> A few things you need to know:
>>>> - Unspecified sizes default to \infty.  For instance, "Nat" is  
>>>> really "Nat {\infty}"
>>>> - The successor \uparrow is not a constructor, it cannot be  
>>>> matched, but it can appear in dot-patterns.
>>>> - Things are a bit fiddly, so I had to try a bit which sizes I  
>>>> need to mention explicitly and which can be inferred sensibly.
>>>> - It is advisable to turn on hidden arguments to see where stuff  
>>>> fails.
>>>>
>>>> If you look at the example where I made sizes more explicit, you  
>>>> see that the mutual functions j and helper terminate on the first  
>>>> argument "size".  It is decreasing in the call j-->helper and  
>>>> unchanged in the call back.
>>>>
>>>> j : ∀ {size} → Nat {size} -> Nat
>>>> j zero = zero
>>>> j .{↑ size} (suc {size} n) = helper {size} (suc n) (z (suc n)  
>>>> (s≤s z≤n))
>>>> where
>>>> helper : {size : Size} -> (sn : Nat {↑ size}) -> ∃ {Nat  
>>>> {size}} (λ n → n < sn) -> Nat
>>>> helper {size} sn (n , _) = j {size} n
>>>>
>>>> Hope that helps,
>>>> Cheers,
>>>> Andreas
>>>>
>>>> On Jan 16, 2010, at 12:25 AM, Ruben Henner Zilibowitz wrote:
>>>>
>>>>> Hi Andreas,
>>>>>
>>>>> Below is a slightly simpler example. Function j does not  
>>>>> termination check. Would you be so kind as to demonstrate how to  
>>>>> use sized types to fix this?
>>>>> I'm having some trouble figuring out how sized types are  
>>>>> supposed to work exactly.
>>>>>
>>>>> Thanks,
>>>>> Ruben
>>>>>
>>>>> -----------
>>>>>
>>>>> module TerminationTwoConstructors where
>>>>>
>>>>> open import Data.Nat
>>>>> open import Relation.Binary
>>>>> open import Relation.Binary.PropositionalEquality
>>>>> open import Data.Product
>>>>>
>>>>> ≤-refl : _≡_ ⇒ _≤_
>>>>> ≤-refl = IsPreorder.reflexive (IsPartialOrder.isPreorder  
>>>>> (IsTotalOrder.isPartialOrder (IsDecTotalOrder.isTotalOrder  
>>>>> (DecTotalOrder.isDecTotalOrder decTotalOrder))))
>>>>>
>>>>> z : (n : ℕ) → (0 < n) → ∃ (λ m → m < n)
>>>>> z zero ()
>>>>> z (suc n) _ = n , ≤-refl refl
>>>>>
>>>>> j : ℕ -> ℕ
>>>>> j zero = zero
>>>>> j (suc n) = helper (suc n) (z (suc n) (s≤s z≤n))
>>>>> where
>>>>> helper : (sn : ℕ) -> ∃ (λ n → n < sn) -> ℕ
>>>>> helper sn (n , _) = j n
>>>>>
>>>>> On 12/01/2010, at 8:41 PM, Andreas Abel wrote:
>>>>>
>>>>>> Hi Ruben,
>>>>>>
>>>>>> from the perspective of the termination checker, there is no  
>>>>>> difference in g and h.  The proofs of equality/leq are not used  
>>>>>> by the termination checker, it only honors structural  
>>>>>> ordering.  It "sees" that
>>>>>>
>>>>>> sn < suc (suc n)
>>>>>>
>>>>>> by composing the calls g --> helper --> g.
>>>>>>
>>>>>> For function i to termination check, it would have to evaluate  
>>>>>> proj_1 whee, but the termination checker does not do any  
>>>>>> evaluation (since evaluation (1) is safe only after termination  
>>>>>> checking, and (2) leads to unfeasible termination checking (see  
>>>>>> the Coq guardedness checker)).
>>>>>>
>>>>>> If you want to propagate termination arguments (like sn < ssn)  
>>>>>> through functions and data structures, you need more  
>>>>>> informative typing, like sized types.
>>>>>>
>>>>>> Cheers,
>>>>>> Andreas
>>>>>>
>>>>>> On Jan 11, 2010, at 2:24 PM, Ruben Henner Zilibowitz wrote:
>>>>>>
>>>>>>> In relation to issue 59:
>>>>>>>
>>>>>>> http://code.google.com/p/agda/issues/detail?id=59&can=1&q=termination
>>>>>>>
>>>>>>> Here is another problem I've encountered along similar lines.  
>>>>>>> In the code below, the functions f, g, h, and i all are in  
>>>>>>> principal the same. However, only g and h pass the termination  
>>>>>>> checker. Function f suffers from the problem in issue 59.  
>>>>>>> Function g solves it with the same workaround suggested in  
>>>>>>> issue 59. Function h solves it in a similar way. The problem  
>>>>>>> is function i. It is very similar to function h but the  
>>>>>>> argument (sn < ssn) in the helper function is concealed inside  
>>>>>>> a product type and needs to be extracted using proj₂ which  
>>>>>>> breaks this example. Is this a bug? Sorry for the hard to read  
>>>>>>> code and function names..
>>>>>>>
>>>>>>> The code below is based on Andreas Abel's earlier example..
>>>>>>>
>>>>>>> Ruben
>>>>>>>
>>>>>>> ----------
>>>>>>>
>>>>>>> module TerminationTwoConstructors where
>>>>>>>
>>>>>>> open import Data.Nat
>>>>>>> open import Relation.Binary
>>>>>>> open import Relation.Binary.PropositionalEquality
>>>>>>> open import Data.Product
>>>>>>>
>>>>>>> bla : ℕ -> ℕ
>>>>>>> bla m = m
>>>>>>>
>>>>>>> f : ℕ -> ℕ
>>>>>>> f zero = zero
>>>>>>> f (suc zero) = zero
>>>>>>> f (suc (suc n)) with bla (suc (suc n))
>>>>>>> ... | m = f (suc n)
>>>>>>>
>>>>>>> g : ℕ -> ℕ
>>>>>>> g zero = zero
>>>>>>> g (suc zero) = zero
>>>>>>> g (suc (suc n)) = helper (suc (suc n)) (suc n) refl (bla (suc  
>>>>>>> (suc n)))
>>>>>>> where
>>>>>>> helper : (ssn : ℕ) -> (sn : ℕ) -> (suc sn ≡ ssn) -> (m :  
>>>>>>> ℕ) -> ℕ
>>>>>>> helper ssn sn _ m = g sn
>>>>>>>
>>>>>>> ≤-refl : _≡_ ⇒ _≤_
>>>>>>> ≤-refl = IsPreorder.reflexive (IsPartialOrder.isPreorder  
>>>>>>> (IsTotalOrder.isPartialOrder (IsDecTotalOrder.isTotalOrder  
>>>>>>> (DecTotalOrder.isDecTotalOrder decTotalOrder))))
>>>>>>>
>>>>>>> h : ℕ -> ℕ
>>>>>>> h zero = zero
>>>>>>> h (suc zero) = zero
>>>>>>> h (suc (suc n)) = helper (suc (suc n)) (suc n) (≤-refl refl)  
>>>>>>> (bla (suc (suc n)))
>>>>>>> where
>>>>>>> helper : (ssn : ℕ) -> (sn : ℕ) -> (sn < ssn) -> (m : ℕ) - 
>>>>>>> > ℕ
>>>>>>> helper ssn sn _ m = h sn
>>>>>>>
>>>>>>> zog : (n : ℕ) -> (ℕ × n < suc n)
>>>>>>> zog n = n , ≤-refl refl
>>>>>>>
>>>>>>> i : ℕ -> ℕ
>>>>>>> i zero = zero
>>>>>>> i (suc zero) = zero
>>>>>>> i (suc (suc n)) = let whee = zog (suc n) in helper (suc (suc  
>>>>>>> n)) (proj₁ whee) (proj₂ whee) (bla (suc (suc n)))
>>>>>>> where
>>>>>>> helper : (ssn : ℕ) -> (sn : ℕ) -> (sn < ssn) -> (m : ℕ) - 
>>>>>>> > ℕ
>>>>>>> helper ssn sn _ m = i sn
>>>>>>
>>>>>> Andreas ABEL
>>>>>> INRIA, Projet Pi.R2
>>>>>> 23, avenue d'Italie
>>>>>> F-75013 Paris
>>>>>> Tel: +33.1.39.63.59.41
>>>>>>
>>>>>>
>>>>>>
>>>>>
>>>>>
>>>>>
>>>>
>>>> Andreas ABEL
>>>> INRIA, Projet Pi.R2
>>>> 23, avenue d'Italie
>>>> F-75013 Paris
>>>> Tel: +33.1.39.63.59.41
>>>>
>>>>
>>>>
>>>
>>>
>>>
>>
>> Andreas ABEL
>> INRIA, Projet Pi.R2
>> 23, avenue d'Italie
>> F-75013 Paris
>> Tel: +33.1.39.63.59.41
>>
>>
>>
>
>
>

Andreas ABEL
INRIA, Projet Pi.R2
23, avenue d'Italie
F-75013 Paris
Tel: +33.1.39.63.59.41