extraction des preuves de l'égalité de correspondance

Question

Je suis en train de faire les travaux suivants:

Definition gen `{A:Type} 
      {i o: nat} 
      (f: nat -> (option nat)) 
      {ibound: forall (n n':nat), f n = Some n' -> n' < i} 
      (x: svector A i) (t:nat) (ti: t < o): option A 
    := match (f t) with 
    | None => None 
    | Some t' => Vnth x (ibound t t' _) 
    end. 

En dernier lieu de « _ » Je besoin d'une preuve que « f t » est égal à égal à «Certains t». Je ne pouvais pas comprendre comment l'obtenir du match. Est définie comme vne:

Vnth 
    : ∀ (A : Type) (n : nat), vector A n → ∀ i : nat, i < n → A 

Answer 1

L'écriture de cette fonction nécessite une instance de ce qu'on appelle le modèle du convoi (voir here). Je crois que ce qui suit devrait fonctionner, bien que je ne puisse pas le tester, puisque je n'ai pas le reste de vos définitions.

Definition gen `{A:Type} 
      {i o: nat} 
      (f: nat -> (option nat)) 
      {ibound: forall (n n':nat), f n = Some n' -> n' < i} 
      (x: svector A i) (t:nat) (ti: t < o): option A 
    := match f t as x return f t = x -> option A with 
    | None => fun _ => None 
    | Some t' => fun p => Vnth x (ibound t t' p) 
    end (eq_refl (f t)).