proposition: Lemma word_indexed_correct : forall n (i : Fin.t n) (t : t (word sz) n), NoDupVector t -> match word_indexed (nth t i) t with | Some w' => i = w' | None => False end.
proof: Proof. clear. induction i. - intro; pattern n, t; apply Vector.caseS; simpl; intros. rewrite (proj2 (weqb_true_iff h h)); eauto. - intro; generalize i (IHi (Vector.tl t)); clear. pattern n, t; apply Vector.caseS; simpl. intros h n0 t0 i; case_eq (word_indexed (nth t0 i) t0); intros; apply NoDupVector_invert in H1; intuition subst. case_eq (weqb (nth t0 t1) h); intros; eauto. apply weqb_true_iff in H0; subst. destruct H2; generalize t0 H; clear; induction t1. + intro; pattern n, t0; apply Vector.caseS; simpl; intros; econstructor. + intro; revert t1 IHt1; pattern n, t0; apply Vector.caseS; simpl; intros. case_eq (weqb (nth t t1) h); intros; eauto. * apply weqb_true_iff in H0; subst; econstructor. * rewrite H0 in H. econstructor 2; apply IHt1. destruct (word_indexed (nth t t1) t); try discriminate. f_equal; apply Fin.FS_inj; congruence. Qed.
imports: Fiat.Common.BoundedLookup Fiat.Narcissus.Common.Specs Fiat.Narcissus.BaseFormats Fiat.Narcissus.Formats.WordOpt Coq.Vectors.Vector Bedrock.Word