proposition: Lemma greatest_fixpoint_fixpoint a : step (greatest_fixpoint a) = greatest_fixpoint a.
proof: Proof. unfold greatest_fixpoint. set (sz := sizeof a). assert (H : sizeof a <= sz) by reflexivity. clearbody sz. revert dependent a. induction sz as [|sz IHsz]. { simpl. intros a Hle. assert (sizeof (step a) <= 0) by (etransitivity; [ apply step_monotonic | apply Hle ]). apply step_eq; omega. } { simpl. intros. repeat match goal with | [ |- context[if ?e then _ else _] ] => destruct e eqn:? | [ H : leb _ _ = true |- _ ] => apply leb_iff in H | [ H : leb _ _ = false |- _ ] => apply leb_iff_conv in H | _ => solve [ eauto with nocore ] | [ |- step _ = _ ] => apply step_eq | _ => omega | [ H : forall a, _ -> _ = _ |- _ ] => rewrite H by omega | [ H : _ < _ |- _ ] => hnf in H | [ H : S _ <= S _ |- _ ] => apply Nat.succ_le_mono in H | [ H : sizeof ?x <= ?y, H' : ?y <= sizeof (step ?x) |- _ ] => let H'' := fresh in assert (H'' : sizeof (step x) <= sizeof x) by apply step_monotonic; assert (sizeof x = y) by omega; assert (y = sizeof (step x)) by omega; clear H H' H'' | [ H : sizeof ?x <= sizeof (step ?x) |- _ ] => let H'' := fresh in assert (H'' : sizeof (step x) <= sizeof x) by apply step_monotonic; assert (sizeof x = sizeof (step x)) by omega; clear H H'' end. } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Arith.EqNat Coq.Arith.Compare_dec Coq.ZArith.ZArith Coq.Lists.List Fiat.Common.List.ListFacts Fiat.Common