proposition: Theorem SumType_decode_correct' {m} {P} (types : Vector.t Type m) (formatrs : ilist (B := fun T => T -> CacheFormat -> Comp (B * CacheFormat)) types) (decoders : ilist (B := fun T => B -> CacheDecode -> option (T * B * CacheDecode)) types) (invariants : forall idx, Vector.nth types idx -> Prop) (cache_invariants : forall idx, (CacheDecode -> Prop) -> Prop) (formatrs_decoders_correct : forall idx, cache_inv_Property P (cache_invariants idx) -> CorrectDecoder monoid (fun st => invariants idx st) (fun st => invariants idx st) eq (ith formatrs idx) (ith decoders idx) P (ith formatrs idx)) idx : cache_inv_Property P (fun P => forall idx, cache_invariants idx P) -> CorrectDecoder monoid (fun st => SumType_index types st = idx /\ invariants _ (SumType_proj types st)) (fun st => SumType_index types st = idx /\ invariants _ (SumType_proj types st)) eq (format_SumType types formatrs) (decode_SumType types decoders idx) P (format_SumType types formatrs).
proof: Proof. split; revert types formatrs decoders invariants formatrs_decoders_correct; unfold CorrectDecoder, format_SumType, decode_SumType. { intros; intuition. unfold id in *; eapply (proj1 (formatrs_decoders_correct _ (H _))) in H2; eauto; destruct_ex; intuition. subst; setoid_rewrite H2; simpl. eexists _, _; intuition eauto. repeat f_equal. unfold id; rewrite inj_SumType_proj_inverse; reflexivity. unfold id; rewrite inj_SumType_proj_inverse; eauto. } { intros. destruct (ith decoders idx t env') as [ [ [? ?] ? ] | ] eqn : ? ; simpl in *; try discriminate; injections. eapply (proj2 (formatrs_decoders_correct idx (H _))) in Heqo; eauto; destruct Heqo as [? [? ?] ]; destruct_ex; intuition; subst. eexists _, _; intuition eauto; unfold id in *; eauto; try rewrite index_SumType_inj_inverse; eauto. - unfold id; pattern (SumType_index types (inj_SumType types idx n)), (SumType_proj types (inj_SumType types idx n)). eapply SumType_proj_inj; eauto. - unfold id; pattern (SumType_index types (inj_SumType types idx n)), (SumType_proj types (inj_SumType types idx n)). eapply SumType_proj_inj; eauto. } Qed.
imports: Fiat.Common.ilist Fiat.Common.SumType Fiat.Common.IterateBoundedIndex Fiat.Narcissus.Common.Specs Coq.Sets.Ensembles Bedrock.Word