proposition: Lemma nth_error_GetAttributeRaw: forall {N} (tup: @RawTuple (MakeWordHeading N)) (idx: Fin.t N), let n := (projT1 (Fin.to_nat idx)) in BinNat.N.lt (BinNat.N.of_nat n) (Word.Npow2 32) -> let k1 := Word.natToWord 32 n in nth_error (TupleToListW tup) (Word.wordToNat k1) = @Some W match MakeWordHeading_allWords idx with | eq_refl => (GetAttributeRaw tup idx) end.
proof: Proof. induction idx; simpl in *. - reflexivity. - destruct (Fin.to_nat idx). unfold TupleToListW in *; simpl in *; apply lt_BinNat_lt in l. intros. rewrite Word.wordToNat_natToWord_idempotent in * by auto using BinNat_lt_of_nat_S. simpl; rewrite IHidx by auto using BinNat_lt_of_nat_S; reflexivity. Qed.
imports: CertifiedExtraction.Extraction.QueryStructures.Basics CertifiedExtraction.Extraction.QueryStructures.BinNatUtils CertifiedExtraction.Extraction.QueryStructures.TupleToListW CertifiedExtraction.Extraction.QueryStructures.EnsemblesOfTuplesAndListW Fiat.QueryStructure.Specification.Representation.Tuple Bedrock.Memory Coq.Lists.List CertifiedExtraction.Utils