Merge pull request #746 from patrick-nicodemus/rewrite

Created rewrite tactic

apps/eltac/tests/test_rewrite.v

@@ -0,0 +1,44 @@
+From elpi.apps Require Import eltac.rewrite.
+
+Goal (forall x : nat, 1 + x = x + 1) -> 
+    forall y,  2 * ((y+y) + 1) = ((y + y)+1) * 2.
+Proof.
+    intro H. 
+    intro x.
+    eltac.rewrite H.
+    eltac.rewrite PeanoNat.Nat.mul_comm.
+    exact eq_refl.
+Defined.
+
+Section Example_rewrite.
+Variable A : Type.
+Variable B : A -> Type.
+Variable C : forall (a : A) (b : B a), Type.
+Variable add : forall {a : A} {b : B a}, C a b -> C a b -> C a b.
+Variable sym : forall {a : A} {b : B a} (c c' : C a b), add c c' = add c' c.
+
+Goal forall (a : A) (b : B a) (x y : C a b),
+    add x y = add y x /\ add x y = add y x.
+Proof.
+    intros a b x y.
+    eltac.rewrite @sym. (* @sym is a gref *)
+    (** [add y x = add y x /\ add y x = add y x] *)
+    easy.
+Defined.
+
+Goal forall (a : A) (b : B a) (x y : C a b),
+    add x y = add y x /\ add x y = add y x.
+Proof.
+    intros a b x y.
+    eltac.rewrite sym. (* because of implicit arguments, this is sym _ _, which is a term *)
+   easy.
+Defined.
+
+Goal forall n, 2 * n = n * 2.
+Proof.
+    intro n.
+    Fail eltac.rewrite PeanoNat.Nat.add_comm.
+    eltac.rewrite PeanoNat.Nat.add_comm "strong".
+    Abort.
+
+End Example_rewrite.

apps/eltac/theories/rewrite.v

@@ -0,0 +1,46 @@
+From elpi Require Export elpi.
+
+Elpi Tactic rewrite.
+Elpi Accumulate lp:{{
+    % Second argument is a type of the form forall x1 x2 x3... P = Q.
+    % First argument is a term of that type.
+    % This tactic finds a subterm of the goal that Q unifies with
+    % and rewrites all instances of that subterm from right to left.
+    pred rewrite i:list argument, i:term, i:term, o:goal, o:list sealed-goal.
+
+    % The copy predicate used below is discussed in the tutorial here:
+    % https://lpcic.github.io/coq-elpi/tutorial_coq_elpi_tactic.html#let-s-code-set-in-elpi
+
+    rewrite Strong Eqpf {{@eq lp:S lp:P lp:Q }} (goal _ _ GoalType _ _ as G) GL :- 
+    % First, introduce a rule that causes "copy" to act as a function
+    % sending a type T to the same type, but with all 
+    % subterms of T unifiable with Q to be replaced with a fresh constant x.
+        pi x\ 
+        (pi J\ copy J x :- Strong = [str "strong"| _], coq.unify-leq Q J ok) =>
+        (pi J\ copy J x :- [] = Strong, Q = J) =>
+        % Apply this copy function to the goal type.
+            (copy GoalType (A x),
+        % If the subterm Q did indeed appear in the goal,
+        % then pattern match on the given equality assumption P = Q,
+        % causing Q to be replaced with P everywhere.
+            if (occurs x (A x))
+            (refine (match
+                Eqpf {{ fun a (e : @eq lp:S lp:P a) => lp:(A a) }}
+                % We only want to create one hole,
+                % the one corresponding to the 
+                % contents of the (single) branch of the match.
+                [Hole_])
+                G GL 
+            )
+            (coq.ltac.fail _ "Couldn't unify")).
+
+    solve (goal _ _ _ _ [trm Eq | Strong] as G) GL :- 
+        coq.typecheck Eq Ty ok,
+        coq.saturate Ty Eq Eq',
+        coq.typecheck Eq' Ty' ok,
+        rewrite Strong Eq' Ty' G GL.
+}}.
+
+Tactic Notation "eltac.rewrite" ident(T) := elpi rewrite ltac_term:(T).
+Tactic Notation "eltac.rewrite" uconstr(T) := elpi rewrite ltac_term:(T).
+Tactic Notation "eltac.rewrite" uconstr(T) string(s) := elpi rewrite ltac_term:(T) ltac_string:(s).

apps/eltac/theories/tactics.v

@@ -1,5 +1,6 @@
 From elpi.apps.eltac Require Export
   intro
+  rewrite
   constructor
   assumption
   discriminate