The Coq mailing list

[robert <robdockins AT fastmail.fm>]

Ltac wizards,

 

I've copied below a simplified version of a tactic I've been playing with recently to automatically convert terms into applicative form using SKI combinators. (why? I'm evaluating the hypothesis that proof automation for properties about functions works better when things are in applicative form)

 

The hard part here is opening up lambda-terms to work on their bodies. I've found a trick that lets me do pretty much what I want, but it has the side-effect of generating useless and potentially large proof structure. I've found this can have a noticable effect on Qed time for some examples. I wonder if there is a way to accomplish the same thing without cluttering up the generated proof.

 

Question 1: Is there any way to relably generate a new evar without introducting a local definition in the proof or otherwise having the evar eventaully appear in the proof term? If so, I could improve the "sk2" tactic below so it produces less proof structure; in particular the calculated SKI term would not be copied into the proof.

 

Question 2: Why does tactic sk3 fail? Can it be fixed?

 

Challenge: Is there any way to fix my tactic so it produces no extra proof structure at all?

 

 

Cheers,

Rob

 

 

 

(*** code below, for Coq 8.4 ***)

 

Definition S' A B C (f:A -> B -> C) (g:A -> B) (a:A) : C := (f a) (g a).

Definition I' A (a:A) : A := a.

Definition K' A B (b:B) (a:A) := b.

 

Arguments S' [A B C] f g a.

Arguments K' [A B] b a.

Arguments I' {A} a.

 

Ltac do_sk x y :=

match y with

| ?f ?g =>

let f' := do_sk x f in

let g' := do_sk x g in

constr : (S' f' g')

 

| x =>

let X := type of x in

constr : (@I' X)

 

| _ =>

let X := type of x in

let Y := type of y in

constr : (@K' X Y y)

end.

 

(* this works... but it clutters the context with

an open existential variable

*)

Ltac sk1 t :=

let z := fresh "z" in

match type of t with

| ?A -> ?B =>

evar (z:A);

let t' := eval cbv beta in (t z) in

let m := do_sk z t' in

clear z;

change t with m

end.

 

(* this works without generating open evars,

but produces some useless proof structure...

*)

Ltac sk2 t :=

match type of t with

| ?A -> ?B =>

let output := fresh "output" in

evar (output:A -> B);

 

let H := fresh in

assert (H:A -> A);

[ let a := fresh "a" in

intro a;

let t' := eval cbv beta in (t a) in

let m := do_sk a t' in

let out_evar := eval unfold output in output in

unify m out_evar;

exact a

|

let m := eval unfold output in output in

clear H output;

change t with m

]

end.

 

(* this doesn't work, I don't really know why...

*)

Ltac sk3 t :=

match eval hnf in t with

| (fun z => ?t') =>

let m := do_sk z t'

in change t with m

end.

 

 

(* testing... *)

 

Definition ten := 10.

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

 

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

match goal with [ |- asdf ?X ] => sk1 X end.

hnf; trivial.

(* can't QED, open evar *)

Abort.

 

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

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

hnf. trivial.

Qed.

Print Unnamed_thm. (* extra junk...*)

 

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

(* This fails altogether. Any way to fix it? *)

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