The Coq mailing list

[t x <txrev319 AT gmail.com>]

(2) + (3) can be fairly easily solved via

repeat(find_false || simpl in * || break_stuff || do_associativity)

where find_false is a tactic that kills branches, and do_associativity is whatever you want to do with associativity, and break_stuff just breaks hypothesis / goals into smaller terms.

As for (1), you're unlikely to do better than pure brute force. Given Ltac's choice + backtracking support, one can view Ltac as a non-deterministic machine.

The query you want, "shortest proof" is like Sigma_2 P in complexity -- you want to say:

exists (proof P), forall (proof Q): valid (Q) -> length(Q) >= length(P)

NTMs are not known to be able to solve such queries efficiently.

On Sun, Sep 15, 2013 at 11:23 PM, Michiel Helvensteijn <mhelvens AT gmail.com> wrote:

Hi all!

I have a simple finite type with a precisely defined binary operation.
I want to prove a property about the operator. This is easy with Coq,
because I can just try all possible variable assignments. The
resulting proof is simple, but huge.


Require Export Coq.Unicode.Utf8.

Inductive Term :=
  | err: Term
  | add: Term
  | rep: Term
  | rem: Term
  | frb: Term.

Definition comp (x y: Term) :=
  match x, y with
  |  add, rem  =>  rep
  |  add, frb  =>  add
  |  rep, add  =>  add
  |  rep, rep  =>  rep
  |  rem, add  =>  frb
  |  rem, rep  =>  rem
  |  frb, rem  =>  rem
  |  frb, frb  =>  frb
  |  _  , _    =>  err
  end.

Infix "·" := comp (at level 40).

Lemma CCR: ∀ x y z,  z·y·x = z·x·y  →  z·x ≠ err  →  z·y ≠ err
                     →  ∀ d, z·d·y·x = z·d·x·y.
  intros x y z H E₁ E₂; case x, y, z;
    auto;
    (contradict E₁; auto);
    (contradict E₂; auto).
Qed.


But I would like to find the shortest possible proof, to write down
for human consumption. This involves (1) finding the best order in
which to eliminate the variables, (2) cutting off branches of the
proof as early as possible, (3) automatically taking associativity
into account (which is also provable), ... that sort of thing.

Are there existing tools / plugins / libraries to help me with this?

--
www.mhelvens.net