The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Hi Laurent,

I am not advocating against "proof by reflexion" ;-)
But it has a limitation: it only works for decidable
predicates.

The other one can reduce to a finitary number
of goals for any predicate over nat.

The reason it is slow compared to "reflexion" is
because it uses the proof-search engine instead
of the normalization engine.

Best,

D.

Ltac reduce_conj :=
  exact I || (apply conj; [ | reduce_conj ]).

Tactic Notation "bounded" "forall" :=
  apply bounded_forall_spec; reduce_conj.

Lemma can_be_brute_forced (P : nat -> Prop) : forall (n : nat), n < 20
-> P n.
Proof.
  bounded forall.
  (* Whatever ... *)
Qed.


> On 7/8/19 11:03 PM, Dominique Larchey-Wendling wrote:
>> I do not think Boolean's are really required here ...
>> just a variation around your proposal though 
> 
> Nice,
> 
> using bool just proves the goal with a single computation, so the proof
> term is  smaller. For example,
> 
> Lemma stupid_brute_forced : forall (n : nat), n < 1000 -> n = n.
> Proof.
>   now apply bounded_forall_spec.
> Qed.
> 
> takes ages to check
> 
> Lemma stupid_brute_forced : forall (n : nat), n < 1000 -> n = n.
> Proof.
>   now apply icheck_correct.
> Qed.
> 
> is instantaneous.
> 
> 
>