proposition: Lemma refine_Iterate_Decide_Comp_equiv : forall (Remaining : nat) (P P' : Ensemble (Fin.t Remaining)), (forall idx, P idx -> P' idx) -> (forall idx, ~ P idx -> ~ P' idx) -> refine (@Iterate_Decide_Comp Remaining P') (@Iterate_Decide_Comp Remaining P).
proof: Proof. induction Remaining; simpl; intros. - reflexivity. - f_equiv. + unfold refine; intros; computes_to_inv; subst; computes_to_econstructor; destruct v; simpl in *; eauto. + unfold pointwise_relation; intros b; destruct b; simpl; eauto. reflexivity. 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