The Coq mailing list

[Gyesik Lee <gslee AT ropas.snu.ac.kr>]

Sorry, there was some typos in my previous email.

[Rep] stands for [toto] in my first email.
(a problem of copy-and-paste)

Gyesik


2010/10/12 Gyesik Lee 
<gslee AT ropas.snu.ac.kr>:
> Hi Adam,
>
>> This property doesn't even type-check for [bool], but it's a mistake to
>> conclude that it isn't easy to "use [bool]s as types."  Just use the 
>> boolean
>> as the index to this type family:
>>
>>    Inductive sing : bool -> Type := Sing : sing true.
>>
>> There are other encodings you could consider, too.
>
> Yes, you are right. It was my mistake to have ruled out the boolean.
> Although I didn't succeed in making direct use of [sing] or similar
> things, I got another idea.
>
> I just defined a boolean version of [VarIn] and used it to do a decision.
> Here is my solution.
>
> Fixpoint bVarIn (r:Rep) : bool :=
>  match r with
>    | Var        => true
>    | Plus r0 r1 => if (bVarIn r0) then true else (bVarIn r1)
>    | Unit          => false
>  end.
>
> Fixpoint VarIn (r:Rep) : Prop :=
>  match r with
>    | Var        => True
>    | Plus r0 r1 => if (bVarIn r0) then VarIn r0 else VarIn r1
>    | Unit         => False
>  end.
>
> Then the proof unicity is simple to prove.
>
> Lemma VarIn_unicity : forall r (p q : VarIn r), p = q.
>
> Many thanks for useful helps.
>
> Gyesik
>
>
>
> 2010/10/12 Adam Chlipala 
> <adam AT chlipala.net>:
>> Gyesik Lee wrote:
>>>>
>>>> Why don't you just use [bool] instead of [Prop]?
>>>>
>>>>
>>>
>>> because I want to have the property that there is no term of type
>>> [VarIn r] when its value is False.
>>> But this does not work with the Boolean [false].
>>>
>>
>