## Stream: Coq users

### Topic: Failure of the tactic inductive ... using

#### Dominique Larchey-Wendling (Oct 19 2022 at 10:21):

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'.
``````

#### Dominique Larchey-Wendling (Oct 19 2022 at 13:13):

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.

#### Pierre Castéran (Oct 19 2022 at 14:22):

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!

#### Dominique Larchey-Wendling (Oct 19 2022 at 14:35):

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.

#### Pierre Castéran (Oct 19 2022 at 15:32):

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:

#### Paolo Giarrusso (Oct 19 2022 at 17:19):

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

#### Paolo Giarrusso (Oct 19 2022 at 17:19):

if the old name remains around (possibly deprecated), migration should be easy.
Of course, if somebody volunteers to write the patch.

#### Pierre Castéran (Oct 19 2022 at 19:10):

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`.

#### Dominique Larchey-Wendling (Oct 19 2022 at 19:35):

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.

#### Dominique Larchey-Wendling (Oct 19 2022 at 19:37):

Btw, the initial code snippet uses `apply ... with ...` after the `Fail induction ...`tactic.

#### Dominique Larchey-Wendling (Oct 19 2022 at 19:41):

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.

#### Paolo Giarrusso (Oct 19 2022 at 20:04):

@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.

#### Paolo Giarrusso (Oct 19 2022 at 20:09):

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?

#### Paolo Giarrusso (Oct 19 2022 at 20:26):

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`.

#### Dominique Larchey-Wendling (Oct 20 2022 at 06:25):

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.
``````

#### Dominique Larchey-Wendling (Oct 20 2022 at 06:27):

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.

#### Pierre Courtieu (Oct 22 2022 at 10:10):

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).

#### Meven Lennon-Bertrand (Oct 24 2022 at 12:25):

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`

#### Pierre Courtieu (Oct 25 2022 at 17:37):

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)
^^        ^^^^^^^^^^^^^^^^^^^^^^^^
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...).
``````

#### Pierre Courtieu (Oct 25 2022 at 17:39):

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

#### Meven Lennon-Bertrand (Oct 26 2022 at 09:18):

Indeed, formalizing this in the documentation (probably that of the `induction` tactic) would be very useful!

Last updated: Oct 03 2023 at 02:34 UTC