The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

I reckon [easy] do a [repeat do_intro] before doing a [do_atom] on any path in
the control flow. Hence, x <= y is transformed into H: x ?=y = Gt |- False
which cannot be solved by [easy].


changing the line do_ccl with
[with do_ccl := trivial with eq_true; do_atom; repeat do_intro; do_atom in ] 
...
solves this particular bug. (Notice the extra do_atom with respect to the
original easy script).

With best regards,
thomas



On Mon, Jan 23, 2012 at 10:17 AM, Pierre Boutillier
<pierre.boutillier AT inria.fr>
 wrote:
> Hi list,
>
> I am currently going though the "trunk" bugs of Coq in order to tag the one
> that need to be fix before v8.4 release commenting dozens of:
> "This bug should be fixed before v8.4 release."
>
> I'm sorry  but coqdevs won't be able to handle them in a reasonable amount
> of time. My hope in order not to fall in depression is that for some of them
> advanced users among you could maybe help us. For example, on the following
> example: http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2630
>
> The easy tactic is written in ltac. In its code
> http://coq.inria.fr/distrib/V8.4beta/stdlib/Coq.Init.Tactics.html, you can
> see a "reflexivity". Anyway, it does not work in the
>
> Require Import QArith.
>
> Lemma kaas (x:Q) : Qle x x.
>   unfold Qle.
>   (* fails: easy. *)
>   (* works: *) reflexivity.
> Qed.
>
> example. Can an Ltac expert can see why ?
>
> Thanks in advance if you accept to spare time on that and help is really,
> really, really, enjoyed in any example of
> http://www.lix.polytechnique.fr/coq/bugs/report.cgi?x_axis_field=version&y_axis_field=component&z_axis_field=&query_format=report-table&short_desc_type=allwordssubstr&short_desc=&long_desc_type=allwordssubstr&long_desc=&bug_file_loc_type=allwordssubstr&bug_file_loc=&deadlinefrom=&deadlineto=&bug_status=UNCONFIRMED&bug_status=NEW&bug_status=ASSIGNED&bug_status=REOPENED&emailassigned_to1=1&emailtype1=substring&email1=&emailassigned_to2=1&emailreporter2=1&emailcc2=1&emailtype2=substring&email2=&bugidtype=include&bug_id=&chfieldfrom=&chfieldto=Now&chfieldvalue=&format=table&action=wrap&field0-0-0=noop&type0-0-0=noop&value0-0-0=
>
> (btw it is the exact moment to make fun of us and say that the solution is
> "info" :-) but please troll kindly)
>
> All the best
> Pierre Boutillier