Dominique Larchey-Wendling (Oct 19 2022 at 10:21): 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'.
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 Ltacbut 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
Ltacbut 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 inductiontactic? 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
inductionhere, 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.
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)
^^ ^^^^^^^^^^^^^^^^^^^^^^^^
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.
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 13 2024 at 01:02 UTC