The Coq mailing list

[Li-yao Xia <lysxia AT gmail.com>]

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