The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2014-06-16 10:09 GMT+02:00 Vladimir Voevodsky <vladimir AT ias.edu>:

This sounds usefu but I did not understand how to use it in practice.

Suppose my proof is

....

refine ( constr _ _ ).

{ apply a1. exact b1. }

{ apply a2. exact b2. }

Defined.

How do I "abstract" the first argument of constr?

V.

The annoying part of abstract, is that for now (I hope it will change someday…) you have to give one-liners for tactics.
Thus in your example (assuming that the second component does not depend on the first, i.e. constr:A→B→C and not constr:∀a, T a →C), that would be written:

refine (constr _ _).
abstract (apply a1; (*and sadly not dot!*) exact b1).
abstract (apply a2; (*and sadly not dot!*) exact b2).
Defined.

Of course, if the second argument depends on the first, you do not want to use the abstract tactic for the first argument, as it will make it opaque.

I sometimes use this feature to do stuff like:

Definition div_aux (n : nat) : ∀ m, {p : nat * nat | m = (S n) * (fst p) + n - (snd p) ∧ (snd p)≤n }.
refine (
  fix div_aux m :=
  match m as m return {p : nat * nat | m = (S n) * (fst p) + (n - (snd p)) ∧ (snd p)≤n } with
  | O => exists _ (O, n) _(*O=(S n)*O+(n-n)∧O≤n*)
  | S m =>
    match div_aux m with
    | exists p Hp =>
      match snd p as sp return m = (S n) * (fst p) + (n - sp) ∧ sp≤n → _ with
      | O => fun Hp => exists _ (S (fst p), n) _ (*m = (S n) * (fst p) + (n - O) ∧ O≤n → S m = (S n) * (S (fst p)) + (n - n) ∧ n≤n*)
      | S x => fun Hp => exists _ (fst p, x) _ (*m = (S n) * (fst p) + (n - (S x)) ∧ (S x)≤n → S m = (S n) * (S (fst p)) + (n - x) ∧ x≤n*)
    end Hp
  end
).
Proof (*O=(S n)*O+(n-n)∧O≤n*).
 clear.
 abstract (…).
Proof (*m = (S n) * (fst p) + (n - O) ∧ O≤n → S m = (S n) * (S (fst p)) + (n - n) ∧ n≤n*).
 clear - Hp.
 abstract (…).
Proof (*m = (S n) * (fst p) + (n - (S x)) ∧ (S x)≤n → S m = (S n) * (S (fst p)) + (n - x) ∧ x≤n*).
 clear - Hp.
 abstract (…).
Defined.

This makes the computational part readable. A new feature (I did not test, as I have not installed trunk) allows to put proof scripts directly in the term,
this should remove use of "refine", and with combination of powerful tactics (like Adam Chipala 'crush' tactic) could reduce the definition to:

Definition div_aux (n : nat) : ∀ m, {p : nat * nat | m = (S n) * (fst p) + n - (snd p) ∧ (snd p)≤n } :=
  fix div_aux m :=
  match m as m return {p : nat * nat | m = (S n) * (fst p) + (n - (snd p)) ∧ (snd p)≤n } with
  | O => exists _ (O, n) $(clear; abstract pow_tac)$
  | S m =>
    match div_aux m with
    | exists p Hp =>
      match snd p as sp return m = (S n) * (fst p) + (n - sp) ∧ sp≤n → _ with
      | O => fun Hp => exists _ (S (fst p), n) $(clear - Hp; abstract pow_tac)$
      | S x => fun Hp => exists _ (fst p, x) $(clear - Hp; abstract pow_tac)$
    end Hp
  end.
 
Note that "clear …" is used before abstract. This is due to the fact that abstract is not clever enough to generalize only required hypothesis.
In particular, in presence of a fixpoint, the fixpoint is generalized without being passed a smaller argument, and thus breaks guard condition.

On Jun 15, 2014, at 11:00 PM, AUGER Cédric <sedrikov AT gmail.com> wrote:

> Le Sun, 15 Jun 2014 20:01:10 +0000,
> Erik Palmgren <palmgren AT math.su.se> a écrit :
>
>>
>> Many thanks to Matthieu, Bas and Vladimir, for the hints how to
>> improve proof performance. The suggested separation of data and
>> proofs (for setoids and categories) seems to have speeded up the
>> first part of the proof, but slowed down the final part, probably
>> since further levels of records/existentials were introduced.  In
>> total a slightly worse runtime: from 34 min 40 sec to 34 min 50 sec
>> on the Mac Book Air I am using. I guess the main problem is what
>> Matthieu describes below. In general I would like to end all proofs
>> with "Defined", since I may need the constructions of the proofs
>> later.
>
> The "abstract" tactic can be quite helpful for this kind of things.
>
> For instance, you can do something like:
>
> Definition foo : bar.
> Proof.
> <regular tactics for parts you want transparent>
> abstract (<opaque proof part>).
> Defined.
>
> This is especially useful in combination with the refine tactic.
>
> Definition foo : {x : bar | P x}.
> refine (existT P (f x) _).
> abstract (my_tactic).
> Defined.
>
>
>>
>> Best regards
>>
>> Erik
>>
>> ________________________________
>> Från: matthieu.sozeau AT gmail.com [matthieu.sozeau AT gmail.com] för
>> Matthieu Sozeau [matthieu.sozeau AT inria.fr] Skickat: den 15 juni 2014
>> 12:12 Till: coq-club AT inria.fr
>> Ämne: [Coq-Club] Slow iterated sigmas
>>
>> Hi Erik,
>>
>>  Apart from Vladimir's answer about separating "data" and proofs,
>> there is a known problem of representation when using projections of
>> sigma types and parametrized records that you might be experiencing.
>> Each projection takes all the parameters as arguments, and in
>> nested/iterated cases this can lead to a blowup in proof-term size
>> and type checking time. You can check that this happens using Set
>> Printing All, the actual proof term should be much much larger than
>> what you see if implicit arguments are hidden. The next version (and
>> current trunk) will have support for a more economical representation
>> that solves that problem. -- Matthieu
>>
>> On Saturday, June 14, 2014, Erik Palmgren
>> <palmgren AT math.su.se<UrlBlockedError.aspx>> wrote:
>>
>> Here is a remark I made some time ago. I am getting, what I think,
>> absurdly slow response from Coq when checking proofs involving many
>> iterated sigmas or records. There was some improvement when upgrading
>> from 8.3 to 8.4, and rearranging some sigma-constructions, but it is
>> still too hard for the quite modest complexity I am considering.
>>
>> I am using an alternative development of setoids, since I want to
>> the truth-values of equality to be in Set rather than in the
>> Coq-standard Prop. The goal of the development is to construct a
>> category of setoids closed under the various categorical
>> constructions as pullbacks, pushouts and internal products etc. I see
>> no principal difficulties in this, but the implementation in Coq has
>> turned to be quite frustrating, because of the slowness of checking
>> proofs. So far just proving closure for pullbacks, has required
>> machine times of up to an hour.
>>
>> Does anyone have an idea for how to improve performance?
>>
>> The URL
>>
>> http://people.su.se/~epalm/coq/czf_and_setoids/
>>
>> contains
>> CategoricalUniverse-test12.v<http://people.su.se/~epalm/coq/czf_and_setoids/CategoricalUniverse-test12.v>
>> which is the actual development (it may require recompilation).
>>
>> Best regards
>>
>> Erik Palmgren
>>
>>
>>
>> --
>>
>

--
.../Sedrikov\...