The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

> One possibility would be to create a custom induction principle, but
> since red is very complicated, this would amount to duplicate a lot of
> code, which I would rather avoid.

Would it be OK to define only a custom *inductive* and let coq build
the principle for you?

If you define an inductive (redP x) that has the same constructors
than red but with extra hypothesis saying that P is true for each
values you need in each case.

Then prove (rec x -> P x -> redP x) once.

Then use the principle of redP in your proof(s).

Best,
Pierre

Le jeu. 27 août 2020 à 16:18, Nathanaël Courant
<nathanael.courant AT ens.fr> a écrit :
>
> Hi,
>
> Thanks a lot of the idea! However, while this would be a possibility
> when proving this specific case, it only allows to use one such
> additional property P : X -> A -> Prop. I'd like to be able to use
> different properties as well, possibly with different types, such as Q :
> X -> B -> Prop.
> I was thinking about making A polymorphic in that case, and adding
> another parameter to be the function used to determine the values of
> type A used in the recursive calls, but it seems to be too clumsy and to
> pollute the definition with a lot of added complexity.
>
> Cheers,
> Nathanaël
>
> On 8/27/20 3:26 PM, Li-yao Xia wrote:
> > Hi Nathanaël,
> >
> > One idea is to generalize the open recursion so the recursive predicate
> > takes an A parameter:
> >
> > Inductive red_ (rec : X -> A -> Prop) : X -> Prop.
> >
> > Would there be any problem doing that?
> >
> > Cheers,
> > Li-yao
> >
> >
> > On 8/27/2020 6:13 AM, Nathanaël Courant wrote:
> >> Hi all,
> >>
> >> I have a complicated inductive proposition:
> >>
> >> Inductive red: X -> Prop :=
> >> | case_1 : ...
> >> ...
> >> | case_N : ...
> >>
> >>
> >> I also have some proposition P : X -> Prop.
> >> I have goals of the form:
> >>
> >> forall x, red x -> P x -> Q x.
> >>
> >> which I prove by induction on red x. I can prove that if red x and P
> >> x, then P y is true for all y appearing as recursive calls to red in
> >> the constructor of red x.
> >>
> >> However, each time I want to prove such a result, I have to prove P is
> >> true for each of the recursive calls, and I want to avoid such code
> >> duplication.
> >>
> >>
> >>
> >> One possibility would be to create a custom induction principle, but
> >> since red is very complicated, this would amount to duplicate a lot of
> >> code, which I would rather avoid.
> >>
> >>
> >>
> >> Another possibility I tried was to switch to open recursion:
> >>
> >> Inductive red_ (rec : X -> Prop) : X -> Prop :=
> >> ...
> >> Inductive red := red_intro : forall x, red_ red x -> red x.
> >>
> >> Then I proved:
> >>
> >> forall H x, red_ (fun x => red x /\ H x) x -> P x ->
> >>              red_ (fun x => red x /\ H x /\ P x) x
> >>
> >> and
> >>
> >> forall x, red_ (fun x => red x /\ P x /\ Q x) x -> Q x
> >>
> >> which, combined, allow to prove forall x, red x -> P x -> Q x, and the
> >> deduplication of the work is done thanks to the first proof, which
> >> does not depend on Q.
> >>
> >>
> >> This works well on that simple case, however, the case I have is a bit
> >> more complicated: P is not of type X -> Prop, but of type X -> A ->
> >> Prop, for some other type A.
> >>
> >> I still have that if red x and P x a are true, then P y b are true for
> >> all y appearing as recursive calls to red in the constructor of red x
> >> (i.e. as calls to rec in red_ rec x), but it is for some b that
> >> depends on the recursive call and the constructor used.
> >> Thus, I can still prove the same thing as in the open recursion case,
> >> but with the proposition (fun x => exists a, P x a). However, I want
> >> to be able to use the correct value of a for the recursive calls in
> >> the second part of the proof when I want to prove Q, and I can't,
> >> because it is hidden away by the exists, since I have to prove:
> >>
> >> forall x, red_ (fun x => red x /\ (exists a, P x a) /\ Q x) x -> Q x.
> >>
> >>
> >>
> >> Finally, I tried to create a function to extract the values of a
> >> needed from the constructor used to prove red x, but I'm getting a
> >> universe inconsistency, since red is a Prop.
> >>
> >>
> >>
> >> Does anyone have an idea about how to extend recursion schemes for
> >> induction propositions, while proving some property is preserved as
> >> above, without getting a lot of code duplication in the way?
> >>
> >>
> >> Thanks,
> >> Nathanaël
> >