proposition: Lemma refine_Iterate_Decide_Comp_Pre : forall (Remaining : nat) (P : Fin.t Remaining -> option Prop) (Q : Prop), refine (@Iterate_Decide_Comp_Pre Remaining (fun idx => match P idx with | Some P' => P' | None => True end) Q) (@Iterate_Decide_Comp_opt_Pre Remaining P Q).
proof: Proof. induction Remaining; simpl; intros. - reflexivity. - destruct (P Fin.F1). + f_equiv; unfold pointwise_relation; intros. destruct a; simpl; try reflexivity. setoid_rewrite <- IHRemaining; f_equiv. + rewrite decides_True_Pre; simplify with monad laws; simpl. setoid_rewrite <- IHRemaining; f_equiv. Qed.
imports: Coq.Lists.List Coq.Arith.Compare_dec Coq.Arith.Arith Coq.Bool.Bool Coq.Strings.String Coq.Sets.Ensembles Fiat.Common.BoolFacts Fiat.Common.List.PermutationFacts Fiat.Common.List.ListMorphisms Fiat.Common.IterateBoundedIndex Fiat.Common.List.ListFacts Fiat.Common.LogicFacts Fiat.Common.DecideableEnsembles Fiat.Common.BoundedLookup Fiat.Common.IterateBoundedIndex Fiat.Computation.Core Fiat.Computation.Monad Fiat.Computation.ApplyMonad Fiat.Computation.SetoidMorphisms Fiat.Computation.Refinements.General Fiat.Computation.Refinements.Tactics