Блог

Я хочу доказать приведенную ниже лемму.

 Require Import Coq.Vectors.Vector.

Lemma t (A:Type)(n:nat)(v:t A (n 0)): fst (splitat n v)    (nil A) = v.
Proof.
induction n.
refine (match v with (nil _) => _ end).
reflexivity.
remember (splitat (S n) v).
Abort.
  

Как мне научить Coq, который fst (splitat n v) совпадает с v?

Вы можете преобразовать векторы в списки. (Примечание: в приведенном ниже примере я использую язык доказательства ssreflect, который, на мой взгляд, проще для написания анализа случаев и индукции для этих зависимых типов данных.)

 From Coq Require Import ssreflect.
Require Import Coq.Lists.List.
Require Import Coq.Vectors.Vector.

Import VectorNotations.

Lemma to_list_injective A n (v1 v2 : Vector.t A n) :
  to_list v1 = to_list v2 -> v1 = v2.
Proof.
elim: n / v1 v2=> [|x1 n v1 IH] /= v2.
- by elim/@case0: v2.
- by elim/@caseS': v2=> x2 v2 [-> /IH ->].
Qed.

Lemma to_list_splitat1 A n m (v : Vector.t A (n   m)) :
  to_list (fst (splitat n v)) = firstn n (to_list v).
Proof.
elim: n v=> [|n IH] //=.
elim/@caseS'=> x v /=.
rewrite -IH.
by case: (splitat n v).
Qed.

Lemma to_list_app A n m (v1 : Vector.t A n) (v2 : Vector.t A m) :
  to_list (v1    v2) = (to_list v1    to_list v2)%list.
Proof.
elim: n / v1=> [//|x1 n v1 /= IH].
by congr List.cons.
Qed.

Lemma length_to_list A n (v : Vector.t A n) : length (to_list v) = n.
Proof.
by elim: n / v=> [//|/= x n v ->].
Qed.

Lemma l (A:Type)(n:nat)(v:t A (n 0)): fst (splitat n v)    (nil A) = v.
Proof.
apply: to_list_injective.
rewrite to_list_app app_nil_r to_list_splitat1.
by rewrite {1}[n]plus_n_O -{1}(length_to_list _ _ v) firstn_all.
Qed.
  

Я нашел более простое доказательство.

 Lemma l (A:Type)(n:nat)(v:t A (n 0)): fst (splitat n v)    (nil A) = v.
Proof.
induction n.
refine (match v with Vector.nil _ => _ end).
reflexivity.
simpl.
rewrite (surjective_pairing (splitat n (Vector.tl v))).
simpl.
rewrite (IHn (tl v)).
rewrite <- eta.
reflexivity.
Qed.