The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

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