Hi Coq tactic devs,

I would like to use a induction principle called `clos_refl_trans_ind_1n`

that works from the head `x`

a chain `clos_refl_trans _ R x z`

where the tail `z`

is *fixed*. So the idea would be to invoke the tactic `induction 1 as [ | ... ] using clos_refl_trans_ind_1n`

. While I can force the induction using a refined `apply clos_refl_trans_ind_1n`

tactic, the `induction`

tactic fails with the `Cannot recognize the conclusion of an induction scheme`

message.

However, the reverse principle that works from the tail with a fixed head is "compatible" with the `induction`

tactic. Any clue on modifying the shape of `clos_refl_trans_ind_1n`

so that `induction`

recognize an induction principle?

The below code example was tested on `Coq 8.15.2`

and `Coq 8.16.0`

. The critical point comes in the proof of `crt_crt_with_1n`

, line starting with `Fail`

.

Thx in advance for any hint,

Dominique

```
Require Import Relations.
#[local] Hint Constructors clos_refl_trans : core.
Section two_induction_principles.
Hint Resolve clos_rtn1_rt clos_rt1n_rt : core.
Variables (A : Type) (R : relation A).
Section clos_refl_trans_indn1.
Variables (x : _) (P : _ -> Prop)
(HP0 : P x)
(HP1 : forall y z, R y z -> clos_refl_trans _ R x y -> P y -> P z).
Lemma clos_refl_trans_ind_n1 z : clos_refl_trans _ R x z -> P z.
Proof.
intros H%clos_rt_rtn1.
induction H; eauto.
Qed.
End clos_refl_trans_indn1.
Section clos_refl_trans_ind1n.
Variable (z : A).
Inductive clos_refl_trans_1n' : _ -> Prop :=
| crt_1n'_stop : clos_refl_trans_1n' z
| crt_1n'_prev x y : R x y -> clos_refl_trans_1n' y -> clos_refl_trans_1n' x.
Variables (P : _ -> Prop)
(HP0 : P z)
(HP1 : forall x y, R x y -> clos_refl_trans _ R y z -> P y -> P x).
Lemma clos_refl_trans_ind_1n x : clos_refl_trans _ R x z -> P x.
Proof.
intros H%clos_rt_rt1n.
induction H; eauto.
Qed.
End clos_refl_trans_ind1n.
End two_induction_principles.
Fact crt_n1_crt X R x z : clos_refl_trans_n1 _ R x z -> clos_refl_trans X R x z.
Proof.
induction 1 as [ | y z Hyz H IH ].
+ constructor 2.
+ constructor 3 with (1 := IH); now constructor 1.
Qed.
Fact crt_crt_with_n1 X R x z : clos_refl_trans _ R x z -> clos_refl_trans X R x z.
Proof.
induction 1 as [ | y z Hyz H IH ] using clos_refl_trans_ind_n1.
all: eauto.
Qed.
Fact crt_1n'_crt X R x z : clos_refl_trans_1n' _ R z x -> clos_refl_trans X R x z.
Proof.
induction 1 as [ | x y Hxy H IH ].
all: eauto.
Qed.
Fact crt_crt_with_1n X R x z : clos_refl_trans _ R x z -> clos_refl_trans X R x z.
Proof.
Fail induction 1 as [ | x y Hxy H IH ] using clos_refl_trans_ind_1n.
revert x; apply clos_refl_trans_ind_1n with (P := fun x => clos_refl_trans X R x z);
[ | intros x y Hxy H IH ].
all: eauto.
Qed.
Check clos_refl_trans_n1_ind.
Print Implicit clos_refl_trans_n1_ind.
Check clos_refl_trans_ind_n1.
Print Implicit clos_refl_trans_ind_n1.
Check clos_refl_trans_1n'_ind.
Print Implicit clos_refl_trans_1n'_ind.
Check clos_refl_trans_ind_1n.
Print Implicit clos_refl_trans_ind_1n.
Print clos_refl_trans_n1.
Print clos_refl_trans_1n'.
```

Let me complete my own question. The problem seems to be related to the *order* in which arguments appear. I mean if one defines

```
Definition crt_rev {X} (R : X -> X -> Prop) := (fun x y => clos_refl_trans _ R y x).
```

and uses `crt_rev _ R y x`

in place of `clos_refl_trans _ R x y`

in the statement of `clos_refl_trans_ind_1n`

, then the `induction`

tactic works.

Hi, @Dominique Larchey-Wendling ,

I noticed the same problems with the induction schemes in `Relations/Operators_Properties`

, e.g. `clos_refl_trans_ind_left`

.

I ended with rewriting equivalences like `clos_rt_rt1n_iff`

, but if we can improve the shape of these induction lemmas, it would be nice!

Hi @Pierre Castéran ,

Actually it seems that the term of the StdLib `Relations/Operators_Properties`

corresponding to `clos_refl_trans_ind_1n`

is `clos_refl_trans_ind_right`

except that `z`

comes before `P`

. I wanted to mimic the induction principle as generated by the inductive definition `clos_refl_trans_1n'`

above. But apparently you ran into similar issues.

To me, the advantage of tailored induction principle is that you do not need to rewrite before `induction`

, and then possibly after applying the induction hypotheses.

I'm not an expert in `Ltac`

but just applying the induction principles seems to work?

```
Ltac rt_left_ind H :=
match goal with H : clos_refl_trans ?A ?R ?x ?z |- ?P ?z =>
apply (@clos_refl_trans_ind_left A R x P )
end.
Ltac rt_right_ind H :=
match goal with H : clos_refl_trans ?A ?R ?x ?z |- ?P ?x =>
apply (@clos_refl_trans_ind_right A R P z )
end.
Hint Constructors clos_refl_trans.
Fact crt_crt_l X R x z :
clos_refl_trans _ R x z -> clos_refl_trans X R x z.
Proof.
intro H; rt_left_ind H; eauto.
Qed.
Fact crt_crt_with_r X R x z :
clos_refl_trans _ R x z -> clos_refl_trans X R x z.
Proof.
intro H. pattern x; rt_right_ind H; eauto.
Qed.
```

Note: I couldn't avoid the `pattern x`

in the last example :thinking:

even if that ltac successfully reimplements (parts of) `induction`

, it might be nice to migrate the stdlib to the arg. order understood by the actual tactic

if the old name remains around (possibly deprecated), migration should be easy.

Of course, if somebody volunteers to write the patch.

Indeed, in order to avoid the `pattern`

, we may add the following induction principle:

```
Lemma clos_refl_trans_ind_right2 (A:Type)(R: relation A)
(P: A -> A -> Prop)
(z:A):
(P z z) ->
(forall x y : A, R x y -> P y z-> clos_refl_trans A R y z -> P x z)
->
forall x : A, clos_refl_trans A R x z -> P x z.
```

```
Ltac rt_right_ind2 H :=
match goal with H : clos_refl_trans ?A ?R ?x ?z |- ?P ?x ?z=>
apply (@clos_refl_trans_ind_right2 A R P z )
end.
Fact crt_crt_r X R x z :
clos_refl_trans _ R x z -> clos_refl_trans X R x z.
Proof.
intro H; eapply clos_refl_trans_ind_right2 with (R:=R); eauto.
Qed.
```

Of course, it remains to update the previous lemma in order to be used by `induction ... using`

.

Pierre Castéran said:

I'm not an expert in

`Ltac`

but just applying the induction principles seems to work?

Yes it does. But my point is, I want to use `induction ... using ...`

because intro patterns are better packed as `as [ | x y H IH ]`

than `apply ...; [ | intros x y H IH ]`

.

And this use case is the purpose of the induction tactic and recalls something to the reader about the nature of the proof argument.

Btw, the initial code snippet uses `apply ... with ...`

after the `Fail induction ...`

tactic.

Paolo Giarrusso said:

even if that ltac successfully reimplements (parts of)

`induction`

, it might be nice to migrate the stdlib to the arg. order understood by the actual tactic

So you can confirm that the failure lies in the management of the order of arguments in the actual implementation of the `induction`

tactic? That was my first impression but I was not sure. I have no experience in the OCaml internals of Ltac.

@Dominique Larchey-Wendling more precisely, I've already noticed that `induction`

demands a very specific argument order, and I use the same order in manual induction principles if possible; so I'd fix the stdlib statement.

oh... looking more closely, you ran into a different problem than what I've seen... but how would you enhance `induction`

here, on paper? Would you use higher-order unification?

I ask because the result of `induction`

seems much more predictable than, say, the result of `apply`

, and it'd be a bit unfortunate if generalizing `induction`

lost this property and/or changed the meaning of existing proofs. If I wanted to know the induction motive that `induction x`

will use, I just use `pattern x`

to rephrase my goal as `?motive x`

— even if the goal starts with premises or quantifiers that'd confuse `apply`

.

Paolo Giarrusso said:

oh... looking more closely, you ran into a different problem than what I've seen... but how would you enhance

`induction`

here, on paper? Would you use higher-order unification?

Well that I do not know. But here is stripped down illustration of the problem:

```
Require Import Relations.
#[local] Hint Constructors clos_refl_trans : core.
#[local] Hint Resolve clos_rt1n_rt : core.
(** The induction principle we want to use *)
Fact clos_refl_trans_ind_1n A (R : A -> A -> Prop) z (P : A -> Prop) :
P z
-> (forall x y, R x y -> clos_refl_trans A R y z -> P y -> P x)
-> forall x, clos_refl_trans _ R x z -> P x.
Proof. intros ? ? ? H%clos_rt_rt1n; induction H; eauto. Qed.
(** (crt_rev _ R) REVERSES the arguments of (clos_refl_trans _ R) *)
Definition crt_rev A (R : A -> A -> Prop) := (fun x y => clos_refl_trans _ R y x).
(** This is the SAME type as above and the SAME proof term *)
Fact crt_rev_ind :
forall A (R : A -> A -> Prop) z (P : A -> Prop),
P z
-> (forall x y, R x y -> crt_rev A R z y -> P y -> P x)
-> forall x, crt_rev _ R z x -> P x.
Proof. exact clos_refl_trans_ind_1n. Qed.
(** induction ... using clos_refl_trans_ind_1n FAILS but apply works of course *)
Fact crt_crt_with_1n A R x z : clos_refl_trans A R x z -> clos_refl_trans A R x z.
Proof.
Fail induction 1 as [ | x y Hxy H IH ] using clos_refl_trans_ind_1n.
revert x; apply clos_refl_trans_ind_1n with (P := fun x => clos_refl_trans _ R x z);
[ | intros x y Hxy H IH ].
all: eauto.
Qed.
(** induction ... using crt_rev_ind works as expected *)
Fact crt_rev_crt A R x z : crt_rev _ R z x -> clos_refl_trans A R x z.
Proof. induction 1 using crt_rev_ind; eauto. Qed.
```

Additionally, if we switch the order `P`

/`z`

in the principles `clos_refl_trans_ind_1n`

and `crt_rev_ind`

then the proof of `crt_rev_crt`

fails again.

Indeed the induction scheme recognition is quite rigid on parameter ordering. This is not ltac, it is done is ocaml (`tactics/tactics.ml`

around line `compute_scheme_signature`

). I wonder if making this verification less strict owuld break things (like intro patterns).

Is this recognition documented somewhere? Currently I often end up using `apply`

instead of induction with custom induction-like principles I defined myself, it would definitely be nice to be able to reliably predict how I should craft them to get support by `induction`

We should maybe formalize this in the documentation. Here is the central comment in the code:

```
The general form of an induction principle is the following:
forall prm1 prm2 ... prmp, (induction parameters)
forall Q1...,(Qi:Ti_1 -> Ti_2 ->...-> Ti_ni),...Qq, (predicates)
branch1, branch2, ... , branchr, (branches of the principle)
forall (x1:Ti_1) (x2:Ti_2) ... (xni:Ti_ni), (induction arguments)
(HI: I prm1..prmp x1...xni) (optional main induction arg)
-> (Qi x1...xni HI (f prm1...prmp x1...xni)).(conclusion)
^^ ^^^^^^^^^^^^^^^^^^^^^^^^
optional optional argument added if
even if HI principle generated by functional
present above induction, only if HI does not exist
[indarg] [farg]
HI is not present when the induction principle does not come directly from an
inductive type (like when it is generated by functional induction for
example). HI is present otherwise BUT may not appear in the conclusion
(dependent principle). HI and (f...) cannot be both present.
Principles taken from functional induction have the final (f...).
```

But there is no more precision about the ordering of variables.

Indeed, formalizing this in the documentation (probably that of the `induction`

tactic) would be very useful!

Last updated: Jan 28 2023 at 06:30 UTC