add tactic set - Githubissues

fblanqui commented 5 months ago

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 commented 5 months ago

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

NotBad4U commented 5 months ago

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 commented 5 months ago

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

Deducteam / lambdapi

add tactic set #1101