The Coq mailing list

[robert <robdockins AT fastmail.fm>]

> Have you read Section 15.5 of CPDT <http://adam.chlipala.net/cpdt/>? I

> haven't read all of the code you included, but the prose makes it sound

> like that section shows how to do what you're looking for.

 

Thanks, Adam. I missed that section when skimming CPDT looking for answers. It seems the trick here is using @? patterns in just the right way and uncurrying lambdas as you encounter them.

 

However, I'm still sort of stuck; trying to apply the technique to my setting gives me odd behavior I don't undersdand. In the final goal below, I expect the match to go into the "app" branch, but instead it goes into the "app no @?" branch. This seems like it might be a bug, because the branch succeeds on my example if I change the pattern to:

 

(plus (@?f x) (@?g x))

 

So maybe it doesn't want to match on partial applications for some reason? Any advice?

 

 

(*******)

 

Ltac do_sk t k :=

idtac "do_sk" t;

lazymatch t with

| (fun (x:?T) => x) =>

idtac "x"; k 1

 

| (fun (x:?T) => (@?f x) (@?g x)) =>

idtac "app" f g; k 2

 

| (fun (x:?T) => ?f ?g) =>

idtac "app, no @?" f g; k 22

 

| (fun (x:?Tx) (y:?Ty) => (@?t' x y) ) =>

idtac "lambda" t'; k 3

 

| (fun (x:?T) => (@?t' x)) =>

idtac "other" t'; k 4

 

| _ => idtac "fallthrough" t

end.

 

Ltac sk t :=

do_sk t ltac:(fun m => idtac m).

 

Definition ten := 10.

Definition asdf (f:nat -> nat) := True.

Definition asdf2 (f:nat -> nat -> nat) := True.

 

Goal (asdf (fun w => w)).

match goal with [ |- asdf ?t ] => sk t end.

(* OK, as expected *)

Abort.

 

Goal (asdf2 (fun w w' => w)).

match goal with [ |- asdf2 ?t ] => sk t end.

(* OK, as expected *)

Abort.

 

Goal (asdf (fun w => plus (plus ten w) ten)).

match goal with [ |- asdf ?t ] => sk t end.

(* Hunh? I expect it to go into the "app" case

but it goes into "app no @?" instead.

*)

Abort.