The Coq mailing list

[soham chakraborty <soham4you AT gmail.com>]

Thanks Valentin for the reference. Yes, these commands solve the problem and Raghu's solution works :)

One query. In theorem n + 0 = n is not accepted (guess it is due to recursion as Nick suggested earlier). But "simpl in IHp." allows "p + 0 = p". Any particular reason?

Best Regards,
soham

On Fri, Sep 6, 2013 at 3:39 PM, Valentin Robert <valentin.robert.42 AT gmail.com> wrote:

You should download the files here and work through them:
http://www.cis.upenn.edu/~bcpierce/sf/
(Download in the bottom-right corner, then open Induction.v)

In particular, to work with Raghu's code, you will need at least the
following commands upfront:

Require String. Open Scope string_scope.

Ltac move_to_top x :=
  match reverse goal with
  | H : _ |- _ => try move x after H
  end.

Tactic Notation "assert_eq" ident(x) constr(v) :=
  let H := fresh in
  assert (x = v) as H by reflexivity;
  clear H.

Tactic Notation "Case_aux" ident(x) constr(name) :=
  first [
    set (x := name); move_to_top x
  | assert_eq x name; move_to_top x
  | fail 1 "because we are working on a different case" ].

Tactic Notation "Case" constr(name) := Case_aux Case name.
Tactic Notation "SCase" constr(name) := Case_aux SCase name.
Tactic Notation "SSCase" constr(name) := Case_aux SSCase name.
Tactic Notation "SSSCase" constr(name) := Case_aux SSSCase name.
Tactic Notation "SSSSCase" constr(name) := Case_aux SSSSCase name.
Tactic Notation "SSSSSCase" constr(name) := Case_aux SSSSSCase name.
Tactic Notation "SSSSSSCase" constr(name) := Case_aux SSSSSSCase name.
Tactic Notation "SSSSSSSCase" constr(name) := Case_aux SSSSSSSCase name.

- Valentin

On Fri, Sep 6, 2013 at 10:53 AM, soham chakraborty <soham4you AT gmail.com> wrote:
> Hi Raghu,
>
> Good to hear from you. I have also started with the same book but yet to
> study the case analysis part :)
> On the solution you sent Coq is getting stuck at
>
> Case "n = O". Error: No interpretation for string "n = O".
>
> Can you please check.
>
> Best Regards,
> soham
>
>
> On Fri, Sep 6, 2013 at 1:39 PM, N. Raghavendra <raghu AT hri.res.in> wrote:
>>
>> At 2013-09-05T23:47:34+05:30, soham chakraborty wrote:
>>
>> > Using them I have found following ways to solve the theorem 1 * n =
>> > n. Please review and provide your feedback.
>>
>> I've also just begun to learn Coq.  This is an exercise in Pierce's
>> software foundations book:
>>
>> http://www.cis.upenn.edu/~bcpierce/sf/Induction.html
>>
>> At the level of that chapter, I'd solve this exercise as follows:
>>
>> Theorem mult_1_l :
>>   forall n : nat,
>>     1 * n = n.
>>
>> Proof.
>>   intros n.
>>   induction n as [ | p IHp].
>>   {
>>     Case "n = O".
>>     reflexivity.
>>   }
>>   {
>>     Case "n = S p".
>>     simpl.
>>     simpl in IHp.
>>     rewrite -> IHp.
>>     reflexivity.
>>   }
>> Qed.
>>
>> Best regards,
>> Raghu.
>>
>> --
>> N. Raghavendra <raghu AT hri.res.in>, http://www.retrotexts.net/
>> Harish-Chandra Research Institute, http://www.hri.res.in/
>>
>