Library CFML.CFAsymptoticsDemos

Set Implicit Arguments.
Require Import CFLib.

Parameter f : int -> int. Parameter f_spec : exists c, forall x, f x = c * x.
Parameter g : int -> int. Parameter g_spec : exists c, forall x, g x = c * x.
Definition h x := g (f x).

Definition proj1_exists (A:Type) (P:A->Prop) (H: exists x, P x) : A :=
  proj1_sig (indefinite_description H).
Arguments proj1_exists [A] [P].

Definition proj2_exists (A:Type) (P:A->Prop) (H: exists x, P x) : (P (proj1_exists H)) :=
  proj2_sig (indefinite_description H).
Arguments proj2_exists [A P].

Lemma proj1_exists_prop : forall (A:Type) (P:A->Prop) (H: exists x, P x) x,
  x = proj1_exists H -> P x.
Proof using.
  intros. subst. applys proj2_exists.
Qed.

Arguments proj1_exists_prop [A] [P].

Definition hole (A:Type) (x:A) := x.

Lemma h_spec : exists c, forall x, h x = c * x.
Proof using.

Ltac hole_intro T :=
  let c := fresh "c" in evar (c:T); exists (hole c); subst c.

  hole_intro int. intros. unfold h.

Ltac hole_find tt :=
  match goal with |- context [ hole ?x ] => constr:(x) end.


Ltac hole_remove x :=
  replace (hole x) with x; [ | reflexivity ].

Ltac hole_step op v :=
  let T := match type of op with ?T -> ?T -> ?T => constr:(T) end in
  let x := hole_find tt in
  let c := fresh "c" in evar (c:T);
  let H := fresh in
  hole_remove x;
  assert (H: x = op v (hole c)); [ reflexivity | clear H ]; subst c.


Ltac hole_stop neutral :=
  let x := hole_find tt in
  let H := fresh in
  hole_remove x;
  assert (H: x = neutral); [ try reflexivity | clear H ].


Ltac exists_extract E x H :=
  sets x: (proj1_exists E);
  forwards H: proj1_exists_prop x; [reflexivity|];
  simpl in H.



Ltac exists_cleanup E x :=
  change (proj1_exists E) with x;
  clearbody x.

Ltac cst_step E x H :=
  exists_extract E x H;
  hole_step Z.mul x;
  exists_cleanup E x.


  cst_step g_spec cg Hcg. rewrite Hcg.
  cst_step f_spec cf Hcf. rewrite Hcf.
  hole_stop 1.
  ring.

Qed.

Lemma h_spec' : exists c, forall x, h x = c * x.
Proof using.
  evar (c0:int). exists c0.
  intros. unfold h.

  sets cf: (proj1_exists f_spec).
  forwards* Hcf: proj1_exists_prop cf. simpl in Hcf.
  evar (c1:int). assert (c0 = c1 * cf). subst c0. reflexivity.
  rewrite Hcf. clear Hcf.
  sets_eq cf': (proj1_exists f_spec). clear EQcf'. subst cf.

  sets cg: (proj1_exists g_spec).
  forwards* Hcg: proj1_exists_prop cg. simpl in Hcg.
  evar (c2:int). assert (c1 = c2 * cg). subst c1. reflexivity.
  rewrite Hcg. clear Hcg.
  sets_eq cg': (proj1_exists g_spec). clear EQcg'. subst cg.

  assert (c2 = 1). subst c2. reflexivity.

  subst c0. ring.
Qed.