proposition: Lemma well_founded_lift_gtb {leb_Reflexive : Reflexive leb} {leb_Proper : Proper (eqb ==> eqb ==> eq) leb} {eqb_Proper : Proper (eqb ==> eqb ==> eq) eqb} : well_founded (Basics.flip lift_ltb).
proof: Proof. intro a. eapply Acc_subrelation. { eapply function_relationA_of_Acc; [ .. | eexact well_founded_gt | | eapply is_finite_for_keys ]; [ try exact _.. ]; [ repeat match goal with | [ |- is_true (?R ?x ?x) ] => reflexivity | _ => progress unfold gtb, ltb, flip, impl in * | _ => intro | _ => progress subst | _ => assumption | [ H : is_true (eqb ?x ?y) |- _ ] => rewrite H in *; clear x H end.. | | ]. { simpl; unfold gtb, flip, ltb in *. intro x; rewrite top_top; simpl. destruct (eqb x top) eqn:Heqb; [ left | right; reflexivity ]. fold_is_true. rewrite Heqb; reflexivity. } { unfold to_function, find_default. intros ???? H. rewrite !(find_o _ H). trivial. } } { unfold gtb, flip; intros x y _ H. unfold lift_ltb in H. apply andb_true_iff in H. destruct H as [H0 H1]. unfold function_relation. split; [ clear H1 | clear H0 ]. { unfold to_function, lift_leb, find_default, ltb in *. setoid_rewrite lift_brelation_iff in H0. intro k; specialize (H0 k). do 2 edestruct find; repeat match goal with | _ => progress simpl in * | _ => left; congruence | _ => right; reflexivity | [ |- context[eqb ?x ?y] ] => destruct (eqb x y) eqn:? | [ H : context[?x = true] |- _ ] => change (is_true x) in H | [ H : is_true ?x, H' : context[?x] |- _ ] => rewrite H in H' | [ H : is_true ?x |- context[?x] ] => rewrite H | [ H : is_true (eqb ?x ?y) |- _ ] => rewrite H in *; clear x H | [ H : is_true (eqb ?x ?y) |- _ ] => rewrite <- H in *; clear y H | [ H : context[eqb ?x ?x] |- _ ] => replace (eqb x x) with true in H by (symmetry; change (is_true (eqb x x)); reflexivity) end. } { unfold lift_eqb, to_function, find_default in *. apply negb_true_iff in H1. rewrite lift_brelation_iff_false in H1. destruct H1 as [k H1]; exists k. do 2 edestruct find; repeat match goal with | _ => progress simpl in * | _ => progress subst | _ => congruence | _ => intro | [ H : is_true (eqb ?x ?y) |- _ ] => rewrite H in *; clear x H | [ H : is_true (eqb ?x ?y) |- _ ] => rewrite <- H in *; clear y H | [ H : context[eqb ?x ?x] |- _ ] => replace (eqb x x) with true in H by (symmetry; change (is_true (eqb x x)); reflexivity) end. } } Qed.
imports: Coq.FSets.FMapInterface Fiat.Common.Wf Fiat.Common.FMapExtensions Fiat.Common.FMapExtensions.LiftRelationInstances Fiat.Common