coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
>
>
>
- [Coq-Club] How do I handle computational parts of a proof?, Agnishom Chattopadhyay, 07/08/2019
- Re: [Coq-Club] How do I handle computational parts of a proof?, Dominique Larchey-Wendling, 07/08/2019
- Re: [Coq-Club] How do I handle computational parts of a proof?, Laurent Thery, 07/08/2019
- Re: [Coq-Club] How do I handle computational parts of a proof?, Dominique Larchey-Wendling, 07/08/2019
- Re: [Coq-Club] How do I handle computational parts of a proof?, Laurent Thery, 07/09/2019
- Re: [Coq-Club] How do I handle computational parts of a proof?, Dominique Larchey-Wendling, 07/09/2019
- Re: [Coq-Club] How do I handle computational parts of a proof?, Laurent Thery, 07/09/2019
- Re: [Coq-Club] How do I handle computational parts of a proof?, Dominique Larchey-Wendling, 07/08/2019
- Re: [Coq-Club] How do I handle computational parts of a proof?, Laurent Thery, 07/08/2019
- Re: [Coq-Club] How do I handle computational parts of a proof?, Emilio Jesús Gallego Arias, 07/09/2019
- Re: [Coq-Club] How do I handle computational parts of a proof?, Laurent Thery, 07/09/2019
- Re: [Coq-Club] How do I handle computational parts of a proof?, Dominique Larchey-Wendling, 07/08/2019
Archive powered by MHonArc 2.6.18.