Stream: Coq users

Topic: Proof of FS_inj in tactic mode


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mukesh Tiwari (Jun 05 2022 at 09:26):

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


Last updated: Feb 04 2023 at 22:29 UTC