The Coq mailing list

[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].
>>
>