Hi everyone,

I am wondering how can I write the proof of FS_inj in tactic mode. I am trying to understand the proof written in the library, and one of the problem I am facing with the library proof is a lot of details in pattern matching. (I can write it using `Eqdep.EqdepTheory.inj_pair2`

but I am curious about the proof in library).

```
(* library version *)
Lemma FS_inj :
forall {n} (x y : Fin.t n), FS x = FS y -> x = y.
Proof.
intros ? ? ? Heq.
refine
match
Heq in _ = a
return
match
a as a' in Fin n
return
match n with
| 0 => Prop
| S n' => Fin n' -> Prop
end
with
| Fz => fun _ => True
| Fs y => fun x' => x' = y
end x
with
| eq_refl => eq_refl
end.
Qed.
Lemma FS_inj :
forall {n} (x y : Fin.t n), FS x = FS y -> x = y.
Proof.
intros ? ? ? Heq.
inversion Heq as (Heqq).
apply Eqdep.EqdepTheory.inj_pair2.
exact Heqq.
Qed.
```

You can think of these theorems as instances of `f_equal : a = b -> f a = f b`

, here with `a = FS x`

, `b = FS y`

, `f : Fin.t (S n) -> Fin.t n`

the predecessor function.

Thanks @Li-yao . Nice way to think about these proofs.

Last updated: Jun 20 2024 at 13:02 UTC