ltac2app.v

Require Import Coq.Init.Prelude.

Fixpoint fnd (n : nat) : Prop :=
  match n with
  | O => True
  | S n => True /\ fnd n
  end.

Fixpoint big_and (xs : list Prop) : Prop :=
  match xs with
  | nil => True
  | cons x xs => and x (big_and xs)
  end.
Fixpoint typeof_big_conj (xs : list Prop) (P : Prop) : Prop :=
  match xs with
  | nil => P
  | cons x xs => x -> typeof_big_conj xs P
  end.
Lemma apply_rconj_and xs (P Q : Prop) : P -> typeof_big_conj xs Q -> typeof_big_conj xs (P /\ Q).
Proof. revert Q; revert P; induction xs; intros; cbn in *; eauto. Qed.
Lemma big_conj xs : typeof_big_conj xs (big_and xs).
Proof. induction xs. exact I. cbn. intros. apply apply_rconj_and; eauto. Qed.

Require Import Coq.Lists.List.

Require Import Ltac2.Ltac2.
Require Import Ltac2.Control.
Require Import Ltac2.Std.
Require Import Ltac2.Notations.

Ltac2 get_constant (c : constr)
  := match Constr.Unsafe.kind c with
     | Constr.Unsafe.Constant c _ => c
     | _ => throw Match_failure
     end.

Ltac2 Notation "eval" "cbv" s(strategy) "in" v(constr) :=
  Std.eval_cbv s v.

Ltac2 fill_with_I (n : int) (h : constr) :=
  let args := Array.make n 'I in
  Constr.Unsafe.make (Constr.Unsafe.App h args).

Ltac2 rec int_of_nat (v : constr) :=
  Message.print (Message.of_constr v);
  match Constr.Unsafe.kind v with
  | Constr.Unsafe.App h args => let v := Array.get args 0 in Int.add 1 (int_of_nat v)
  | _ => 0
  end.

Goal fnd 7000.
  let n := match! goal with [ |- fnd ?n ] => n end in
  let n_int := 7000 (*Control.time (Some "to_int") (fun () => int_of_nat n)*) in
  let ls := constr:(repeat True $n) in
  let ls := Control.time (Some "cbv1") (fun () => (eval cbv in $ls)) in
  let pf := constr:(big_conj $ls) in
  let t := Constr.type pf in
  let t := Control.time (Some "cbv2") (fun () => (eval cbv [typeof_big_conj big_and] in $t)) in
  Control.time (Some "assert") (fun () => (assert (H : $t) by refine pf));
    let h' := Control.time (Some "fill I") (fun () => fill_with_I n_int 'H) in
    Control.time (Some "tc") (fun () => '$h'; ()).