add tactic set

[fblanqui]

TODO:

• [x] 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?