The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Wed, 18 Jul 2012 22:17:22 +0200,
Laurent Théry 
<Laurent.Thery AT inria.fr>
 a écrit :

> On 07/18/2012 09:48 PM, Adam Chlipala wrote:
> > Fixpoint truue (n : nat) : Prop :=
> >   match n with
> >     | O => True
> >     | S n' => True /\ truue n'
> >   end.
> >
> > Fixpoint truuue (n : nat) : Prop :=
> >   match n with
> >     | O => True
> >     | S n' => truue 1000 /\ truuue n'
> >   end.
> >
> > Goal truuue 100.
> >   compute.
> >   Time split. (* 5 secs *) 
> Maybe this is not exactly what you want but ou could try to reduce
> the height of the formula with ad-hoc inductive conjunction.
> If you go to the extreme this gives:
> 
> Inductive and100
> (
> A00 A01 A02 A03 A04 A05 A06 A07 A08 A09
> A10 A11 A12 A13 A14 A15 A16 A17 A18 A19
> A20 A21 A22 A23 A24 A25 A26 A27 A28 A29
> A30 A31 A32 A33 A34 A35 A36 A37 A38 A39
> A40 A41 A42 A43 A44 A45 A46 A47 A48 A49
> A50 A51 A52 A53 A54 A55 A56 A57 A58 A59
> A60 A61 A62 A63 A64 A65 A66 A67 A68 A69
> A70 A71 A72 A73 A74 A75 A76 A77 A78 A79
> A80 A81 A82 A83 A84 A85 A86 A87 A88 A89
> A90 A91 A92 A93 A94 A95 A96 A97 A98 A99 : Prop) : Prop
>   := conj100 :
> A00 -> A01 -> A02 -> A03 -> A04 -> A05 -> A06 -> A07 -> A08 -> A09 ->
> A10 -> A11 -> A12 -> A13 -> A14 -> A15 -> A16 -> A17 -> A18 -> A19 ->
> A20 -> A21 -> A22 -> A23 -> A24 -> A25 -> A26 -> A27 -> A28 -> A29 ->
> A30 -> A31 -> A32 -> A33 -> A34 -> A35 -> A36 -> A37 -> A38 -> A39 ->
> A40 -> A41 -> A42 -> A43 -> A44 -> A45 -> A46 -> A47 -> A48 -> A49 ->
> A50 -> A51 -> A52 -> A53 -> A54 -> A55 -> A56 -> A57 -> A58 -> A59 ->
> A60 -> A61 -> A62 -> A63 -> A64 -> A65 -> A66 -> A67 -> A68 -> A69 ->
> A70 -> A71 -> A72 -> A73 -> A74 -> A75 -> A76 -> A77 -> A78 -> A79 ->
> A80 -> A81 -> A82 -> A83 -> A84 -> A85 -> A86 -> A87 -> A88 -> A89 ->
> A90 -> A91 -> A92 -> A93 -> A94 -> A95 -> A96 -> A97 -> A98 -> A99  ->
> and100
> A00 A01 A02 A03 A04 A05 A06 A07 A08 A09
> A10 A11 A12 A13 A14 A15 A16 A17 A18 A19
> A20 A21 A22 A23 A24 A25 A26 A27 A28 A29
> A30 A31 A32 A33 A34 A35 A36 A37 A38 A39
> A40 A41 A42 A43 A44 A45 A46 A47 A48 A49
> A50 A51 A52 A53 A54 A55 A56 A57 A58 A59
> A60 A61 A62 A63 A64 A65 A66 A67 A68 A69
> A70 A71 A72 A73 A74 A75 A76 A77 A78 A79
> A80 A81 A82 A83 A84 A85 A86 A87 A88 A89
> A90 A91 A92 A93 A94 A95 A96 A97 A98 A99.
> 
> Goal and100
>    True True True True True True True True True True
>    True True True True True True True True True True
>    True True True True True True True True True True
>    True True True True True True True True True True
>    True True True True True True True True True True
>    True True True True True True True True True True
>    True True True True True True True True True True
>    True True True True True True True True True True
>    True True True True True True True True True True
>    True True True True True True True True True True.
> constructor; auto.
> Qed.
> 
> 

I had a similar suggestion with tree balancing.
Maybe that putting propositions in a binary tree that you try to keep
balanced while constructing it could help…

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

Fixpoint truuue (n : nat) : Prop :=
   match n with
     | O => True
     | S n' => truue 63 /\ truuue n'
   end.

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

Goal truuue 64. (* should be a conjunction of 64*63+1 Trues *)
  compute.
  Time repeat split.
Qed.

Goal True /\ (bruue 12) (* a 2^12+1 Trues conjunction *).
  compute.
  Time repeat split.
Qed.

It seems I get a factor 4 with it here…