The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

Hi,

I tried to tackle your problem using proof by reflection.
This seems to be significantly faster: 
the equivalent of repeat split takes 180s for (truuue 40) ~ 40000 sub-goals 
but bigger problems trigger a stack overflow.


Inductive Tree : Type :=
| Leaf (A:Prop)
| Node (L:Tree) (R:Tree).

Fixpoint iTree (t : Tree) : Prop :=
  match t with
    | Leaf A => A
    | Node L R => (iTree L) /\ (iTree R)
  end.

Fixpoint xflatten (t : Tree) (acc: Prop) : Prop :=
  match t with
    | Leaf A => A -> acc
    | Node L R => xflatten L (xflatten R acc)
  end.

Lemma xflatten_split : forall t (p:Prop), (iTree t -> p) ->  xflatten t p.
Proof.
  induction t.
  simpl. tauto.
  simpl.
  intros.
  apply IHt1.
  intros.
  apply IHt2.
  intros.
  apply H ; tauto.
Qed.

Lemma flatten_split : forall t, xflatten t (iTree t).
Proof.
  intros.
  apply xflatten_split ; auto.
Qed.

Fixpoint truueT (n : nat) : Tree :=
 match n with
   | O => Leaf True
   | S n' => Node (Leaf True)  (truueT n')
 end.

Fixpoint truuueT (n : nat) : Tree :=
 match n with
   | O => Leaf True
   | S n' => Node (truueT 1000) (truuueT n')
 end.

Set Silent.

Goal iTree (truuueT 40).
Time generalize (flatten_split (truuueT 40)); 
  set (f := truuueT 40); 
  generalize (iTree f);
  intros ; compute in H; apply H; clear H.