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.