Very simple question regarding typepred or the like

[Peter Gumm]

Suppose I have a type defined as 

S : Type = {0,1} 

and I want to prove 

forall (x:S): x=0 or x=1

I would have expected, that after a (skeep) i could use 

(typepred x)

Unfortunately, that does not work. The only way I know how to finish the proof is with 

(assert)

However, this being a black box I'd rather see a basic proof command to make progress.

Which is the one I am missing?

H. Peter 

[Mariano Moscato]

Hi Peter,

I'm sorry for the (so) late response.

The typepred command does not add any information to the sequent because the enumeration types, as the one you define in your message, are supported as syntactic sugar for abstract datatype definitions. Then, the S type is for PVS an uninterpreted type for which some axioms are added automatically by the typechecker. You can see those by using the `prettypint-expanded` emacs command.

Unfortunatly, as long as I know, the easiest way to prove the lemma you propose (besides `assert`) is using the induction schema defined for the datatype (see below). 

This could look like an overkill, but it has to be proved in this way because of the way the properties on the ADTs are implicitly expressed by those axioms.

(""
 (NAME "P" "lambda(x: S): x = 0 OR x = 1")
 (LEMMA "S_induction")
 (INST -1 "P")
 (SPLIT -1)
 (("1" (EXPAND "P" :ASSERT? NONE) (PROPAX))
  ("2" (REPLACE -1 :HIDE? T :DIR RL) (BETA 1) (PROPAX))
  ("3" (REPLACE -1 :HIDE? T :DIR RL) (BETA 1) (PROPAX))))

Hope it helps.

Kindly,

Mariano.

[Peter Gumm]

Thanks for your explanation. It makes perfect sense. 
H.Peter