The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

I assume, that there is no problem of implicit arguments, and that your problem is that you did not succeed in specifying which subterm is to be rewritten (you have 4 choices).

Solutions:
- «f_equal. (*or fequal, I do not remember the syntax*)
  apply H1. (*or «rewrite H1.», but direct appliance is more straightforward. *)»
- «rewrite (H1 c a). (* If you are lazy, partial appliance is enough with «rewrite (H1 c).» as there is no ambiguity anymore. *)»
- Import the Setoid module, and use «rewrite H1 at 2.»
- mask occurences manually:
  «set (tmp := s b). rewrite H1. subst tmp.», or
  «set (tmp := s) at 1 3 4. rewrite H1. subst tmp.»
and probably many other possibilities.

2014-07-30 10:30 GMT+02:00 coqcdp <coqcdpnxj AT 163.com>:

Hi,

       The context of my program  is 

                                          s:U->U->U.

                                          a:U.

                                          b:U.

                                          c:U.

                                        H0: forall a0 b0 c0:U,s (s a0 b0) c0=s a0 (s b0 c0).

                                       H1:forall a0 b0:U,s a0 b0 = s b0 a0.

                         _________________________________________________________________

                                             s b ( s c a) = s b ( s a c)

I want to use "rewrite H1" strategy to rewrite " s c a " to " s a c" ，but it doesn't work.  Could you tell me the reason and give me some proper suggestions?  Thank you very much.

 

Yours Sincerely ,

                             D.P.Chen.

--
.../Sedrikov\...