Rewrite tactic fails to find term occurrence within pattern matching

Question

In Coq, I'm having problems with applying the rewrite tactic in the following situation:

Section Test.

Hypothesis s t        : nat -> nat.
Hypothesis s_ext_eq_t : forall (x : nat), s x = t x.

Definition dummy_s : nat -> nat :=
  fun n => match n with
         | O => 42
         | S np => s np
       end.

Definition dummy_t : nat -> nat :=
  fun n => match n with
         | O => 42
         | S np => t np
       end.

Goal forall (n : nat), dummy_s n = dummy_t n.
Proof.
  intro n. unfold dummy_s. unfold dummy_t.

At that stage, the local context and current goal look as follows:

1 subgoals, subgoal 1 (ID 6)

s : nat -> nat
t : nat -> nat
s_ext_eq_t : forall x : nat, s x = t x
n : nat
============================
match n with
| 0 => 42
| S np => s np
end = match n with
      | 0 => 42
      | S np => t np
      end

Now it should be possible to apply the rewrite tactic to replace the occurence of s np in the goal by t np, thereby making it possible to solve the goal using reflexivity. However,

rewrite s_ext_eq_t.

gives

Toplevel input, characters 0-18:
Error: Found no subterm matching "s ?190" in the current goal.

What am I doing wrong? One can get into a situation where rewrite is applicable via

 destruct n. 
   (* n = 0 *)
   reflexivity.
   (* n > 0 *)
   rewrite s_ext_eq_t.
   reflexivity.
 Qed.

but in the actual situation I am facing, several such destructs would be necessary, and I wonder whether rewrite or a variant of it is able to do this automatically.

---

Addendum The above situation naturally occurs when proving that a function defined via well-founded recursion has the desired fixed point property:

Suppose A: Type and that R: A -> A -> Prop is a well-founded relation, i.e. we have Rwf: well_founded R. Then, given a type family P: A -> Type we may construct a section

Fix : forall (x : A), P a

through recursion over R, with the recursion step given as a function

 F : forall x:A, (forall y:A, R y x -> P y) -> P x

See https://coq.inria.fr/library/Coq.Init.Wf.html However, to show that Fix indeed has the fixed point property

  forall (x : A), Fix x = F (fun (y:A) _ => Fix y)`

we need to provide a witness

  F_ext : forall (x:A) (f g:forall y:A, R y x -> P y),
             (forall (y:A) (p:R y x), f y p = g y p) -> F f = F g.

i.e. we have to show that F does not use anything else from the given f: forall y:A, R y x -> P y but its values. Of course, in any concrete situation, this should be trivial to verify, but when one tries to prove it, one runs into a situation a minimal example of which I have presented above: One is facing a huge equality of two copies of the code for the recursion step, one time with f and another time with g. Your assumption tells that f and g are extensionally equal, so one should be able to rewrite them. However, in the code for the recursion step, there might be a large number of pattern matchings and new variables that doesn't make sense in the local context, hence it would be (unnecessarily?) quite tedious to destruct dozens of times before being allowed to apply rewrite.

Answer 1

As mentioned in a comment above, it is not possible to perform the rewrite directly on the branch of the match statement, because np is not in scope in the top-level environment. As far as Coq's theory is concerned, a proof of your statement will have to destruct n at some point.

Although I am not aware of any tactics for automating this kind of problem, it is not too hard to come up with some custom ltac code for solving your problem without too much pain:

Ltac solve_eq :=
  try reflexivity;
  match goal with
  | |- match ?x with _ => _ end
       = match ?x with _ => _ end =>
    destruct x; auto
  end.

Goal forall (n : nat), dummy_s n = dummy_t n.
Proof.
  intro n. unfold dummy_s. unfold dummy_t.
  solve_eq.
Qed.

If your extensional equality results are hypotheses that appear in your context, then solve_eq should be able to solve many goals of this shape; if not, you might have to add extra lemmas to your hint database.