rocq-provercoq-tactic

Prove that an element of fin 1 is exactly 0


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.

Solution

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