[TYPES] Proof term for proof by exhaustion
Param Jyothi Reddy
paramr at gmail.com
Tue Jul 10 14:26:46 EDT 2007
Lets define vector in usual way with constructors:
nil : Vector T 0
cons : Vector T n -> T -> Vector T (S n)
along with its inductive elimination rule. Let BD be type of Binary
Digits (enumeration with elements 0 and 1).
Also lets say i have proofs of some predicate P for all elements of
Vector's over BD of length 2, i.e.
p_0 : P(00), p_1 : P(01), p_2 : P(10), p_3 : P(11), where bd is cons
(cons nil d) b.
using these How will the proof term for
(forall v : Vector BD (S S 0) ). P(v) look like?
I can use or elimination if i could build proof for:
(forall v : Vector BD (S S 0)). v == 00 or v == 01 or v == 10 or v ==
11. However i am not sure how the proof term for this looks either.
Can someone help me understand this?
More information about the Types-list