[Agda] Induction-induction in a tricky order

[Simon Boulier]

Thanks for both answers!
I'll have a closer look but it seems to be exactly what I was looking for.

Simon



Le 15/03/2016 17:08, Fredrik Nordvall Forsberg a écrit :
> Hi Simon,
>
> On 15/03/16 14:06, Simon Boulier wrote:
>> Is it a way to type check the following:
>>
>>     data Foo  : Set
>>     data Bar  : Foo → Set
>>     data Bar2 : Foo → Set
>>
>> [...]
>>       bar'  : (x : Foo) → Bar (foo x (bar x) (bar2 x))
>> [...]
>>       bar2  : (x : Foo) → Bar2 x
> So to summarise, you want a constructor for Bar which has a constructor
> for Bar2 in its index. In this particular case, since Bar and Bar2 are
> not dependent on each other, you can introduce them simultaneously by
> indexing them over a two-element type, and then interleave the
> constructors as you wanted to do. By defining syntactic sugar for Bar
> and Bar2 early using new-style mutual blocks, we can make the definition
> look quite natural:
>
> -------------------------------------------------
>
> open import Data.Bool
>
> data Foo  : Set
> data Bar-and-Bar2 : Foo → Bool → Set
>
> Bar : Foo → Set
> Bar x = Bar-and-Bar2 x true
>
> Bar2 : Foo → Set
> Bar2 x = Bar-and-Bar2 x false
>
> data Foo where
>   foo   : (x : Foo) → Bar x → Bar2 x → Foo
>
> data Bar-and-Bar2 where
>   bar   : (x : Foo) → Bar x
>   bar2  : (x : Foo) → Bar2 x
>   bar'  : (x : Foo) → Bar (foo x (bar x) (bar2 x))
>   bar2' : (x : Foo) → Bar2 (foo x (bar x) (bar2 x))
>
> -------------------------------------------------
>
> If you want also Bar2 to be indexed over Bar, i.e.
>
>   data Foo  : Set
>   data Bar  : Foo → Set
>   data Bar2 : (x : Foo) → Bar x → Set
>
> this encoding does not work any more (without Hickey's Very Dependent
> Types). However Agda lets us work around this by simultaneously defining
> an auxiliary copy of the constructor in question (I learnt about this
> trick from Ulf Norell on this mailing list):
>
>   data Foo  : Set
>   data Bar  : Foo → Set
>   data Bar2 : (x : Foo) → Bar x → Set
>   bar2aux : (x : Foo) → (y : Bar x) → Bar2 x y
>
> This way earlier constructors know about the existence of bar2aux, and
> after the real bar2 has been introduced, we can simply define
> bar2aux = bar2. Note that this is *not* an instance of
> (induction-)induction-recursion, but something weirder, because the
> (trivially) recursively defined function bar2aux does not have as
> codomain some already defined type D.
>
> Here is your example again in this setting:
>
> -------------------------------------------------
>
> data Foo  : Set
> data Bar  : Foo → Set
> data Bar2 : (x : Foo) → Bar x → Set
> bar2aux : (x : Foo) → (y : Bar x) → Bar2 x y
>
> data Foo where
>   foo   : (x : Foo) → (y : Bar x) → Bar2 x y → Foo
>
> data Bar where
>   bar   : (x : Foo) → Bar x
>   bar'  : (x : Foo) → Bar (foo x (bar x) (bar2aux x (bar x)))
>
> data Bar2 where
>   bar2  : (x : Foo) → (y : Bar x) → Bar2 x y
>   bar2' : (x : Foo) → Bar2 (foo x (bar x) (bar2aux x (bar x))) (bar' x)
>
> bar2aux = bar2
>
> bar'-has-right-type-because-this-is-accepted
>   : (x : Foo) → Bar (foo x (bar x) (bar2 x (bar x)))
> bar'-has-right-type-because-this-is-accepted = bar'
>
> also-bar2'-has-right-type
>   : (x : Foo) → Bar2 (foo x (bar x) (bar2 x (bar x))) (bar' x)
> also-bar2'-has-right-type = bar2'
>
> -------------------------------------------------
>
> Semantically, it seems like it is possible to understand the meaning of
> definitions like this (without the bar2aux encoding) in the same way
> that we give semantics to the mutual dependencies of higher inductive types.
>
> Hope that helps, and cheers,
> Fredrik
>


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
Url : http://lists.chalmers.se/pipermail/agda/attachments/20160315/e5299bd3/signature.bin