Consider the simple indexed inductive type
Inductive Single : nat -> Set :=
| single_O : Single O
| single_S {n} : Single n -> Single (S n).
Intuitively, I thought that Single n
has a unique value for each n : nat
.
I started by trying to prove that forall s : Single O, s = single_O
.
However, the usual tactics inversion
, destruct
, and induction
did not work:
Lemma single_O_unique (s : Single O) : s = single_O.
inversion s. (* No effect *)
Fail destruct s.
Fail induction s.
The error messages were:
Abstracting over the terms "n" and "s" leads to a term
fun (n0 : nat) (s0 : Single n0) => s0 = single_O
which is ill-typed.
Reason is: Illegal application:
The term "@eq" of type "forall A : Type, A -> A -> Prop"
cannot be applied to the terms
"Single n0" : "Set"
"s0" : "Single n0"
"single_O" : "Single 0"
The 3rd term has type "Single 0" which should be coercible to
"Single n0".
So I resorted to a manual match
expression:
refine match s with
| single_O => _
| single_S _ => _
end.
Resulting in the following proof context:
s: Single 0
(1/2)
single_O = single_O
(2/2)
IDProp
which was puzzling, but easy to prove:
- reflexivity.
- exact idProp.
Qed.
Questions:
Why was
inversion
unable to recognize thats
could only besingle_O
and substitute accordingly?Why did the
refine
tactic produce the subgoalIDProp
?Is there a way to get
inversion
ordestruct
to work in this case? Or, what would a better way to proves = single_O
?
Full example:
Inductive Single : nat -> Set :=
| single_O : Single O
| single_S {n} : Single n -> Single (S n).
Lemma single_O_unique (s : Single O) : s = single_O.
inversion s. (* No effect *)
Fail destruct s.
Fail induction s.
refine match s with
| single_O => _
| single_S _ => _
end.
- reflexivity.
- exact idProp.
Qed.