The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi,
as explained by Michael, automatic solvers always try "cheap" tactics (i.e.
that do not create several subgoals) before trying a case analysis. It
would look more like:

destruct a; auto; destruct b; auto; ....

than

destruct a; destruct b ;... ; auto.

(replace auto by anything that would cheaply discharge some intermediate
subgoals).

Below is an example of automation of this on the same example as Michael.
It is a less sophisticated solution than Michael's. In this example each
case analysis leads to two subgoals one of which is discharged by auto.
That leads to ~ 14 subgoals instead of ~16000.

Of course if it is not possible to discharge intermediate subgoals then you
a re stuck with your 16000 case analysis (and coq's performance is probably
bad compared to auto provers). Sometimes the order in which you chose
variables to analyse may be very important and auto provers have very smart
and secret heuristics to avoid this kid of pathological cases.

Require Import List.
Notation "x + y" := (andb x y) (at level 50, left associativity) :
bool_scope.
Notation "x * y" := (orb x y) (at level 40, left associativity) :
bool_scope.
Open Scope bool_scope.

(* take a list of boolean variables and performs destruct on each of them,
but applies auto to each subgoal between each destruct. *)
Ltac case_bool  l :=
   match l with
   | nil => idtac
   | ?x::?l' => destruct x;auto; case_bool l'
   end.

Lemma foo: forall a b c d e f g h i j k l m n x y:bool,
     a*b*c*d*e*f*g*h*i*j*k*l*m*n + x + x*y = a*b*c*d*e*f*g*h*i*j*k*l*m*n + x.
   intros.
   (* to help auto to solve cases *)
   assert (x + x * y = x). {
     destruct x;destruct y;auto.
   }

   time case_bool (a::b::c::d::e::f::g::h::i::j::k::l::m::n::x::y::nil).





Which you can automate like this:



Le mer. 9 mai 2018 à 16:03, Soegtrop, Michael 
<michael.soegtrop AT intel.com>
a écrit :

> Dear Wilayat,



> below please find a complete proof script which works. It takes 30
milliseconds (on my rather old machine).



> You can repelace the solution also with



> repeat DestructMatchArg.

> all: reflexivity.



> The first repeat results in 29 trivial goals, not 65536 as with a brute
force destruct.



> To see how it works, it is instructive to call DestructmatchArg and
reflexivity manually step by step.



> Of cause you can also add DestructmatchArg as extern hint to auto, as
well as the unfolding, so that just auto does the trick.



> Hope it helps J



> Best regards,



> Michael





> (* DestructMatchArg Example *)



> Inductive  bool: Type:= true | false.

> Definition and (x y: bool) : bool :=

>    match x, y with

>    | true, true => true

>    | _, _ => false

>    end.



> Definition or (x y: bool) : bool :=

>    match x, y with

>    | false, false => false

>    | _, _ => true

>    end.



> Notation "x + y" := (and x y) (at level 50, left associativity) :
bool_scope.

> Notation "x * y" := (or x y) (at level 40, left associativity) :
bool_scope.



> Open Scope bool_scope.



> (* In nested matches, get the argument of the inner most match *)



> Local Ltac GetInnerMatch term :=

>    match term with

>    | context [match ?inner with _ => _ end] => GetInnerMatch inner

>    | _ => term

>    end.



> (**  Destruct the argument of a match in the goal or hypothesis *)



> Ltac DestructMatchArg :=

>    match goal with

>    | |- context [match ?term with _ => _ end] =>

>      let EQ:=fresh "EQ_DestructMatchArg" in

>      let inner:=GetInnerMatch term in

>      destruct inner eqn:EQ

>    | H: context [match ?term with _ => _ end] |- _ =>

>      let EQ:=fresh "EQ_DestructMatchArgInHyp" in

>      let inner:=GetInnerMatch term in

>      destruct inner eqn:EQ

>    end.





> Theorem equal: forall a b c d e f g h i j k l m n x y:bool,

>     a*b*c*d*e*f*g*h*i*j*k*l*m*n + x + x*y = a*b*c*d*e*f*g*h*i*j*k*l*m*n +
x.

> Proof.

>    intros; unfold or; unfold and.

>    time repeat (

>      try reflexivity;

>      try DestructMatchArg

>    ).

> Qed.

> Intel Deutschland GmbH
> Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
> Tel: +49 89 99 8853-0, www.intel.de
> Managing Directors: Christin Eisenschmid, Christian Lamprechter
> Chairperson of the Supervisory Board: Nicole Lau
> Registered Office: Munich
> Commercial Register: Amtsgericht Muenchen HRB 186928