example with open terms: extensional replace

README.md

@@ -140,6 +140,9 @@ and `ocaml-lsp-server` (version 1.15).
 - [reduction surgery](examples/example_reduction_surgery.v) implements
   a tactic fine tuning cbv with a list of allowed unfoldings taken from a
   module.
+- [open terms](examples/example_open_terms.v) implements
+  a tactic like `replace` that receives terms containing free variables, i.e.
+  variables bound in the goal but not in the proof context.
 
 ### Applications written in Coq-Elpi
 
@@ -395,13 +398,14 @@ Tactics also accept Ltac variables as follows:
 - `ltac_string:(v)` (for `v` of type `string` or `ident`)
 - `ltac_int:(v)` (for `v` of type `int` or `integer`)
 - `ltac_term:(v)` (for `v` of type `constr` or `open_constr` or `uconstr` or `hyp`)
-- `ltac_(string|int|term)_list:(v)` (for `v` of type `list` of ...)
+- `ltac_open_term:(v)` (for `v` of type `uconstr`)
+- `ltac_(string|int|term|open_term)_list:(v)` (for `v` of type `list` of ...)
 - `ltac_tactic:(t)` (for `t` of type `tactic_expr`)
 - `ltac_attributes:(v)` (for `v` of type `attributes`)
 For example:
 ```coq
-Tactic Notation "tac" string(X) ident(Y) int(Z) hyp(T) constr_list(L) simple_intropattern_list(P) :=
-  elpi tac ltac_string:(X) ltac_string:(Y) ltac_int:(Z) ltac_term:(T) ltac_term_list:(L) ltac_tactic:(intros P).
+Tactic Notation "tac" string(X) ident(Y) int(Z) hyp(T) constr_list(L) simple_intropattern_list(P) uconstr(U) :=
+  elpi tac ltac_string:(X) ltac_string:(Y) ltac_int:(Z) ltac_term:(T) ltac_term_list:(L) ltac_tactic:(intros P) ltac_open_term:(U).
 ```
 lets one write `tac "a" b 3 H t1 t2 t3 [|m]` in any Ltac context.
 Arguments are first interpreted by Ltac according to the types declared
@@ -413,8 +417,12 @@ unresolved implicit arguments, since this is what the `constr` Ltac type means
 If they were typed as `open_constr` or `uconstr`, the last or both checks would
 be respectively skipped. In any case they are passed to the Elpi code as `trm ...`.
 Both `"a"` and `b` are passed to Elpi as `str ...`.
+Argument `U` flagged as `ltac_open_constr` can mention free variables. The Elpi
+tactic receives `open-trm N F` where `N` is the number of free variables in `U`
+and `F` is `fun x1 => ... fun xN => U`.
 Finally, `ltac_term:(T)` and `(T)` are *not* synonyms: but the former must be used
 when defining tactic notations, the latter when invoking elpi tactics directly.
+``` `(T)``` can be used to pass an open term to `elpi tactic ...`.
 
 ##### Attributes
 

builtin-doc/coq-builtin-synterp.elpi

@@ -74,6 +74,7 @@ kind argument type.
 type int       int    -> argument. % Eg. 1 -2.
 type str       string -> argument. % Eg. x "y" z.w. or any Coq keyword/symbol
 type trm       term   -> argument. % Eg. (t).
+type open-trm  int -> term -> argument.
 
 % Extra arguments for commands. [Definition], [Axiom], [Record] and [Context]
 % take precedence over the [str] argument above (when not "quoted").

builtin-doc/coq-builtin.elpi

@@ -47,6 +47,7 @@ kind argument type.
 type int       int    -> argument. % Eg. 1 -2.
 type str       string -> argument. % Eg. x "y" z.w. or any Coq keyword/symbol
 type trm       term   -> argument. % Eg. (t).
+type open-trm  int -> term -> argument.
 
 % Extra arguments for commands. [Definition], [Axiom], [Record] and [Context]
 % take precedence over the [str] argument above (when not "quoted").

elpi/coq-arg-HOAS.elpi

@@ -32,6 +32,7 @@ kind argument type.
 type int       int    -> argument. % Eg. 1 -2.
 type str       string -> argument. % Eg. x "y" z.w. or any Coq keyword/symbol
 type trm       term   -> argument. % Eg. (t).
+type open-trm  int -> term -> argument.
 
 % Extra arguments for commands. [Definition], [Axiom], [Record] and [Context]
 % take precedence over the [str] argument above (when not "quoted").

examples/example_open_terms.v

@@ -0,0 +1,207 @@
+From elpi Require Import elpi.
+Require Import Arith ZArith List FunctionalExtensionality.
+
+Axiom map2 : (nat -> nat -> nat) -> list nat -> list nat -> list nat.
+
+(* This example make use of the open-trm argument type in order to
+   implement a tactic that takes in input expressions mentioning
+   variables that are bound in the goal (and not in the proof context) *)
+
+Lemma easy_example : forall x, x + 1 = 1 + x.
+Proof.
+  intros x.
+  (* easy: x is bound by the proof context *)
+  replace (x + 1) with (1 + x) by ring.
+  reflexivity.
+Qed.
+
+Lemma hard_example : forall l, map (fun x => x + 1) l = map (fun x => 1 + x) l.
+Proof.
+  intros l.
+  (* hard: x is bound by a lambda in the goal *)
+  Fail replace (x + 1) with (1 + x) by ring.
+  (* fails and prints: The variable x was not found in the current environment.*)
+
+  (* This example implements a new repl tactic that will instead succeed. *)
+Abort.
+
+(* Elpi provides a type of tactic argument called open-trm for terms
+    with free variables. Since there is no such a thing as free variables
+    in Elpi, a pre-processor closes the term under binders and pairs the
+    closed term with the number of such "technical binders". *)
+
+Elpi Tactic show_open_term.
+Elpi Accumulate lp:{{
+  solve (goal _ _ _ _ [open-trm N F]) _ :-
+    coq.say "The argument " {coq.term->string F} "was closed under" N "binders".
+}}.
+
+Goal map (fun x => x + x) nil = nil :> list nat.
+elpi show_open_term `(x + _).
+(* prints: The argument fun x : ?e => x + ?e1 was closed under 1 binders *)
+Abort.
+
+(* A key step in the implementation of repl is to align the technical binders
+   of the open term with actual binders present in the goal. For this
+   we use the names as written by the user. We call this operation instantiate *)
+
+(* We put the code into a file, so that we can reuse it later *)
+Elpi File instantiate.code lp:{{
+
+% [instantiate-replacement N Ty x L R L1 R1] is called when crossing
+% a goal binder for the variable x named N and of type Ty. The replacement
+% L with R  is instantiated (if possible) to  L1 with R1
+pred instantiate-replacement i:name, i:term, i:term, i:argument, i:argument, o:argument, o:argument.
+instantiate-replacement N Ty C L R L1 R1 :- std.do! [
+  instantiate N Ty C L L1,
+  instantiate N Ty C R R1,
+].
+
+pred instantiate i:name, i:term, i:term, i:argument, o:argument.
+instantiate _ _ _ (open-trm 0 A) (open-trm 0 A) :- !.
+instantiate N T C (open-trm I F) (open-trm J F1) :- remove-binder-for N T C F F1, !,
+  J is I - 1.
+instantiate _ _ _ X X.
+
+pred remove-binder-for i:name, i:term, i:term, i:term, o:term.
+% we found the binder
+remove-binder-for N _ C (fun N1 _ F) Res :- {coq.name->id N} = {coq.name->id N1}, !,
+  % Remember that in Elpi all names are the same, eg `x` = `y`
+  % coq.name->id gives a string, the string used for printing, and as one expects
+  % not("x" = "y")
+  Res = (F C).
+% we cross the binder and look deeper
+remove-binder-for N T C (fun N1 T1 F) (fun N1 T1 F1) :-
+  @pi-decl N1 T1 x \ remove-binder-for N T C (F x) (F1 x).
+
+}}.
+
+
+Elpi Tactic test_instantiate.
+Elpi Accumulate File instantiate.code.
+Elpi Accumulate lp:{{
+solve (goal _ _ {{ map2 lp:F _ _ = _ }} _ [(open-trm _ LF as L), (open-trm _ RF as R)]) _ :-
+  coq.say "old replacement:" {coq.term->string LF} "with" {coq.term->string RF},
+  F = fun N Ty _,
+  @pi-decl N Ty x\
+    instantiate-replacement N Ty x L R (open-trm _ (L1 x)) (open-trm _ (R1 x)),
+    coq.say "new replacement:" {coq.term->string (L1 x)} "with" {coq.term->string (R1 x)}.
+
+}}.
+
+
+Goal map2 (fun x y => x - y) nil nil = nil.
+elpi test_instantiate `(x - y) `(y + x).
+(* prints: 
+old replacement:
+  fun (x : ?e) (y : ?e0) => x - y
+with
+  fun (y : ?e1) (x : ?e2) => y + x
+
+new replacement:
+  fun y : ?e0 => x - y
+with
+  fun y : ?e1 => y + x
+
+Remark that the technical binders are generated following a left-to-right
+traversal of the term, hence their order varies. This is the reason why we
+need the second rule for remove-binder-for.
+
+Also remark that L1 and R1 need to see the variable we crossed, and that
+is bound by pi: we are capturing the free variable by it (or better removing
+the techincal binding and replacing that bound variable by the variable bound
+by pi).
+
+*)
+Abort.
+
+
+(* We need a few helpers to cress the context *)
+
+Lemma congrP (A : Type) (B : A -> Type) (f g : forall x : A, B x) :
+  f = g -> forall v1 v2 (p : v1 = v2), match p in _ = x return B x with eq_refl => f v1 end = g v2.
+Proof. now intros fg v1 v2 v1v2; rewrite fg, v1v2. Qed.
+
+Lemma congrA (A B : Type) (f g : A -> B) :
+  f = g -> forall v1 v2 (p : v1 = v2), f v1 = g v2.
+Proof. now intros fg v1 v2 v1v2; rewrite fg, v1v2. Qed.
+
+(* We now build the final tactic *)
+
+Elpi Tactic replace.
+Elpi Accumulate File instantiate.code.
+Elpi Accumulate lp:{{
+
+% iterates congrA and congrP to prove f x1..xn = f y1..yn from proofs of xi = yi
+pred mk-app-prf i:term, i:term, i:term, i:list term, i:list term, i: list term, i:term, o:term.
+mk-app-prf _ _ _ [] [] [] P P :- !.
+mk-app-prf F G {{ _ -> lp:Ty }} [X|XS] [Y|YS] [PXY|PS] PFG Q :- !,
+  PFXGY = {{ congrA _ _ lp:F lp:G lp:PFG lp:X lp:Y lp:PXY }},
+  mk-app-prf {coq.mk-app F [X]} {coq.mk-app G [Y]} Ty XS YS PS PFXGY Q.
+mk-app-prf F G {{ forall x, lp:(Ty x) }} [X|XS] [Y|YS] [PXY|PS] PFG Q :-
+  PFXGY = {{ congrP _ _ lp:F lp:G lp:PFG lp:X lp:Y lp:PXY }},
+  mk-app-prf {coq.mk-app F [X]} {coq.mk-app G [Y]} (Ty X) XS YS PS PFXGY Q.
+
+% [replace L R X Y P] replaces L by R in X obtaining Y and
+% a proof P that X = Y. P will contain holes (sub goals) for sub proofs
+% of L = R.
+pred replace i:argument, i:argument, i:term, o:term, o:term.
+
+% all binders are crossed and we find a term identical to L.
+% the proof is a hole of type L = R.
+replace (open-trm 0 L) (open-trm 0 R) L R P :- !,
+  coq.typecheck P {{ lp:L = lp:R }} ok.
+
+% we cross the binder by functional extensionality
+replace L R (fun N T F) (fun N T F1) {{ functional_extensionality lp:{{ fun N T F }} lp:{{ fun N T F1 }} lp:{{ fun N T Prf }}}} :- !,
+  @pi-decl N T x\
+    instantiate-replacement N T x L R (L1 x) (R1 x),
+    replace (L1 x) (R1 x) (F x) (F1 x) (Prf x).
+
+replace L R (app [HD|TS]) (app [HD|TS1]) Prf :-
+  replace-list L R TS TS1 PS,
+  coq.typecheck HD Ty ok,
+  mk-app-prf HD HD Ty TS TS1 PS {{ refl_equal lp:HD }} Prf.
+
+% base cases
+replace _ _ X X {{ refl_equal lp:X }} :- name X, !.
+replace _ _ (global _ as C) C {{ @refl_equal Type lp:C }} :- coq.typecheck-ty C _ ok, !. % we don't like Set
+replace _ _ (global _ as C) C {{ refl_equal lp:C }} :- !.
+% we omit rules for primitive constants, fixpoints, let, forall, ...
+
+pred replace-list i:argument, i:argument, i:list term, o:list term, o:list term.
+replace-list _ _ [] [] [].
+replace-list L R [X|XS] [Y|YS] [P|PS] :- replace L R X Y P, replace-list L R XS YS PS.
+
+solve (goal _ _ {{ lp:X = lp:Y }} _ [(open-trm _ _ as L), (open-trm _ _ as R)] as G) GL :- !, std.do! [
+  replace L R X X1 P,
+  refine {{ @eq_trans _ lp:X lp:X1 lp:Y lp:P _ }} G GL,
+].
+
+solve (goal _ _ {{ _ = _ }} _ _) _ :- !, coq.error "elpi: replace: the goal is not an equality".
+solve _ _ :- !, coq.error "elpi: replace: the two arguments must be open terms".
+
+}}.
+
+Tactic Notation (at level 0) "repl" uconstr(x) "with" uconstr(y) :=
+  elpi replace ltac_open_term:(x) ltac_open_term:(y); simpl.
+
+Tactic Notation (at level 0) "repl" uconstr(x) "with" uconstr(y) "by" tactic(t) :=
+  elpi replace ltac_open_term:(x) ltac_open_term:(y); try (simpl; t).
+
+Lemma hard_example : forall l, map (fun x => x + 1) l = map (fun x => 1 + x) l.
+Proof.
+  intros l.
+  repl (x + 1) with (1 + x) by ring.
+  reflexivity.
+Qed.
+
+Lemma hard_example2 : forall l, map2 (fun x y => x + 0 + y) l l = map2 (fun x y => y + x) l l.
+Proof.
+  intros l.
+  repl (x + 0 + y) with (y + x) by ring.
+  reflexivity.
+Qed.
+
+(* An extended version of this tactic by Y. Bertot can be found in the tests/
+   directory under the name test_open_terms.v *)