Allow rewrite tactic on hypotheses

[QGarchery]

Rewriting on an hypothesis that is defined earlier than the equality to rewrite is cumbersome.

require open Stdlib.Set Stdlib.Prop Stdlib.Eq Stdlib.Nat;

symbol test_rew_hyp (a b : ℕ) f : π (f a) → π (a = b) → π (f b)
≔ begin
  assume a b f fa eab;

  // I want to rewrite eab in fa

  // The following attempt does not work since eab is also put in the goal:
  // generalize fa; rewrite eab;

  // Instead, we have to do:
  have fa_fb : π (f a ⇒ f b);
  rewrite eab; refine (λ x, x);
  refine fa_fb fa;
end;

Feature wish: allow to directly rewrite on any hypothesis (for example with the syntax rewrite eab in fa;) and/or make generalize more precise by not also generalizing independent following hypotheses.

[fblanqui]

Now, for your example, you can also simply do:

  assume a b f fa ab; rewrite left ab; apply fa;

But I agree that it could sometimes be useful to be able to rewrite in an assumption. If the equation is before the assumption, this can be done as follows:

// assume that your goal is: ..., e: l = r, x1:A1, .., xm:Am, h: A, y1:B1, .., yn:Bn ⊢?:C
// rewrite e in h can be simulated as follows:
generalize h; rewrite e; assume h y1 .. yn

Otherwise, we need to permute them (this is possible only if e does not depend on h). This can be done as follows:

// assume that your goal is: ..., h:A, x1:A1, .., xm:Am, e: l = r, y1:B1, .., yn:Bn ⊢?:C
have lem: Π (x1:A1) .. (xm:Am) (e:l = r) (h:A) (y1:B1) .. (yn:Bn), C;
  // proof of lem:
  assume x1 .. xm e h y1 .. yn; ...
// proof of C using lem:
apply lem x1 .. xm e h y1 .. yn;

This can be avoided by changing the order of propositions in the initial statement but this may be inconvenient in some cases.

[NotBad4U]

Hi everyone,

I am also highly interested in this feature. In my case, I am working on the reconstruction of proofs obligation generated by the SMT veriT in LambdaPi (maybe something similar to the verine project). Proof made by SMT solvers like veriT are made in a forward reasoning. What I mean by forward reasoning is it starts from what is given (premises, previously proven theorems) and iteratively draws conclusions from them until the goal is reached. In this way, we often rewrite and play with hypotheses in the context. For now, I bypass this with the same method of @QGarchery, I create a new goal with have tactic that represents my hypothesis rewrited, and proved it by applying a lemma.

So I think it could be interesting to have the possibility to

• Rewrite in hypotheses rewrite ... in ...;
• apply on a hypothesis apply ... in ...;
• simplify hypothesis simplify in H;

[fblanqui]

Thank you for your comment. Yes, it would be great to add this feature. As explained before, for rewrite and simplify, it could be implemented by using current tactics, possibly by adding a permutation tactic. For apply-in, we should first clarify the semantics. Concerning your project, I would be happy to know more. Please, send me a mail.