The Coq mailing list

[Andrew Cave <acave1 AT cs.mcgill.ca>]

The standard trick to encode IR in Coq is to index by the result you
want to compute.

Inductive Foo : nat -> Set :=
| fooA (n: nat) : Foo n
| fooPlus n1 (f1: Foo n1) n2 (f2: Foo n2) : Foo (n1 + n2)
| fooWeird n1 (f1: Foo n1) n2 (f2: Foo n2) (f3: Foo 10) : Foo (n1 + n2 + 10).

Now {n : nat & Foo n} corresponds to your old Foo. This trick goes
quite far, with the caveat that if you're using it to compute Types
then you have to go up a universe level. See e.g.
www.cs.ru.nl/~venanzio/publications/induction_recursion.ps



On Thu, Aug 29, 2013 at 6:38 PM, t x 
<txrev319 AT gmail.com>
 wrote:
> Jason: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AgdaVsCoq
> agrees with you.
>
> Rui: interesting, I think this suffices.
>
>
> On Thu, Aug 29, 2013 at 9:43 PM, Rui Baptista 
> <rpgcbaptista AT gmail.com>
> wrote:
>>
>> What about:
>>
>> Inductive Foo' :=
>> | fooA (n: nat)
>> | fooPlus (f1: Foo') (f2: Foo')
>> | fooWeird (f1: Foo') (f2: Foo') (f3: Foo').
>>
>> Fixpoint evalFoo f :=
>> match f with
>> | fooA n => n
>> | fooPlus f1 f2 => (evalFoo f1 ) + (evalFoo f2)
>> | fooWeird f1 f2 f3 => (evalFoo f1) + (evalFoo f2) + (evalFoo f3)
>> end.
>>
>> Definition Foo :=
>>   {f1 : Foo' | forall f2 f3 f4, f1 = fooWeird f2 f3 f4 -> evalFoo f4 =
>> 10}.
>
>