The Coq mailing list

[Eric Tanter <etanter AT dcc.uchile.cl>]

Note that I've just realized that the HTML page for Basics.v in SF:
http://www.cis.upenn.edu/~bcpierce/sf/Basics.html

defines plus within a Playground2 module in order to not mess up with the 
actual definition. 

But the file Basics.v that is distributed does not include these module 
declarations, so the definition of plus given there does interfere. 

At this point, I guess I'm interested in understanding why the definition of 
plus used in the code below does not work.

Thanks,

-- Éric


On Dec 25, 2010, at 11:47 PM, Eric Tanter wrote:

> Hi Evgeny,
> 
>> (Note that you can just say "rewrite H" instead of "rewrite -> H".) In
>> any case, your insight that one can do "rewrite H. apply Em." instead
>> of "rewrite <- H in Em. apply Em." is correct.
> 
> Thanks for confirming this! at least I'm not so confused ;)
> 
>> If you still have this problem, could you create a small standalone
>> file and post it? Also, what version of Coq do you have? If you can
>> use the command line and if you know where the program coqtop is, you
>> can type "coqtop --version" to find out the version.
> 
> I have found what seems to be the problem. The SF files do some imports, 
> which eventually import Basics.v. This file has a definition for plus/+ :
> 
> Fixpoint plus (n : nat) (m : nat) {struct n} : nat :=
>  match n with
>    | O => m
>    | S n' => S (plus n' m)
>  end.
> 
> Notation "x + y" := (plus x y)  (at level 50, left associativity).
> 
> Putting these definitions at the beginning of the following file:
> -----------------------
> (** imports, or definition of plus/+ **)
> 
> Inductive ev : nat -> Prop :=
>  | ev_0 : ev O
>  | ev_SS : forall n:nat, ev n -> ev (S (S n)).
> 
> Theorem ev_sum : forall n m,
>   ev n -> ev m -> ev (n+m).
> Proof.
>  intros n m En.
>  induction En as [|n' En'].
>  simpl. intro Em. apply Em.
>   intro Em. apply IHEn' in Em.
>   assert (H: S (S n') + m = S (S (n' + m))).
>   simpl. reflexivity.
>   apply ev_SS in Em.  
>   rewrite H.
> (* rewrite <- H in Em. *)
>   apply Em.
> Qed.
> -----------------------
> fails on the rewrite H with 
> "Error: Found no subterm matching "S (S n') + m" in the current goal."
> 
> If I remove the imports / remove the definition of plus/+, then it works!
> 
> So this seems to be a problem with the definition of plus/+. Any idea?
> 
> Thanks,
> 
> -- Éric
>