Changing type under lambda in Coq

I encountered a situation where setoid rewriting does not work because convertible types are not matched by the tactic. The workaround I came up with does not work under lambda. Looking for suggestions:

Require Import Setoid Morphisms Relations.

(* Sample definitions *)
Record S {i o: nat} : Type.
Definition C {i o: nat} (f: @S i o):  @S i o. Admitted.
Definition B {o:nat} (z:nat): @S (o+o) o. Admitted.

(* Relations *)
Parameter R: forall {i o}, relation (@S i o).
Instance R_proper {i o}: Proper (R ==> R ==> iff) (@R i o). Admitted.
Definition Rext {i o} := pointwise_relation nat (@R i o).

(* Sample rewriting lemma *)
Lemma Rewrite (x:nat): forall z, R (C (@B x z)) (B z). Admitted.

Ltac Type_Fix :=
  match goal with
  | [ |- context G [ (@C (Datatypes.S _) ?o (@B ?o ?z))] ] =>
    let G' := context G[(@C (o+o) o (@B o z))] in change G'
  end.

(* Simple case. Works with workaround *)
Theorem Foo (p:nat): R (@C 2 1 (@B 1 p)) (@C 2 1 (@B 1 p)).
Proof.
  Fail setoid_rewrite Rewrite.
  repeat Type_Fix.
  repeat setoid_rewrite Rewrite.
Admitted.

(* Now try under lambda. Does not work! *)
Theorem Bar (p:nat): Rext (fun z => @C 2 1 (@B 1 z)) (fun z => @C 2 1 (@B 1 z)).
Proof.
  Fail setoid_rewrite Rewrite.
  Fail Type_Fix.
Admitted.

In both Foo and Bar direct application of setoid_rewrite fails. The problem is that type of C (B p) is @S 2 1 while our rewriting lemma expects @C (1+1) 1. In Foo I was able to fix this via LTAC. However, this fix does not work under lambda in Bar.

Solution

Here are three solutions:

Flip the order of your arguments, to help setoid_rewrite pick up the right terms even though it's using left-to-right inference.

Your example becomes:

Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Relations.Relations.

(* Sample definitions *)
Record S {o i: nat} : Type.
Definition C {o i: nat} (f: @S o i):  @S o i. Admitted.
Definition B {o:nat} (z:nat): @S o (o+o). Admitted.

(* Relations *)
Parameter R: forall {o i}, relation (@S o i).
Definition Rext {o i} := pointwise_relation nat (@R o i).

(* Sample rewriting lemma *)
Lemma Rewrite (x:nat): forall z, R (C (@B x z)) (B z). Admitted.

Global Instance R_Proper {o i} : Proper (R ==> R ==> Basics.flip Basics.impl) (@R o i).
Proof.
Admitted.

(* Simple case. Works with workaround *)
Theorem Foo (p:nat): R (@C 1 2 (@B 1 p)) (@C 1 2 (@B 1 p)).
Proof.
  setoid_rewrite Rewrite.
Admitted.

Global Instance Rext_Proper {o i}
  : Proper
      ((pointwise_relation nat R)
         ==> (pointwise_relation nat R)
         ==> Basics.flip Basics.impl) (@Rext o i).
Proof.
Admitted.

(* Now try under lambda. Does not work! *)
Theorem Bar (p:nat): Rext (fun z => @C 1 2 (@B 1 z)) (fun z => @C 1 2 (@B 1 z)).
Proof.
  setoid_rewrite Rewrite.
Admitted.

Make Type_Fix smarter.

You could do this instead:

Ltac Type_Fix :=
  progress
    repeat match goal with
           | [ |- context G [@C _ ?o] ]
             => progress let G' := context G[@C (o+o) o] in change G'
           end.

This version only requires that the o argument to C not be a binder, and allows the f argument to be a binder. I've replaced Datatypes.S _ with _ and used progress to ensure that we find places where it makes sense to change; this makes the tactic more general and allows it to fix other representations as well (for example, @C 0 0).

Use match to fill in the relevant argument to Rewrite.

You could replace setoid_rewrite Rewrite with something like

  match goal with
  | [ |- context[C (@B ?x _)] ]
    => setoid_rewrite (Rewrite x)
  end.