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

[louiseddp]

The new tactic takes an hypothesis H : f = g, which f and g some functions, and generates and proves a new hypothesis H1 : forall x1 ... xn, f x1 ... xn = g x1 ... xn. The tactic is written in Ltac1, showing how to cross binders in this language, in Ltac2, tackling some issues about variables, and in coq-elpi, also showing how to combine tactics in this language. I tried to document everything as much as possible, but none of these implementations are trivial. I recommend using coq-8.17 to compile the files.

[gares]

Hi @louiseddp thanks for your PR!

I have a few comments on the elpi code:

• the tactic notation should take a hyp(t), since the entire code supposes so.
• clearing section variables in Coq is problematic, so I don't think the example should do so
• I think it would be simpler to do the clear in Coq, I mean elpi eliminate_ho_eq ltac_term:(t); clear t (also t is now a hyp so clear should be happy about it)
• calls like mk-proof-eq H (app [T1, x]) are OK-ish, but not perfect. All coq.* APIs tolerate "nested applications" but as you point out with your get-head, these terms are painful to work with. There are two ways:
  • the efficient one, which should speak to functional programmers, is to carry the head term and a list of arguments until the base case, then reverse the list and build the application
  • the easy one is to write mk-proof-eq H {coq.mk-app T1 [x]} which is not efficient since it flattens the app over and over, but looks simpler
• if you follow the first approach I suggest, then names and occurs are not needed since the base case receives as an argument exactly the list L' you build (in reverse order). Also T1 and T2 may use more proof variables other than the ones taken by the function, I guess, so I'm so sure your code is 100% correct.
• finally, you can call the type checker at the very end, and leave holes in the proof term

Let me sketch the code I propose:

  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 (app [T1, x]) (app [T2, x]) (F1 x) [x|Acc] (F2 x).
    mk-proof-eq H T1 T2 Codom Acc {{ @eq_ind_r _ lp:T2 lp:Predicate (eq_refl lp:T2Args) T1 H }} :-
      std.rev Acc Args,
      coq.mk-app T2 Args T2Args,
      Predicate = {{ fun y => lp:{{ app[ {{y}} | Args] }} = lp:T2Args }}.

or

  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 (app [T1, x]) (app [T2, x]) (F1 x) [x|Acc] (F2 x).
    mk-proof-eq H T1 T2 Codom Acc {{ @eq_ind_r _ lp:T2 (fun y => lp:(P y)) lp:Refl T1 H }} :-
      std.rev Acc Args,
      Refl = {{ eq_refl lp:{{ app [ T2 | Args ] }} }},
      pi y\
        P y = {{ lp:{{ app[ y | Args] }} = lp:{{ app[T2 | Args] }} }}.

and then

mk-proof-eq H T1 T2 Ty [] R1,
coq.typecheck R1 _ ok,

Hope it helps.

[louiseddp]

Hi @gares, thank you very much for you detailed answer ! I'll submit a new PR taking into account your remarks.

• It is indeed simpler to do the clear in Coq, but I thought it would be pedagogic to have an example chaining tactics directly in elpi, to illustrate how we can relate two goals. What do you think ?
• I like the functional programming version, thanks, I often forget to think "functional" when I use elpi while this way of programing still works even in logical programing.
• You said that T1 and T2 might mention other variables than the one taken by the functions, it's true if their head are defined locally, I should have removed their head. But in any case I used your version as the way of dealing with application is better.
• You're right it's more convenient to leave holes as it can be painful to build the proof manually

Thank you again for your help !