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: Oct 13 2024 at 01:02 UTC