## Stream: Coq users

### Topic: Proof of FS_inj in tactic mode

#### Mukesh Tiwari (Jun 04 2022 at 19:25):

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.
``````

#### Li-yao (Jun 04 2022 at 20:23):

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.

#### Mukesh Tiwari (Jun 05 2022 at 09:26):

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

Last updated: Oct 03 2023 at 04:02 UTC