Helper

step_iota_enum

File dumas2017dual/dsdp/dsdp_pismc.v

Section interp_sound_section

Type Lemma

Proof Lines 1

Signature

Lemma step_iota_enum n (ps : seq (proc data)) : [seq smc_interpreter.step ps nil i | i <- iota 0 n] = [seq smc_interpreter.step ps nil (val i) | i <- enum 'I_n].

Description

step_sound gives rsteps using tuples; we need to connect that to the seq-level interp1 which uses iota. These two lemmas bridge the iota/enum gap.

Uses (0)

This lemma does not use any other lemmas from the stats.

Used By (0)

No lemmas in the stats use this lemma.

Coq Source Code

View on GitHub

Loading source code...

← Back to Stats