proposition: Lemma forall_enumerable_by_beq_aggregate_correct (H_f_good : forall y, f x = f y -> P y -> P x) : forall_enumerable_by_beq_aggregate = if P x then g (f x) else base.
proof: Proof. rewrite forall_enumerable_by_beq_aggregate'_eq by assumption. rewrite <- (forall_enumerable_by_beq_correct P x (fun y => g (f y)) base). unfold forall_enumerable_by_beq_aggregate', forall_enumerable_by_beq. change eq_R_enum with beq. progress change (@beq _ (@beq _ eq_R_enum)) with (@beq _ eq_R_enum). rewrite fold_right_uniquize. rewrite !fold_right_beq_in_correct'. repeat match goal with | [ |- ?x = ?x ] => reflexivity | _ => discriminate | [ |- context[list_bin ?beq ?x ?y] ] => destruct (list_bin beq x y) eqn:? | [ H : list_bin _ _ _ = true |- _ ] => apply (list_in_bl bl) in H | [ H : List.In _ (List.map _ _) |- _ ] => apply List.in_map_iff in H | [ |- List.In _ (List.map _ _) ] => apply List.in_map_iff | _ => progress subst | _ => progress destruct_head ex | _ => progress destruct_head sig | _ => progress destruct_head and | _ => progress simpl in * | [ H : list_bin ?beq ?x ?y = false |- _ ] => exfalso; rewrite (list_in_lb lb) in H; [ | clear H ] | [ |- _ /\ _ ] => split | [ |- @ex (sig _) _ ] => eexists (exist _ _ _) | [ |- ex _ ] => eexists | [ |- _ = ?x ] => is_var x; reflexivity | [ |- ?f _ = ?f ?x ] => is_var x; reflexivity | [ |- List.In _ (enumerate _) ] => apply enumerate_correct end. Unshelve. simpl; eapply H_f_good; first [ eassumption | symmetry; eassumption ]. eassumption. Qed.
imports: Fiat.Common Fiat.Common.List.Operations Fiat.Common.List.ListFacts Fiat.Common.Enumerable Fiat.Common.Enumerable.ReflectiveForall Fiat.Common.Equality