New example with comments: ho_equalities, written in Ltac, Ltac2 and coq-elpi

ho_equalities/elpi/ho_equalities.v

@@ -0,0 +1,176 @@
+From elpi Require Import elpi.
+
+(** The main tactic [eliminate_ho_eq] takes a hypothesis which is a 
+higher-order equality of the form [f = g]
+and generates an proves a new hypothesis [forall x1, ... xn, f x1 ... xn = g x1 ... xn] *)
+
+(** 
+Generic considerations about the tactic:
+
+I recommend to look first at the Ltac1 version as the comments will refer to it.
+As we will see, contrary to the Ltac1 version, the difficult part in the elpi implementation
+is not constructing the term but to articulate the tactics 
+together. The only articulation we made here is the chaining between the 
+tactic [myassert] and the tactic [myclear], and this was the longest 
+part to implement.
+
+Here, the tactic takes an hypothesis [H] of the form [f=g] and 
+generates directly an inhabitant (i.e.: a proof) of [forall x1, ... xn, f x1 ... xn = g x1 ... xn]. 
+Another method would have been to generate the hypothesis to prove and use a small Ltac1 or
+Ltac2 script to make the proof. Articulate proof steps in elpi is difficult so I
+would not recommand using a combination of elpi tactics to build a proof.
+I would rather generate the terms in elpi and then go outside the elpi world and use Ltac
+to prove them, or provide the proof term directly. 
+
+*)
+
+(** For some reason, elpi fails when we use original Coq tactics 
+(except if they take no argument), so we have to define our own alias *)
+
+Ltac myassert u :=
+  let H := fresh in assert (H := u); simpl in H.
+
+Ltac myclear H := clear H.
+
+
+(** All elpi tactics start with these two vernacular commands: [Elpi tactic foo.] followed 
+by [Elpi Accumulate lp:{{ some elpi code }}.]
+We can also accumulate separate elpi files but here the code 
+is small so keeping only one file is fine. 
+
+In elpi, we use the lambda-prolog language. Every elpi program
+is written as a combination of predicates, taking inputs or outputs.
+
+Each predicate is defined by its rules.
+On the left of the symbol [:-], we write the head of a rule, and on the right its premises. 
+
+The good thing with elpi is that we have access to the deep syntax of Coq terms 
+(contrary to Ltac1 if you remember our tedious tricks). 
+The type [term], defined here: 
+https://github.com/LPCIC/coq-elpi/blob/b92e2c85ecb6bb3d0eb0fbd57920d553b153e49c/elpi/coq-HOAS.elpi
+represents Coq terms. You can even extend it ! 
+
+The other very important thing is that you have quotations. For
+example: [{{ nat }}], is simply transforming the Coq term nat
+into its elpi quotation. You can also use elpi antiquotation, to transform an elpi term of type term [T]
+into a Coq term, by using [lp:T]
+
+Another crucial point is that there is no such thing as a free variable in elpi. 
+It uses higher-order abstact syntax: to cross a binder, we need to introduce a fresh 
+variable (also called "eigenvariable") in the context of the program.
+Fortunately, we have really useful elpi predicates about eigenvariables: [occurs X Y] which holds if its first 
+argument [X] (a variable bound in the context) occurs in the second argument [Y], 
+and [names L] which has as only argument [L] the list of all the eigenvariables introduced in the context.
+
+Elpi has two kinds of variables: unification variables (also called "metavariables"), 
+used to resolve the clauses which
+define elpi predicates and usually written with capital letters, and eigenvariables written in small letters
+(and that you have to bind explicitely as we will see).
+
+ *)
+
+Elpi Tactic eliminate_ho_eq.
+
+Elpi Accumulate lp:{{
+
+  % I can introduce a one-line comment with a %
+
+  % This auxiliary predicate looks in the context of a goal (that is, its local definitions and hypotheses)
+  % and returns the position of the term given as an input.
+  % The input int here is simply an accumulator.
+
+  pred find-pos-in-context i: goal-ctx, i: term, i: int, o: int.
+      find-pos-in-context [(decl T' _ _)| _XS] T N N :- coq.unify-eq T' T ok. %coq.unify-eq returns ok when T' is syntactically equal to T
+      find-pos-in-context [(decl _T' _ _)| XS] T N R :- !, M is N + 1, find-pos-in-context XS T M R.
+      find-pos-in-context [(def T' _ _ _) | _XS] T N N :- coq.unify-eq T' T ok. 
+      find-pos-in-context [(def _T' _ _ _)| XS] T N R :- !, M is N + 1, find-pos-in-context XS T M R.
+      find-pos-in-context [] _ _ _ :- coq.error "no term equal to this one in the context".
+
+  % This auxiliary predicate clear the Nth hypothesis of the context (the 0th is the last introduced hypothesis)
+  % It uses the API coq.ltac.call in order to invoke some Ltac piece of code (here, our [myclear])
+  % This calling to Ltac takes a list of arguments, the current goal and returns the list of new goals generated by the tactic.
+
+  pred clear-with-pos i: int, i: goal, o: list sealed-goal.
+      clear-with-pos N ((goal Ctx _ _ _ _) as G) GL :-
+        std.nth N Ctx (decl X _ _), coq.ltac.call "myclear" [trm X] G GL.
+      clear-with-pos N ((goal Ctx _ _ _ _) as G) GL :-
+        std.nth N Ctx (def X _ _ _), coq.ltac.call "myclear" [trm X] G GL.
+      clear-with-pos _ _ _ :- coq.error "nothing to clear".
+
+  % Here is our main predicate, generating the proof term of forall x1, ..., xn, f x1 ... xn = g x1 ... xn
+  % starting with a proof [H] of f = g, the terms f ([T1]) and g ([T2]), their type and an accumulator.
+  % The first rule is the recursive case: we suppose that the accumulator does not contain all the xis.
+  % Consequently, we bind a eigenvariable by using [pi x\ decl x Na Ty => ...] 
+  % which means that we introduce an eigenvariable variable [x] which
+  % has the name [Na] and the type [Ty]. Behind the [=>], we are allowed to write some code that mentions [x].
+  % So it is sufficent to make a recursive call in which we add the new variable to the accumulator and we apply the resulting 
+  % proof term to the variable [x].
+  % The second rule is the base case. We generate the proof term which is an application of [@eq_ind_r].
+  % We can live holes in the proof as the call to [refine] will fill them.
+  % The functons [T1] and [T2] are transformed into their applied version (we applied them to all 
+  % the eigenvariables generated by our recursive calls).
+
+  pred mk-proof-eq i: term i: term, i: term, i: term, i:list term, o: term.
+    mk-proof-eq H T1 T2 (prod Na Ty F1) Acc (fun Na Ty F2) :- 
+      pi x\ decl x Na Ty =>
+        mk-proof-eq H T1 T2 (F1 x) [x|Acc] (F2 x).
+    mk-proof-eq H T1 T2 _ Acc {{ @eq_ind_r _ lp:T2 lp:Predicate (eq_refl lp:T2Args) lp:T1 lp:H }} :-
+      std.rev Acc Args,
+      coq.mk-app T2 Args T2Args,
+      Predicate = {{ fun y => lp:{{ app[ {{y}} | Args] }} = lp:T2Args }}.
+
+  % All elpi tactics must use the [solve] predicate. It takes a goal and returns the list of subgoals generated by the tactic.
+  % Note that the goal given as input is open, that is, all the variables in the context are considered as eigenvariables.
+  % The outputed list of goals contains sealed-goals: that is, functions binding the variables in the context (by an operator called "nabla").
+  % When we open new goals by introducing all the eigenvariables that represent the terms in the local context, 
+  % the eigenvariables identifiers used in elpi are different that the one used in the previous goals.
+  % This poins causes several problem. Indeed, if we work on a context variable [c0] and generate a new goal, 
+  % [c0] means nothing for the new goal, as it is not in the program context anymore. An hypothesis with the same Coq identifier
+  % and the same type may be in the local context of the new goal, but elpi always chooses a different name. 
+  % So maybe it is called [c1] now... Forgetting this is a frequent cause of failure in elpi.
+  % This is the reason why we computed the position [N] of our hypothesis [H] in the context: we can retrieve [H] in a new goal 
+  % (this will be the [N+1]th hypothesis, as we introduced a new hypothesis at the top of our context). 
+
+  solve ((goal Ctx _ _ _ [trm H]) as Goal) NewGoals :- % I would recommand to look at 
+    % https://lpcic.github.io/coq-elpi/tutorial_coq_elpi_tactic.html#defining-tactics to understand the [goal] predicate
+
+    std.do! % [std.do! L] tries to runs everything in [L] and never backtracks
+    [coq.typecheck H (app [{{ @eq }}, Ty, T1, T2]) ok, % the given hypothesis should be of type [f = g] 
+     mk-proof-eq H T1 T2 Ty [] R1, % we build the proof term given the initial hypothesis, the functions and their types
+     coq.typecheck R1 _ ok, % we typecheck R1 to fill the holes in the proof
+     find-pos-in-context Ctx H 0 N, % we find the position of H in the context as we want to clear it in a new goal
+     coq.ltac.call "myassert" [trm R1] Goal [NewGoal| _], % we add the proof term in the local context and we get a sealed-goal [NewGoal]
+     coq.ltac.open (clear-with-pos (N + 1)) NewGoal NewGoals]. 
+    % as the [clear-with-pos] predicate works on open goals, we use the [coq.ltac.open] function to transform NewGoal into its not sealed version
+}}.
+Elpi Typecheck.
+
+
+(** elpi introduces new parsing annotations for [Tactic Notation], 
+here, we use [ltac_term] but we also have [ltac_term_list] 
+if the tactic we defined takes several arguments *)
+
+Tactic Notation "eliminate_ho_eq" hyp(t) :=
+  elpi eliminate_ho_eq ltac_term:(t).
+
+Section Tests.
+
+Goal forall (f g : forall (A B : Type) (a : A) (b : B), A * B), f = g -> False.
+intros f g Heq. 
+assert (H : length =
+fun A : Type =>
+fix length (l : list A) : nat :=
+  match l with
+  | nil => 0
+  | (_ :: l')%list => S (length l')
+  end) by reflexivity. eliminate_ho_eq H.
+assert (H1 : Nat.add =
+fix add (n m : nat) {struct n} : nat :=
+  match n with
+  | 0 => m
+  | S p => S (add p m)
+  end) by reflexivity. eliminate_ho_eq H1.
+eliminate_ho_eq Heq. 
+Abort.
+
+End Tests.

ho_equalities/ltac1/ho_equalities.v

@@ -0,0 +1,107 @@
+(** The main tactic [eliminate_ho_eq] takes a hypothesis which is a 
+higher-order equality of the form [f = g]
+and generates an proves a new hypothesis [forall x1, ... xn, f x1 ... xn = g x1 ... xn] *)
+
+(** One of the main difficulty of Ltac is that we can't work easily 
+under binders.Try to write a Ltac function which counts the number of (prenex) quantifiers
+in a term to convince yourself !
+
+In order to implement our tactic, we have to cross an arbitrary number of binders, 
+because the functions we consider have an unknown number [n] of arguments.
+But Ltac syntax is high-level, we can't access to the internal representation 
+of a Coq term.
+We can write easily a non-generic tactic which works for functions with 1, 2, 3 ... arguments.
+However, there is a trick to always work on function with one argument, and to 
+avoid the problem: uncurrying ! 
+Thus, the tactic recurses on a function which takes a dependent pair (of the form [{ x : A & P x}])
+In the end, the first projection of the pair should contain all the arguments of the function except the last one.
+The last argument is then contained in the second projection.
+
+In addition, the syntax [@?f x] allows us to use patterns which mentions 
+variables. Here, [f] is indeed a metavariable (i.e.: a variable which has to be unified 
+with a concrete Coq term) which can see [x]. *)
+
+
+Inductive default :=.
+
+Ltac get_uncurry_eq A := 
+  let rec tac_rec A := (* A is a function taking a dependent pair and returning the equality between f and g *)
+  lazymatch constr:(A) with
+    | fun p => @eq (forall (x : @?B p), @?body p x) (@?f p) (@?g p) => 
+        tac_rec ltac:(eval cbv beta in (* we need to reduce the term because the pattern matching of Ltac is purely
+  syntactic, so not up to reduction *)
+        (fun (p : {x & B x})  => @eq (body (projT1 p) (projT2 p)) (f (projT1 p) (projT2 p)) (g (projT1 p) (projT2 p))))
+    | ?C =>  C
+  end in tac_rec (fun _: default => A).
+(* the function we start with takes a dumb default value because 
+we always need two types to build dependent pairs *)
+
+(** After calling get_uncurry_eq on a higher-order equality f = g, 
+we get a term of the form
+[(fun p : {x1 : {x2 : { ... { xn : default & Pn } ...} } } =>
+ f (projT2 (projT1 (projT1 ... (projT1 p)... ))) ... (projT2 (projT1 p)) ... (projT2 p) =
+ g (projT2 (projT1 (projT1 ... (projT1 p)... ))) ... (projT2 (projT1 p)) ... (projT2 p)]
+
+The next step is to curry it, and to remove the useless argument of type [default].
+
+The next function [dependent_curry_eq] does precise reductions, because 
+we need to reduce the term in order to use the syntactical match of Ltac, 
+but not too much, because we may unfold a constant we do not want to 
+For instance, if we work on an equality between a constant and its body; we 
+do not want to unfold the constant, otherwise the two members of the equality will 
+become syntactically equal. *)
+
+
+Ltac dependent_curry_eq t :=
+  lazymatch t with
+    | forall (_ : default), ?h => constr:(h) (* removing the default argument *)
+    | fun (y: { x : _ & @?P x}) => @?body y =>
+        dependent_curry_eq 
+        ltac:(let t := eval cbv beta in (forall a b, body (existT _ a b)) in
+        let t' := eval unfold projT1 in t in eval unfold projT2 in t') (* we should match this branch in the first call 
+of the function, as it binds only one argument *)
+   | forall (y: { x : _ & @?P x}) (z : @?Q y), @?body y z  =>
+        dependent_curry_eq 
+        ltac:(let t := eval cbv beta in (forall a b (c : Q (existT _ a b)), body (existT _ a b) c) in 
+              let t' := eval unfold projT1 in t in eval unfold projT2 in t') (* we should match this branch in the
+following calls. Note that it is crucial to mention the variable z of type Q y, as it depends on the previous binder 
+(a dependent pair) *)
+    | _ => ltac:(let t' := eval unfold projT1 in t 
+                 in eval unfold projT2 in t')
+  end.
+
+
+(** The last tactic [eliminate_ho_eq] is trivial, it combines the previous steps 
+and proves the statement with a really small proof script *) 
+
+Ltac eliminate_ho_eq H :=
+  let T := type of H in 
+  let T' := get_uncurry_eq T in
+  let T'' := dependent_curry_eq T' in 
+  let H0 := fresh H in 
+  assert (H0 : T'') by (intros ; rewrite H ; reflexivity); clear H.
+
+Section tests.
+
+Variable (f : forall (A B : Type) (a : A) (b : B), A * B).
+Variable (g : forall (A B : Type) (a : A) (b : B), A * B).
+Variable (Heq : f = g).  
+
+Goal False. 
+assert (H : length =
+fun A : Type =>
+fix length (l : list A) : nat :=
+  match l with
+  | nil => 0
+  | (_ :: l')%list => S (length l')
+  end) by reflexivity. eliminate_ho_eq H.
+assert (H1 : Nat.add =
+fix add (n m : nat) {struct n} : nat :=
+  match n with
+  | 0 => m
+  | S p => S (add p m)
+  end) by reflexivity. eliminate_ho_eq H1.
+eliminate_ho_eq Heq.
+Abort.
+
+End tests.

ho_equalities/ltac2/ho_equalities.v

@@ -0,0 +1,94 @@
+From Ltac2 Require Import Ltac2.
+From Ltac2 Require Import Constr.
+Import Unsafe.
+
+(** The main tactic [eliminate_ho_eq] takes a hypothesis which is a 
+higher-order equality of the form [f = g]
+and generates an proves a new hypothesis [forall x1, ... xn, f x1 ... xn = g x1 ... xn] *)
+
+(** The unsafe module in the Constr file allow us to have access to the 
+Coq's kernel terms. In Ltac2, we always need to match on the kind of the constr 
+to retrieve its structure. 
+To understand how it works, I strongly recommand to look at the source : 
+https://github.com/coq/coq/blob/master/user-contrib/Ltac2/Constr.v 
+
+The kernel represents variables either by names ([Var] constructor)
+or by their De Brujin index ([Rel] constructor). 
+A De Brujin index [n] is an integer which denotes the number 
+of binders that are in scope between the variable [Rel n] and 
+its corresponding binder.
+*)
+
+(** The main function [gen_eq] takes the functions [f] and [g], the type of [f] [tyf],
+and a list [l] (the variables [x1 ... xn] which we will 
+introduce one by one).
+
+In the base case (we obtained all the arguments for the functions), we build an array containing all 
+the arguments [x1 ... xn] and we give it to [f] and [g], getting [f x1 ... xn] and 
+[g x1 ... xn].
+
+In the recursive case we create a new variable with De Brujin index 1 (as in the kernel, 
+the indexes start by 1), add it to the list of (lifted) variables and recurse under the binder
+
+ *)
+Ltac2 rec gen_eq (f: constr) (g : constr) (tyf : constr) (l: int list) :=
+  match kind tyf with
+    | Prod bind ty => make (Prod bind (gen_eq f g ty (1::List.map (fun x => Int.add x 1) l)))
+    | _ => 
+        let lrel := List.map (fun x => Rel x) l in
+        let lconstr := List.rev (List.map make lrel) in 
+        let f_app := make (App f (Array.of_list lconstr)) in
+        let g_app := make (App g (Array.of_list lconstr)) in 
+        make (App constr:(@eq) (Array.of_list [tyf ; f_app; g_app]))
+  end.
+
+(** The main function uses Control.hyp h to retrieve the constr given the 
+identifier of the hypothesis [h] and checks that its type is an equality.
+It is written [match!] and not [match] because Ltac2 has a low-level match [match]
+and a high-level match [match!]. The last one is similar to the one of Ltac1: 
+we can directly use the syntax of Coq terms and not the syntax of Ltac2.
+
+Once the function has split the product type (argument [a]), 
+a call to the main function is made *)  
+
+Ltac2 eliminate_ho_eq (h : ident) :=
+  let t := Control.hyp h in
+  match! type t with
+    | @eq ?a ?f ?g =>
+        let c := gen_eq f g a [] in assert $c 
+  end.
+
+(** Tactic Notation is useful to transform Ltac2 functions
+into Ltac1 tactics, but we need to use the quotation [ltac2:( arg1 ... arg1 |- ...)] *)
+
+Tactic Notation "eliminate_ho_eq" ident(H) := 
+  let f := ltac2:(id |- 
+  let id2 := Ltac1.to_ident id in 
+  let id3 := match id2 with 
+      | None => Control.throw (Not_found)
+      | Some id3 => id3 
+    end in eliminate_ho_eq id3) in f H.
+
+Section tests.
+
+Set Default Proof Mode "Classic". (* Switchs from Ltac2 to Ltac1 proof mode *)
+
+Goal forall (f g : forall (A B : Type) (a : A) (b : B), A * B) (Heq : f = g), False.
+intros f g Heq. 
+assert (H : length =
+fun A : Type =>
+fix length (l : list A) : nat :=
+  match l with
+  | nil => 0
+  | (_ :: l')%list => S (length l')
+  end) by reflexivity. eliminate_ho_eq H. 
+assert (H1 : Nat.add =
+fix add (n m : nat) {struct n} : nat :=
+  match n with
+  | 0 => m
+  | S p => S (add p m)
+  end) by reflexivity. eliminate_ho_eq H1. 
+eliminate_ho_eq Heq.
+Abort.
+
+End tests.