add tactic set

[fblanqui]

TODO:

• print definitions in lsp clients
• replace t by x in the current goal when doing set x := t
• extend tactic simplify to defined variables
• keep syntax set x := t ? (this makes "set" a keyword)
• define Pure.goal as type goal = (string * string * string option) list * conclusion ?

[fblanqui]

Hi @nicomarg @NotBad4U Could you please check your files with this PR to make sure that it doesn't break anything?

[NotBad4U]

I am not sure that the PR works correctly.
For example, if you change this Lemma in tests/OK/rewrite2.lp, it is impossible to unfold the definition of neither p or q.
Also, the reflexivity failed where normally the conversion rule should allow to prove this equality.

symbol test2' a b : π (f (a + b) (λ _, 0) = f (b + a) (λ _, 0))
≔ begin
  assume a b;
  simplify;
  set p ≔ (a + b);
  set g ≔ (a + b + 0 + 0);
  type p;
  have foo: π (p = g) {
    try simplify p;
    try simplify q;
    reflexivity;
  };
  rewrite add_com;
  reflexivity
end;

[fblanqui]

@NotBad4U @nicomarg I have fixed a number of things. Could you please check if it works with your own developments?

[NotBad4U]

I did some tests and it sounds to work well. I think we can merge the PR.
I think we will need to add a tactic similar to unfold/fold, rewrite -[term1]/term2 from SSreflect or change term1 with term2 of Coq.