0

I am trying to define the rank of a variable in a BES. A BES is defined as a list of equations, and a variable is an inhabitant of the set of propositional variables, which is not an inductive type:

Variable propVar : Set.

Definition rank (E:BES)(x:propVar) : nat :=
let fix block(E':BES)(curMu:bool) : nat := 
match E' with
| nil => fail
| cons (mu xc _) E2 => 
  if xc=x then (if curMu then O else S(O))
    else (if curMu then block E2 true else S(block E2 false))
| cons (nu xc _) E2 => 
  if eqb xc x then (if curMu then S(O) else O)
    else (if curMu then S(block E2 false) else block E2 true)
end
in
block E false.

However, Coq does not accept this definition because xc=x is of type Prop, and Coq expects something of type Bool.

Is it possible to define decidable equality on propVar similar to bool_dec, so that I can use this instead of xc=x?

1 Answer 1

1

You should add

Parameter propVardec : forall x y: propVar, {x = y}+{x <> y}.

This statement adds the hypothesis that every element of propVar are equal or different, making your type decidable.

You could also define

Parameter propVarbeq : propVar -> propVar -> bool.

Which is more or less the same. The main difference is that the first one provides you with the proof of equality (or difference) where the second one only tells you if they are equal or not.

If you ever instantiate your propVar type, you should also prove/instantiate these two functions.

1
  • Thanks, that helped. However, I am going with Definition propVar := nat. Since this also satisfies everything I need from it. Jan 29, 2016 at 10:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.