From 0b7ecf043cef5a1eb91229903cf93172d907136b Mon Sep 17 00:00:00 2001
From: lduboisd <louise.dubois-de-prisque@inria.fr>
Date: Sun, 3 Dec 2023 17:35:49 +0100
Subject: [PATCH 1/9] add ltac1 version of ho equalities

---
 ho_equalities/ltac1/ho_equalities.v | 107 ++++++++++++++++++++++++++++
 1 file changed, 107 insertions(+)
 create mode 100644 ho_equalities/ltac1/ho_equalities.v

diff --git a/ho_equalities/ltac1/ho_equalities.v b/ho_equalities/ltac1/ho_equalities.v
new file mode 100644
index 0000000..f5a2809
--- /dev/null
+++ b/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.

From ea096f0d25a373439561f7a21e570a0db95d52e1 Mon Sep 17 00:00:00 2001
From: lduboisd <louise.dubois-de-prisque@inria.fr>
Date: Mon, 4 Dec 2023 10:35:43 +0100
Subject: [PATCH 2/9] elpi version of ho_equalities

---
 ho_equalities/elpi/ho_equalities.v | 78 ++++++++++++++++++++++++++++++
 1 file changed, 78 insertions(+)
 create mode 100644 ho_equalities/elpi/ho_equalities.v

diff --git a/ho_equalities/elpi/ho_equalities.v b/ho_equalities/elpi/ho_equalities.v
new file mode 100644
index 0000000..eb81deb
--- /dev/null
+++ b/ho_equalities/elpi/ho_equalities.v
@@ -0,0 +1,78 @@
+From elpi Require Import elpi.
+
+(** Contrary to the Ltac version, the difficult part in the elpi implementation
+is not constructing the term but to articulate the tactics 
+together. *)
+
+Ltac myassert u :=
+  let H := fresh in assert (H := u); simpl in H.
+
+Ltac myclear H := clear H.
+
+Elpi Tactic eliminate_ho_eq.
+
+Elpi Accumulate lp:{{
+
+  pred get-head i:term o:term.
+    get-head (app [F|_]) R :- get-head F R.
+    get-head T T.
+
+  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. 
+      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".
+
+  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".
+    
+  pred mk-proof-eq i: term i: term, i: term, i: term, o: term.
+    mk-proof-eq H T1 T2 (prod Na Ty F1) (fun Na Ty F2) :- 
+      pi x\ decl x Na Ty => mk-proof-eq H (app [T1, x]) (app [T2, x]) (F1 x) (F2 x).
+    mk-proof-eq H T1 T2 Codom
+      (app [{{@eq_ind_r}}, Ty', T2', (fun _ Ty' (y\ (app [{{ @eq }} , Codom, app [y | L'], T2]))), app [{{@eq_refl}}, Ty, T2], T1', H]) :-
+      get-head T1 T1', get-head T2 T2', coq.typecheck T1 Ty ok, coq.typecheck T1' Ty' ok,  names L, std.filter L (x\ occurs x T1) L'.
+
+  solve ((goal Ctx _ _ _ [trm H]) as Goal) NewGoals :- std.do!
+    [coq.typecheck H (app [{{ @eq }}, Ty, T1, T2]) ok, 
+     mk-proof-eq H T1 T2 Ty R1, 
+     find-pos-in-context Ctx H 0 N,
+     coq.ltac.call "myassert" [trm R1] Goal [NewGoal| _],
+     coq.ltac.open (clear-with-pos (N + 1)) NewGoal NewGoals]. 
+}}.
+Elpi Typecheck.
+
+Tactic Notation "eliminate_ho_eq" constr(t) :=
+  elpi eliminate_ho_eq ltac_term:(t).
+
+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.
+generalize Heq. intro Heq'. (* here, we have to generalize the section variable, as section variables do not appear 
+in the reified context of a Coq Goal in elpi. Otherwise, the call to clear will fail *)
+eliminate_ho_eq Heq'. 
+Abort.
+
+End Tests.
\ No newline at end of file

From b7827f06e7411ba76b32c88e53d3798ab94a68ac Mon Sep 17 00:00:00 2001
From: lduboisd <louise.dubois-de-prisque@inria.fr>
Date: Mon, 4 Dec 2023 12:01:59 +0100
Subject: [PATCH 3/9] an elpi version full of comments

---
 ho_equalities/elpi/ho_equalities.v | 128 +++++++++++++++++++++++++++--
 1 file changed, 119 insertions(+), 9 deletions(-)

diff --git a/ho_equalities/elpi/ho_equalities.v b/ho_equalities/elpi/ho_equalities.v
index eb81deb..f0daf18 100644
--- a/ho_equalities/elpi/ho_equalities.v
+++ b/ho_equalities/elpi/ho_equalities.v
@@ -1,35 +1,124 @@
 From elpi Require Import elpi.
 
-(** Contrary to the Ltac version, the difficult part in the elpi implementation
+(** 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. *)
+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. 
+
+*)
+
+(** 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 toto.] 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.
+For instance, [get-head T T'] takes a term [T] as input and returns a term [T'] (the same one if it is not 
+an application, and its head otherwise)
+
+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. 
+Thus, [get-head (app [F|_]) R :- get-head F R] means that the output [R] is the head of the application of [F]
+to any arguments (so we use a wildcard) only if it is also the head of [F].
+
+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. In the code, you will see 
+an example: [{{ @eq }}], which is simply turning the Coq term for propositional equality
+into its elpi quotation. You can also use elpi antiquotation, for inserting elpi variables 
+into a Coq term, but we won't need this here.
+
+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 written with capital letters, and eigenvariables written is small letter
+(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 %
 
-  pred get-head i:term o:term.
+  pred get-head i:term o:term. % [i:] means input and [o:] means output
     get-head (app [F|_]) R :- get-head F R.
     get-head T T.
 
+  % 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. 
+      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]), and their type.
+  % The first rule is the recursive case: we suppose that the functions given as 
+  % inputs are only partially applied (or not applied at all).
+  % 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 apply the functions and 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 managed to find the exact form of the proof term by some trials and errors using Ltac's [refine].
+  % Instead of focusing of its hardly readable form, I suggest that you look at the use of elpi's predicates
+  % [names] and [occurs]. We needed to apply the function variable [y] on the correct arguments.
+  % To find them, we looked at all the eigenvariables of our program by using [names L], and then filter these to keep 
+  % only the ones in [T1] (remember that [T1] is precisely f x1 ... xn).
     
   pred mk-proof-eq i: term i: term, i: term, i: term, o: term.
     mk-proof-eq H T1 T2 (prod Na Ty F1) (fun Na Ty F2) :- 
@@ -38,15 +127,36 @@ Elpi Accumulate lp:{{
       (app [{{@eq_ind_r}}, Ty', T2', (fun _ Ty' (y\ (app [{{ @eq }} , Codom, app [y | L'], T2]))), app [{{@eq_refl}}, Ty, T2], T1', H]) :-
       get-head T1 T1', get-head T2 T2', coq.typecheck T1 Ty ok, coq.typecheck T1' Ty' ok,  names L, std.filter L (x\ occurs x T1) L'.
 
-  solve ((goal Ctx _ _ _ [trm H]) as Goal) NewGoals :- std.do!
-    [coq.typecheck H (app [{{ @eq }}, Ty, T1, T2]) ok, 
-     mk-proof-eq H T1 T2 Ty R1, 
-     find-pos-in-context Ctx H 0 N,
-     coq.ltac.call "myassert" [trm R1] Goal [NewGoal| _],
+  % 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
+     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" constr(t) :=
   elpi eliminate_ho_eq ltac_term:(t).
 

From 4a92258dae0cc03b8acfa20433f32220d5d58571 Mon Sep 17 00:00:00 2001
From: lduboisd <louise.dubois-de-prisque@inria.fr>
Date: Mon, 4 Dec 2023 18:57:40 +0100
Subject: [PATCH 4/9] try to use in context

---
 ho_equalities/ltac2/ho_equalities.v | 123 ++++++++++++++++++++++++++++
 1 file changed, 123 insertions(+)
 create mode 100644 ho_equalities/ltac2/ho_equalities.v

diff --git a/ho_equalities/ltac2/ho_equalities.v b/ho_equalities/ltac2/ho_equalities.v
new file mode 100644
index 0000000..ba6463d
--- /dev/null
+++ b/ho_equalities/ltac2/ho_equalities.v
@@ -0,0 +1,123 @@
+From Ltac2 Require Import Ltac2.
+From Ltac2 Require Import Constr.
+Import Unsafe.
+Set Default Proof Mode "Classic".
+Set Printing Existential Instances.
+Set Printing Goal Names.
+
+Goal True.
+let H := fresh in epose (H := ?[x] : ?[Goal]).
+refine (_ _).  Focus 2.
+instantiate (Goal2 := nat).
+
+
+
+
+ assert H. unfold H.
+instantiate (x := (forall (A : Type), A)). intros A.
+refine ( _ _). Focus 2. exact H. *) 
+(* 
+Ltac2 rec make_binder_list (l : (ident option * constr) list) :=
+  match l with
+    | [] => []
+    | (id, a) :: l => Binder.unsafe_make id Binder.Relevant a :: make_binder_list l
+  end. *)
+
+
+Ltac2 split_prod (t : constr) :=
+  let rec aux t acc :=
+    match kind t with
+      | Prod bind t' =>
+          aux t' ((Binder.name bind, Binder.type bind) :: acc)
+      | _ => (acc, t)
+    end in aux t [].
+
+Ltac2 rec gen_eq (hyp: constr) (binds :(ident option * constr) list) (b: constr) (f : constr) (g : constr) (l: kind list) () :=
+Message.print (Message.of_string "test") ;
+  match binds with
+    | [] =>
+        let idH := ident:(H) in 
+        let frees := Fresh.Free.of_ids [ident:(H)] in 
+        let rels := Array.of_list (List.rev (List.map make l)) in
+        let f := make (App f rels) in Message.print (Message.of_constr f) ;
+        let g := make (App g rels) in
+        let arr := Array.of_list [b; f; g] in 
+        let trm := make (App constr:(@eq) arr) in 
+          ltac1:(term |- instantiate (Goal0 := term)) (Ltac1.of_constr trm)
+        (* assert (id : $trm) *) (* by (rewrite $hyp; reflexivity) ; Std.revert [idH] *)
+    | (opt, c) :: binds => 
+        let id :=
+          match opt with
+            | None => 
+                let idH := ident:(H) in
+                let frees := Fresh.Free.of_ids [ident:(H)] in
+                Fresh.fresh frees idH
+            | Some id => id
+          end in  Message.print (Message.of_constr c) ;
+        let newbinds := List.map (fun (x, y) => (x, substnl [make (Var id)] 0 y)) binds in
+        let proof := 
+          in_context id c (gen_eq hyp newbinds b f g ((Var id) :: l)) in
+        let frees := Fresh.Free.of_ids [@proof] in
+        let id := Fresh.fresh frees @proof in assert (id := $proof)
+      end.
+
+
+Ltac2 eliminate_ho_eq (t : constr) :=
+  match! type t with
+    | @eq ?a ?f ?g => 
+        let (l, b) := split_prod a in
+        gen_eq t (List.rev l) b f g [] ()
+  end.
+        
+  
+        
+        (* 
+        let new_eq := make (Prod bind 
+        
+
+
+
+
+        let f' := (liftn 1 0 f) in
+        let g' := (liftn 1 0 g) in
+        (Prod bind (make (gen_eq l b f' g' (0 :: (List.map (fun x => Int.add x 1) rels))))) 
+  end.
+ 
+Ltac2 rec gen_eq (l : binder list) (b: constr) (f: constr) (g: constr) (rels: int list) :=
+  match l with
+    | [] => 
+        let vars := Array.map (fun x => make (Rel x)) (Array.of_list rels) in
+        let arr := Array.of_list [b; make (App f vars); make (App g vars)] in
+        (App constr:(@eq) arr)
+    | bind :: l =>
+        let f' := (liftn 1 0 f) in
+        let g' := (liftn 1 0 g) in
+        (Prod bind (make (gen_eq l b f' g' (0 :: (List.map (fun x => Int.add x 1) rels))))) 
+  end.
+     *)
+(* constr list -> int -> constr -> constr *)
+
+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. intro. intro. reflexivity.
+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.
\ No newline at end of file

From 96be9bbb45dec5e3842967558e69cdcabc57f22a Mon Sep 17 00:00:00 2001
From: lduboisd <louise.dubois-de-prisque@inria.fr>
Date: Tue, 5 Dec 2023 08:54:21 +0100
Subject: [PATCH 5/9] working ltac2 version

---
 ho_equalities/ltac2/ho_equalities.v | 107 +++++++++-------------------
 1 file changed, 32 insertions(+), 75 deletions(-)

diff --git a/ho_equalities/ltac2/ho_equalities.v b/ho_equalities/ltac2/ho_equalities.v
index ba6463d..ff4b052 100644
--- a/ho_equalities/ltac2/ho_equalities.v
+++ b/ho_equalities/ltac2/ho_equalities.v
@@ -1,28 +1,6 @@
 From Ltac2 Require Import Ltac2.
 From Ltac2 Require Import Constr.
 Import Unsafe.
-Set Default Proof Mode "Classic".
-Set Printing Existential Instances.
-Set Printing Goal Names.
-
-Goal True.
-let H := fresh in epose (H := ?[x] : ?[Goal]).
-refine (_ _).  Focus 2.
-instantiate (Goal2 := nat).
-
-
-
-
- assert H. unfold H.
-instantiate (x := (forall (A : Type), A)). intros A.
-refine ( _ _). Focus 2. exact H. *) 
-(* 
-Ltac2 rec make_binder_list (l : (ident option * constr) list) :=
-  match l with
-    | [] => []
-    | (id, a) :: l => Binder.unsafe_make id Binder.Relevant a :: make_binder_list l
-  end. *)
-
 
 Ltac2 split_prod (t : constr) :=
   let rec aux t acc :=
@@ -32,85 +10,64 @@ Ltac2 split_prod (t : constr) :=
       | _ => (acc, t)
     end in aux t [].
 
-Ltac2 rec gen_eq (hyp: constr) (binds :(ident option * constr) list) (b: constr) (f : constr) (g : constr) (l: kind list) () :=
-Message.print (Message.of_string "test") ;
+Ltac2 fresh_ident_of_option (opt : ident option) :=
+  match opt with
+    | None => 
+        let idH := ident:(H) in
+        let frees := Fresh.Free.of_ids [ident:(H)] in
+        Fresh.fresh frees idH
+    | Some id => id
+  end.
+
+Ltac2 rec gen_eq (hyp: ident) (binds :(ident option * constr) list) (b: constr) (f : constr) (g : constr) (l: kind list) () :=
   match binds with
     | [] =>
-        let idH := ident:(H) in 
-        let frees := Fresh.Free.of_ids [ident:(H)] in 
         let rels := Array.of_list (List.rev (List.map make l)) in
-        let f := make (App f rels) in Message.print (Message.of_constr f) ;
+        let f := make (App f rels) in 
         let g := make (App g rels) in
         let arr := Array.of_list [b; f; g] in 
         let trm := make (App constr:(@eq) arr) in 
-          ltac1:(term |- instantiate (Goal0 := term)) (Ltac1.of_constr trm)
-        (* assert (id : $trm) *) (* by (rewrite $hyp; reflexivity) ; Std.revert [idH] *)
+        let idH := Fresh.in_goal @H in 
+        let h := Control.hyp hyp in 
+        assert (idH : $trm) by ltac1:(h |- rewrite h ; reflexivity) (Ltac1.of_constr h) ; eapply &idH 
     | (opt, c) :: binds => 
-        let id :=
-          match opt with
-            | None => 
-                let idH := ident:(H) in
-                let frees := Fresh.Free.of_ids [ident:(H)] in
-                Fresh.fresh frees idH
-            | Some id => id
-          end in  Message.print (Message.of_constr c) ;
+        let id := fresh_ident_of_option opt in 
         let newbinds := List.map (fun (x, y) => (x, substnl [make (Var id)] 0 y)) binds in
         let proof := 
-          in_context id c (gen_eq hyp newbinds b f g ((Var id) :: l)) in
-        let frees := Fresh.Free.of_ids [@proof] in
-        let id := Fresh.fresh frees @proof in assert (id := $proof)
+          in_context id c (gen_eq hyp newbinds (substnl [make (Var id)] (List.length binds) b) f g ((Var id) :: l)) in
+        let id :=  Fresh.in_goal @H in assert ($id := $proof) ; ltac1:(proof |- try (exact proof)) (Ltac1.of_constr proof)
       end.
 
-
-Ltac2 eliminate_ho_eq (t : constr) :=
+Ltac2 eliminate_ho_eq (h : ident) :=
+  let t := Control.hyp h in
   match! type t with
     | @eq ?a ?f ?g => 
         let (l, b) := split_prod a in
-        gen_eq t (List.rev l) b f g [] ()
+        gen_eq h (List.rev l) b f g [] () ;
+        ltac1:(H |- clear H) (Ltac1.of_constr t)
   end.
-        
-  
-        
-        (* 
-        let new_eq := make (Prod bind 
-        
-
 
-
-
-        let f' := (liftn 1 0 f) in
-        let g' := (liftn 1 0 g) in
-        (Prod bind (make (gen_eq l b f' g' (0 :: (List.map (fun x => Int.add x 1) rels))))) 
-  end.
- 
-Ltac2 rec gen_eq (l : binder list) (b: constr) (f: constr) (g: constr) (rels: int list) :=
-  match l with
-    | [] => 
-        let vars := Array.map (fun x => make (Rel x)) (Array.of_list rels) in
-        let arr := Array.of_list [b; make (App f vars); make (App g vars)] in
-        (App constr:(@eq) arr)
-    | bind :: l =>
-        let f' := (liftn 1 0 f) in
-        let g' := (liftn 1 0 g) in
-        (Prod bind (make (gen_eq l b f' g' (0 :: (List.map (fun x => Int.add x 1) rels))))) 
-  end.
-     *)
-(* constr list -> int -> constr -> constr *)
+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.
 
-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).  
+Set Default Proof Mode "Classic".
 
-Goal False. 
+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. intro. intro. reflexivity.
+  end) by reflexivity. eliminate_ho_eq H.  
 assert (H1 : Nat.add =
 fix add (n m : nat) {struct n} : nat :=
   match n with

From f257b1baf2cdef120a82a0551fce5bad0b2aa57e Mon Sep 17 00:00:00 2001
From: lduboisd <louise.dubois-de-prisque@inria.fr>
Date: Tue, 5 Dec 2023 09:48:42 +0100
Subject: [PATCH 6/9] comments for ltac2 version

---
 ho_equalities/ltac2/ho_equalities.v | 104 +++++++++++++++++++++++++---
 1 file changed, 95 insertions(+), 9 deletions(-)

diff --git a/ho_equalities/ltac2/ho_equalities.v b/ho_equalities/ltac2/ho_equalities.v
index ff4b052..44c914f 100644
--- a/ho_equalities/ltac2/ho_equalities.v
+++ b/ho_equalities/ltac2/ho_equalities.v
@@ -2,6 +2,29 @@ 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.
+*)
+
+(** This auxilary function will help us to retrieve the type of the two equal functions.
+We split the product between each argument domain and the codomain. 
+The [Prod] constructor takes a binder (namely a name, a type and a relevance) 
+and a constr to make a new constr. The relevance is only useful when you work in SProp, 
+otherwise you will do fine by using the relevance Binder.Relevant *)
+
 Ltac2 split_prod (t : constr) :=
   let rec aux t acc :=
     match kind t with
@@ -10,15 +33,65 @@ Ltac2 split_prod (t : constr) :=
       | _ => (acc, t)
     end in aux t [].
 
+(** This function helps us to get a fresh ident starting from
+an ident option. Note that the annotation [@H] 
+(or [ident:(H)] as a shorthand) allows to quote [H] as an ident in Ltac2.
+Fresh.free_of_ids generates the list of the free variables in an ident, 
+and Fresh.fresh generates an ident starting to a given one ([@H])
+which does not belong to a set of free variables (here, [frees]). *)
+ 
+
 Ltac2 fresh_ident_of_option (opt : ident option) :=
   match opt with
-    | None => 
-        let idH := ident:(H) in
-        let frees := Fresh.Free.of_ids [ident:(H)] in
-        Fresh.fresh frees idH
+    | None =>
+        let frees := Fresh.Free.of_ids [@H] in
+        Fresh.fresh frees @H
     | Some id => id
   end.
 
+(** The main function [gen_eq] takes an ident [hyp] which is the one of the premise [f = g], 
+a list of binders (the name and the type of the arguments of the functions), the codomain [b],
+[f] and [g] our functions, and a list of kind [l] (the variables [x1 ... xn] which we will 
+introduce one by one). It also expects a term of type unit because this function is in fact a thunk, 
+evaluated only for its side effects on the proof state. 
+
+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].
+We build the desired equality [equ] and we assert it. 
+We designate this hypothesis of type [equ] by a new ident [idH].
+The proof of [equ] is made by a small Ltac2 script: [rewrite $h; reflexivity].
+Here, we use [$h] because [rewrite] takes a Coq term. Thus, [$] performs 
+an antiquotation from the constr of Ltac2 to the underlying Coq term.
+
+The last tactic of the base case, [eapply &idH], will become clearer once we looked at the recursive
+case. It is here because when we reach the base case, we are not in the main goal. The goal here is 
+just a metavariable of any type. So we should then precise our goal, and thus we say that it is [&idH],
+the Coq term designated by the ident [idH], which is of type [trm].
+
+In the recursive case, we introduce a new constr which is a named variable: [make (Var id)], of type [a].
+Consequently, we should substitute the De Brujin index 0 contained in [f], in [g], in [b] and in the 
+type of the other binders by [make (Var id)]. 
+We cannot work directly on De Brujin indexes because each time we call the function [make]
+to build a constr from a kind, [make] will perform a type-checking. So if a term contains free variables, 
+the type-checking will fail, producing a fatal error. 
+In my opinion, this leads to a lot of difficulties, making Ltac2 a language 
+that I do NOT recommend to use for working with De Brujin indexes. But still, we will 
+find a solution in this tutorial.
+
+The trick is to use [in_context id c tac], which runs a tactic [tac] on a new goal (a metavariable of any type),
+keeping the same hypotheses as the previous goal, but with a new hypothesis id : c, and returns the term
+[fun (id : c) => t], where [t] is a proof of the new arbitrary goal.
+This explains the line [let proof := in_context ... ]. We can retrieve the proof [t] of [f x1 ... xn = g xn ... xn], 
+created in a context in which [x1 ... xn] are bound, and abstrating it to [fun x1 ... xn => t]. 
+In order to keep this proof in each recursive call (where the goal is also a metavariable [?Goal]), we
+prove [?Goal] by [exact proof]. Here, we used Ltac1 inside ltac2, to show the syntax to call Ltac1 tactics.
+We write [ltac1:(tac)] for tactics taking no arguments, and [ltac1:(arg1 ... argn |- tac)]
+otherwise. In the second case, the arguments should be of type Ltac1.t, so we perform some casts.
+Indeed, our function uses [Ltac1.of_constr].
+
+ *)
+
 Ltac2 rec gen_eq (hyp: ident) (binds :(ident option * constr) list) (b: constr) (f : constr) (g : constr) (l: kind list) () :=
   match binds with
     | [] =>
@@ -26,18 +99,28 @@ Ltac2 rec gen_eq (hyp: ident) (binds :(ident option * constr) list) (b: constr)
         let f := make (App f rels) in 
         let g := make (App g rels) in
         let arr := Array.of_list [b; f; g] in 
-        let trm := make (App constr:(@eq) arr) in 
+        let equ := make (App constr:(@eq) arr) in 
         let idH := Fresh.in_goal @H in 
         let h := Control.hyp hyp in 
-        assert (idH : $trm) by ltac1:(h |- rewrite h ; reflexivity) (Ltac1.of_constr h) ; eapply &idH 
-    | (opt, c) :: binds => 
+        assert (idH : $equ) by (rewrite $h; reflexivity) ; eapply &idH 
+    | (opt, a) :: binds => 
         let id := fresh_ident_of_option opt in 
         let newbinds := List.map (fun (x, y) => (x, substnl [make (Var id)] 0 y)) binds in
         let proof := 
-          in_context id c (gen_eq hyp newbinds (substnl [make (Var id)] (List.length binds) b) f g ((Var id) :: l)) in
+          in_context id a (gen_eq hyp newbinds (substnl [make (Var id)] (List.length binds) b) f g ((Var id) :: l)) in
         let id :=  Fresh.in_goal @H in assert ($id := $proof) ; ltac1:(proof |- try (exact proof)) (Ltac1.of_constr proof)
       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, and the last thing to do is to clear the previous
+hypothesis which is presumed to be not useful anymore *)  
+
 Ltac2 eliminate_ho_eq (h : ident) :=
   let t := Control.hyp h in
   match! type t with
@@ -47,6 +130,9 @@ Ltac2 eliminate_ho_eq (h : ident) :=
         ltac1:(H |- clear H) (Ltac1.of_constr t)
   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 
@@ -57,7 +143,7 @@ Tactic Notation "eliminate_ho_eq" ident(H) :=
 
 Section tests.
 
-Set Default Proof Mode "Classic".
+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. 

From bb2cb4f3c04e38801939e5e02860da24024da035 Mon Sep 17 00:00:00 2001
From: lduboisd <louise.dubois-de-prisque@inria.fr>
Date: Tue, 5 Dec 2023 17:50:45 +0100
Subject: [PATCH 7/9] temporary elpi version without clear and improving
 application

---
 ho_equalities/elpi/tmp.v | 67 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 67 insertions(+)
 create mode 100644 ho_equalities/elpi/tmp.v

diff --git a/ho_equalities/elpi/tmp.v b/ho_equalities/elpi/tmp.v
new file mode 100644
index 0000000..7c02c34
--- /dev/null
+++ b/ho_equalities/elpi/tmp.v
@@ -0,0 +1,67 @@
+From elpi Require Import elpi.
+
+Ltac myassert u :=
+  let H := fresh in assert (H := u); simpl in H.
+
+Elpi Tactic eliminate_ho_eq.
+
+Elpi Accumulate lp:{{
+
+  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 }}.
+
+  solve ((goal _ _ _ _ [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,
+     coq.ltac.call "myassert" [trm R1] Goal NewGoals].
+
+
+}}.
+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); clear 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.
+
+
+
+
+
+
+

From b624954111bd653c5da9c3302d4f75c524b18ecf Mon Sep 17 00:00:00 2001
From: lduboisd <louise.dubois-de-prisque@inria.fr>
Date: Wed, 6 Dec 2023 08:18:54 +0100
Subject: [PATCH 8/9] taking remarks into account but keeping the clear in elpi

---
 ho_equalities/elpi/ho_equalities.v | 68 ++++++++++++------------------
 ho_equalities/elpi/tmp.v           | 67 -----------------------------
 2 files changed, 28 insertions(+), 107 deletions(-)
 delete mode 100644 ho_equalities/elpi/tmp.v

diff --git a/ho_equalities/elpi/ho_equalities.v b/ho_equalities/elpi/ho_equalities.v
index f0daf18..29b1998 100644
--- a/ho_equalities/elpi/ho_equalities.v
+++ b/ho_equalities/elpi/ho_equalities.v
@@ -20,7 +20,7 @@ Another method would have been to generate the hypothesis to prove and use a sma
 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. 
+to prove them, or provide the proof term directly. 
 
 *)
 
@@ -33,20 +33,16 @@ Ltac myassert u :=
 Ltac myclear H := clear H.
 
 
-(** All elpi tactics start with these two vernacular commands: [Elpi tactic toto.] followed 
+(** 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.
-For instance, [get-head T T'] takes a term [T] as input and returns a term [T'] (the same one if it is not 
-an application, and its head otherwise)
 
 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. 
-Thus, [get-head (app [F|_]) R :- get-head F R] means that the output [R] is the head of the application of [F]
-to any arguments (so we use a wildcard) only if it is also the head of [F].
 
 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). 
@@ -54,10 +50,10 @@ 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. In the code, you will see 
-an example: [{{ @eq }}], which is simply turning the Coq term for propositional equality
-into its elpi quotation. You can also use elpi antiquotation, for inserting elpi variables 
-into a Coq term, but we won't need this here.
+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 
@@ -68,20 +64,17 @@ and [names L] which has as only argument [L] the list of all the eigenvariables
 
 Elpi has two kinds of variables: unification variables (also called "metavariables"), 
 used to resolve the clauses which
-define elpi predicates and written with capital letters, and eigenvariables written is small letter
+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 %
 
-  pred get-head i:term o:term. % [i:] means input and [o:] means output
-    get-head (app [F|_]) R :- get-head F R.
-    get-head T T.
-
   % 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.
@@ -105,27 +98,26 @@ Elpi Accumulate lp:{{
       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]), and their type.
-  % The first rule is the recursive case: we suppose that the functions given as 
-  % inputs are only partially applied (or not applied at all).
+  % 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 apply the functions and the resulting 
+  % 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 managed to find the exact form of the proof term by some trials and errors using Ltac's [refine].
-  % Instead of focusing of its hardly readable form, I suggest that you look at the use of elpi's predicates
-  % [names] and [occurs]. We needed to apply the function variable [y] on the correct arguments.
-  % To find them, we looked at all the eigenvariables of our program by using [names L], and then filter these to keep 
-  % only the ones in [T1] (remember that [T1] is precisely f x1 ... xn).
+  % 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, o: term.
-    mk-proof-eq H T1 T2 (prod Na Ty F1) (fun Na Ty F2) :- 
-      pi x\ decl x Na Ty => mk-proof-eq H (app [T1, x]) (app [T2, x]) (F1 x) (F2 x).
-    mk-proof-eq H T1 T2 Codom
-      (app [{{@eq_ind_r}}, Ty', T2', (fun _ Ty' (y\ (app [{{ @eq }} , Codom, app [y | L'], T2]))), app [{{@eq_refl}}, Ty, T2], T1', H]) :-
-      get-head T1 T1', get-head T2 T2', coq.typecheck T1 Ty ok, coq.typecheck T1' Ty' ok,  names L, std.filter L (x\ occurs x T1) L'.
+  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.
@@ -144,7 +136,8 @@ Elpi Accumulate lp:{{
 
     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
+     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]. 
@@ -157,16 +150,13 @@ Elpi Typecheck.
 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" constr(t) :=
+Tactic Notation "eliminate_ho_eq" hyp(t) :=
   elpi eliminate_ho_eq ltac_term:(t).
 
 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. 
+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 :=
@@ -180,9 +170,7 @@ fix add (n m : nat) {struct n} : nat :=
   | 0 => m
   | S p => S (add p m)
   end) by reflexivity. eliminate_ho_eq H1.
-generalize Heq. intro Heq'. (* here, we have to generalize the section variable, as section variables do not appear 
-in the reified context of a Coq Goal in elpi. Otherwise, the call to clear will fail *)
-eliminate_ho_eq Heq'. 
+eliminate_ho_eq Heq. 
 Abort.
 
 End Tests.
\ No newline at end of file
diff --git a/ho_equalities/elpi/tmp.v b/ho_equalities/elpi/tmp.v
deleted file mode 100644
index 7c02c34..0000000
--- a/ho_equalities/elpi/tmp.v
+++ /dev/null
@@ -1,67 +0,0 @@
-From elpi Require Import elpi.
-
-Ltac myassert u :=
-  let H := fresh in assert (H := u); simpl in H.
-
-Elpi Tactic eliminate_ho_eq.
-
-Elpi Accumulate lp:{{
-
-  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 }}.
-
-  solve ((goal _ _ _ _ [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,
-     coq.ltac.call "myassert" [trm R1] Goal NewGoals].
-
-
-}}.
-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); clear 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.
-
-
-
-
-
-
-

From 5cecd23e4321aad3b1697753ffd93dbe10ee9f9e Mon Sep 17 00:00:00 2001
From: lduboisd <louise.dubois-de-prisque@inria.fr>
Date: Wed, 7 Feb 2024 20:27:02 +0100
Subject: [PATCH 9/9] change ho equalities Ltac2 (much more simple)

---
 ho_equalities/ltac2/ho_equalities.v | 114 +++++-----------------------
 1 file changed, 21 insertions(+), 93 deletions(-)

diff --git a/ho_equalities/ltac2/ho_equalities.v b/ho_equalities/ltac2/ho_equalities.v
index 44c914f..eac3290 100644
--- a/ho_equalities/ltac2/ho_equalities.v
+++ b/ho_equalities/ltac2/ho_equalities.v
@@ -19,97 +19,28 @@ of binders that are in scope between the variable [Rel n] and
 its corresponding binder.
 *)
 
-(** This auxilary function will help us to retrieve the type of the two equal functions.
-We split the product between each argument domain and the codomain. 
-The [Prod] constructor takes a binder (namely a name, a type and a relevance) 
-and a constr to make a new constr. The relevance is only useful when you work in SProp, 
-otherwise you will do fine by using the relevance Binder.Relevant *)
-
-Ltac2 split_prod (t : constr) :=
-  let rec aux t acc :=
-    match kind t with
-      | Prod bind t' =>
-          aux t' ((Binder.name bind, Binder.type bind) :: acc)
-      | _ => (acc, t)
-    end in aux t [].
-
-(** This function helps us to get a fresh ident starting from
-an ident option. Note that the annotation [@H] 
-(or [ident:(H)] as a shorthand) allows to quote [H] as an ident in Ltac2.
-Fresh.free_of_ids generates the list of the free variables in an ident, 
-and Fresh.fresh generates an ident starting to a given one ([@H])
-which does not belong to a set of free variables (here, [frees]). *)
- 
-
-Ltac2 fresh_ident_of_option (opt : ident option) :=
-  match opt with
-    | None =>
-        let frees := Fresh.Free.of_ids [@H] in
-        Fresh.fresh frees @H
-    | Some id => id
-  end.
-
-(** The main function [gen_eq] takes an ident [hyp] which is the one of the premise [f = g], 
-a list of binders (the name and the type of the arguments of the functions), the codomain [b],
-[f] and [g] our functions, and a list of kind [l] (the variables [x1 ... xn] which we will 
-introduce one by one). It also expects a term of type unit because this function is in fact a thunk, 
-evaluated only for its side effects on the proof state. 
+(** 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].
-We build the desired equality [equ] and we assert it. 
-We designate this hypothesis of type [equ] by a new ident [idH].
-The proof of [equ] is made by a small Ltac2 script: [rewrite $h; reflexivity].
-Here, we use [$h] because [rewrite] takes a Coq term. Thus, [$] performs 
-an antiquotation from the constr of Ltac2 to the underlying Coq term.
-
-The last tactic of the base case, [eapply &idH], will become clearer once we looked at the recursive
-case. It is here because when we reach the base case, we are not in the main goal. The goal here is 
-just a metavariable of any type. So we should then precise our goal, and thus we say that it is [&idH],
-the Coq term designated by the ident [idH], which is of type [trm].
-
-In the recursive case, we introduce a new constr which is a named variable: [make (Var id)], of type [a].
-Consequently, we should substitute the De Brujin index 0 contained in [f], in [g], in [b] and in the 
-type of the other binders by [make (Var id)]. 
-We cannot work directly on De Brujin indexes because each time we call the function [make]
-to build a constr from a kind, [make] will perform a type-checking. So if a term contains free variables, 
-the type-checking will fail, producing a fatal error. 
-In my opinion, this leads to a lot of difficulties, making Ltac2 a language 
-that I do NOT recommend to use for working with De Brujin indexes. But still, we will 
-find a solution in this tutorial.
-
-The trick is to use [in_context id c tac], which runs a tactic [tac] on a new goal (a metavariable of any type),
-keeping the same hypotheses as the previous goal, but with a new hypothesis id : c, and returns the term
-[fun (id : c) => t], where [t] is a proof of the new arbitrary goal.
-This explains the line [let proof := in_context ... ]. We can retrieve the proof [t] of [f x1 ... xn = g xn ... xn], 
-created in a context in which [x1 ... xn] are bound, and abstrating it to [fun x1 ... xn => t]. 
-In order to keep this proof in each recursive call (where the goal is also a metavariable [?Goal]), we
-prove [?Goal] by [exact proof]. Here, we used Ltac1 inside ltac2, to show the syntax to call Ltac1 tactics.
-We write [ltac1:(tac)] for tactics taking no arguments, and [ltac1:(arg1 ... argn |- tac)]
-otherwise. In the second case, the arguments should be of type Ltac1.t, so we perform some casts.
-Indeed, our function uses [Ltac1.of_constr].
 
- *)
+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 (hyp: ident) (binds :(ident option * constr) list) (b: constr) (f : constr) (g : constr) (l: kind list) () :=
-  match binds with
-    | [] =>
-        let rels := Array.of_list (List.rev (List.map make l)) in
-        let f := make (App f rels) in 
-        let g := make (App g rels) in
-        let arr := Array.of_list [b; f; g] in 
-        let equ := make (App constr:(@eq) arr) in 
-        let idH := Fresh.in_goal @H in 
-        let h := Control.hyp hyp in 
-        assert (idH : $equ) by (rewrite $h; reflexivity) ; eapply &idH 
-    | (opt, a) :: binds => 
-        let id := fresh_ident_of_option opt in 
-        let newbinds := List.map (fun (x, y) => (x, substnl [make (Var id)] 0 y)) binds in
-        let proof := 
-          in_context id a (gen_eq hyp newbinds (substnl [make (Var id)] (List.length binds) b) f g ((Var id) :: l)) in
-        let id :=  Fresh.in_goal @H in assert ($id := $proof) ; ltac1:(proof |- try (exact proof)) (Ltac1.of_constr proof)
-      end.
+ *)
+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.
@@ -118,16 +49,13 @@ 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, and the last thing to do is to clear the previous
-hypothesis which is presumed to be not useful anymore *)  
+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 (l, b) := split_prod a in
-        gen_eq h (List.rev l) b f g [] () ;
-        ltac1:(H |- clear H) (Ltac1.of_constr t)
+    | @eq ?a ?f ?g =>
+        let c := gen_eq f g a [] in assert $c 
   end.
 
 (** Tactic Notation is useful to transform Ltac2 functions
@@ -153,13 +81,13 @@ fix length (l : list A) : nat :=
   match l with
   | nil => 0
   | (_ :: l')%list => S (length l')
-  end) by reflexivity. eliminate_ho_eq H.  
+  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.
+  end) by reflexivity. eliminate_ho_eq H1. 
 eliminate_ho_eq Heq.
 Abort.