I have an inductive type
Inductive fin : nat -> Set :=
| First : forall n, fin (S n)
| Next : forall n, fin n -> fin (S n).
Coq cannot deduce that if something is of type fin 1
then it must be exactly First 0
. How do I prove the following lemma? Unfortunately I cannot use dependent destruction
.
Lemma fin_1_first : forall (i : fin 1), i = First 0.
If you don't want to use Equations, there is the tactic depedent induction
from Require Import Stdlib.Program.Equality
. Otherwise, you can prove an inversion lemma by hand, but that it is a bit complicated and I doubt it is the expected answer. I suggest you ask your teacher. You can also just check if there is already such a lemma in the library you are allowed.
Inductive fin : nat -> Set :=
| First : forall n, fin (S n)
| Next : forall n, fin n -> fin (S n).
Definition inv_finSn : forall n (i : fin (S n)), (i = First n) + {j : fin n | i = Next n j} :=
fun n i =>
match i as o in (fin m') return (
match m' return (fin m' -> Type) with
| 0 => fun _ => False
| S m' => fun i => ((i = First _) + {j : fin m' | i = Next _ j})%type
end o)
with
| First _ => inl eq_refl
| Next _ j => inr (exist _ j eq_refl)
end.
Lemma fin_1_first : forall (i : fin 1), i = First 0.
intros i. destruct (inv_finSn _ i) as [H | H].
- assumption.
- destruct H as [j e]. inversion j.
Qed.