Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Can Coq help me shorten a proof?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Can Coq help me shorten a proof?


Chronological Thread 
  • From: Michiel Helvensteijn <mhelvens AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Can Coq help me shorten a proof?
  • Date: Mon, 16 Sep 2013 01:23:39 +0200

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



Archive powered by MHonArc 2.6.18.

Top of Page