Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] How do I handle computational parts of a proof?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How do I handle computational parts of a proof?


Chronological Thread 
  • From: Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] How do I handle computational parts of a proof?
  • Date: Tue, 9 Jul 2019 12:06:15 +0200
  • Organization: LORIA

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.
>
>
>




Archive powered by MHonArc 2.6.18.

Top of Page