The Coq mailing list

[Nathanaël Courant <nathanael.courant AT ens.fr>]

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