coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Can Coq help me shorten a proof?, Michiel Helvensteijn, 09/16/2013
- Re: [Coq-Club] Can Coq help me shorten a proof?, t x, 09/16/2013
Archive powered by MHonArc 2.6.18.