Require Import List.
Import ListNotations.
Require Import StructTact.StructTactics.

Set Implicit Arguments.

Inductive Nth {A : Type} : list A -> nat -> A -> Prop :=
| Nth_0 : forall x l, Nth (x :: l) 0 x
| Nth_S : forall l x n y, Nth l n x -> Nth (y :: l) (S n) x.

Section nth.
  Variable A : Type.

  Lemma nth_error_Nth :
    forall n l (x : A),
      nth_error l n = Some x ->
      Nth l n x.
  Proof using.
(* Goal: forall (n : nat) (l : list A) (x : A) (_ : @eq (option A) (@nth_error A l n) (@Some A x)), @Nth A l n x *)
    induction n; intros; simpl in *; auto.
    - break_match; try discriminate.
(* Goal: @Nth A (@cons A a l0) O x *)
      unfold value in *.
(* Goal: @Nth A (@cons A a l0) O x *)
      find_inversion.
(* Goal: @Nth A (@cons A a l0) (S n) x *)
      constructor.
    - break_match; try discriminate.
(* Goal: @Nth A (@cons A a l0) (S n) x *)
      subst. constructor.
(* Goal: @Nth A l0 n x *)
      eauto.
  Qed.

  Lemma Nth_nth_error :
    forall n l (x : A),
      Nth l n x ->
      nth_error l n = Some x.
  Proof using.
(* Goal: forall (n : nat) (l : list A) (x : A) (_ : @Nth A l n x), @eq (option A) (@nth_error A l n) (@Some A x) *)
    intros.
(* Goal: @eq (option A) (@nth_error A l n) (@Some A x) *)
    induction H; simpl in *; auto.
  Qed.
End nth.
