The Coq mailing list

[Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>]

4) Isn't that just [simple induction]?

eg


Variable P : nat -> Prop.

Goal forall n, P n.
simple induction 0.
- (* n : nat |- P 0 *) admit.
- (* n : nat |- forall n0 : nat, P n0 -> P (S n0) *) admit.
Abort.


Gaëtan Gilbert

On 18/09/2016 13:32, Sebastian Böhne wrote:
> Thank you Gaëtan Gilbert and Clément Pit--Claudel for your answers! 
> They already helped a lot!
>
> 1) The suggestion to use tactic notations for writing tactic_example H 
> in H' instead of tactic_example_in H H' indeed works. Yet, there were 
> to thinks to consider:
> a) I first tried:
> Tactic Notation "my_tactic" hyp(H) "in" hyp(H') := my_tactic_in H H'.
> This was problematic since I sometimes want to use the tactic with a 
> lemma for H. This is why I had to use
> Tactic Notation "my_tactic" constr(H) "in" hyp(H') := my_tactic_in H 
> H' instead.
> b) A second problem was that with this notation I was not allowed to 
> use my tactic my_tactic anymore. I solved the problem by renaming the 
> original my_tactic in my_tactic_not_in and making a second tactic 
> notation, namely
> Tactic Notation "my_tactic" constr(H) := my_tactic_not_in H.
> This does not seem to clash with the former tactic notation.
>
> 2) unfold "sign" does indeed work. For some reasons I thought I had 
> tried this, but I was wrong.
>
> 3) Tim Richter, a colleague of mine, helped me with the third point. 
> We were partially successful: We wanted a tactic
> my_tactic H X1 ... Xn (where n = 0 is possible).
> Instead we were able to make a tactic, called
> my_tactic' H X1 ... Xn False
> instead, which behaved like my_tactic H X1 ... Xn should (False could 
> be replaced by something else. It is only a dummy). However,
> my_tactic H L := my_tactic' H L False
> does not work, except with exactly one argument. We tried
> Tactic Notation "my_tactic" constr(H) ident_list(L) := my_tactic' H X1 
> ... Xn False,
> but this does not work neither: Coq exspects a "." after my_tactic H, 
> so for instance my_tactic H X1 X2 X3 does not work. Furthermore 
> my_tactic H produces another error, which might be special to our tactic:
> "Must evaluate to a closed term
> offending expression:
> t
> this is a VList."
>
> Does somebody have an idea how to go from my_tactic' to my_tactic?
>
> 4) My fourth question was not answered yet; perhaps due to the other 
> questions. So I repeat it.
>
> I would like to build an induction-tactic which behaves a little bit 
> different than the original one: It should only match with the current 
> goal and should not be the induction of one of the hypotheses. So far 
> I know how to do it. Another thing is, however, that when applied the 
> original induction tactic makes some intros automatically. For 
> instance when using induction for nat, one subgoal is P(0) (which is 
> ok), while the other is P(Suc n) where n : nat and P(n) are already 
> assumed. I would prefer if it would be simply ∀ n : nat, P n → P (Suc 
> n) as goal instead.
>
> It is no problem to create such a tactic for special cases (like nat), 
> but I would like a tactic as general as the orginal one. The problem 
> seems to me to be that I somehow had to use ind_A for the different 
> inductive types A. Yet ind A or something like that does not work 
> since ind is not a total function and I don't know how to refer to it 
> otherwise.
>
> Another attempt would be to use induction and to regeneralise the 
> hypotheses, but then I need the names and the number of the hypotheses 
> for reconstruction. This in turn seems to me to amount to the same 
> problem of having to know ind_A.
>
> Thank you and best regards
>
> Sebastian Böhne