The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Hi again,

This is what to expect as the most general induction principle from the mutual
fixpoint. Hope this helps,

D.

--------

Section foo_rec_mutual_rect.

  Variable (foo_pre foo_post bar_pre bar_post : Higher -> Type).

  Hypothesis F01 : forall f, (forall x, foo_post (f x)) -> foo_post (Ctor 
(fun x => f x)).
  Hypothesis F02 : forall f, foo_pre (Ctor f) -> forall x, foo_pre (f x).
  
  Hypothesis F11 : forall x, bar_post x -> foo_post (Rec x).
  Hypothesis F12 : forall x, foo_pre (Neg x) -> bar_pre x.

  Hypothesis F21 : forall x, foo_post x -> foo_post (Rec x).
  Hypothesis F22 : forall x, foo_pre (Rec x) -> foo_pre x.

  Hypothesis B01 : forall f, (forall x, bar_post (f x)) -> bar_post (Ctor 
(fun x => f x)).
  Hypothesis B02 : forall f, bar_pre (Ctor f) -> forall x, bar_pre (f x).
  
  Hypothesis B11 : forall x, foo_post x -> bar_post (Rec x).
  Hypothesis B12 : forall x, bar_pre (Neg x) -> foo_pre x.

  Hypothesis B21 : forall x, bar_post x -> bar_post (Rec x).
  Hypothesis B22 : forall x, bar_pre (Rec x) -> bar_pre x.


  Fixpoint foo_spec h : foo_pre h -> foo_post (foo h)
  with     bar_spec h : bar_pre h -> bar_post (bar h).
  Proof.
    + destruct h as [ f | x | x ]; simpl.
      * intros H; apply F01.
        intros x; apply foo_spec, F02, H.
      * intros H; apply F11, bar_spec, F12, H.
      * intros H; apply F21, foo_spec, F22, H.
    + destruct h as [ f | x | x ]; simpl.
      * intros H; apply B01.
        intros x; apply bar_spec, B02, H.
      * intros H; apply B11, foo_spec, B12, H.
      * intros H; apply B21, bar_spec, B22, H.
  Qed.

End foo_rec_mutual_rect.



----- Mail original -----
> De: "Dominique Larchey-Wendling" 
> <dominique.larchey-wendling AT loria.fr>
> À: "coq-club" 
> <coq-club AT inria.fr>
> Envoyé: Mardi 16 Avril 2019 13:23:29
> Objet: Re: [Coq-Club] Mutual induction schemes and recursive function 
> arguments

> Hi John,
> 
> Why not try to use regular fixpoints and prove properties
> by mutual fixpoints mimicking the def of foo/bar. See below
> 
> Best,
> 
> Dominique
> 
> -------------
> 
> Section Foo.
> 
> Variable a : Type.
> 
> Inductive Higher :=
>  | Ctor (f : a -> Higher)
>  | Neg (x : Higher)
>  | Rec (x : Higher).
> 
> Fixpoint foo (h : Higher) : Higher :=
>  match h with
>  | Ctor f => Ctor (fun x => foo (f x))
>  | Neg x => Rec (bar x)
>  | Rec x => Rec (foo x)
>  end
> with
>  bar (h : Higher) : Higher :=
>  match h with
>  | Ctor f => Ctor (fun x => bar (f x))
>  | Neg x => Rec (foo x)
>  | Rec x => Rec (bar x)
>  end.
> 
> Variable (foo_pre foo_post bar_pre bar_post : Higher -> Type).
> 
> Fixpoint foo_spec h : foo_pre h -> foo_post h
> with     bar_spec h : bar_pre h -> bar_post h.
> Proof.
>  (* ... *)
> Admitted.
> 
> End Foo.
> 
> 
> 
> ----- Mail original -----
>> De: "John Wiegley" 
>> <johnw AT newartisans.com>
>> À: "coq-club" 
>> <coq-club AT inria.fr>
>> Envoyé: Mardi 16 Avril 2019 09:11:53
>> Objet: [Coq-Club] Mutual induction schemes and recursive function arguments
> 
>> Hello,
>> 
>> I have a data structure, one of whose constructors takes a function whose
>> result is of the same type. I'd like to be able to recusively apply an 'f' 
>> to
>> this structure, and prove that this 'f' preserves certain properties. 
>> However,
>> the induction hypothesis generated by 'Function' is too weak. What is the 
>> best
>> way to match the strength given by the data structure's own induction
>> hypothesis? The reason I'm unable to use it directly is that I need to take
>> mutual recursion into account. A reduced code example showing the 
>> difficulty
>> follows.
>> 
>> Thank you,
>>  John
>> 
>> Require Import FunInd.
>> Require Import Program.
>> 
>> Section Foo.
>> 
>> Variable a : Type.
>> 
>> Inductive Higher :=
>>  | Ctor (f : a -> Higher)
>>  | Neg (x : Higher)
>>  | Rec (x : Higher).
>> 
>> Function foo (h : Higher) : Higher :=
>>  match h with
>>  | Ctor f => Ctor (foo ∘ f)
>>  | Neg x => Rec (bar x)
>>  | Rec x => Rec (foo x)
>>  end
>> with
>>  bar (h : Higher) : Higher :=
>>  match h with
>>  | Ctor f => Ctor (bar ∘ f)
>>  | Neg x => Rec (foo x)
>>  | Rec x => Rec (bar x)
>>  end.
>> 
>> (* foo is defined
>>   bar is defined
>>   foo, bar are recursively defined (decreasing respectively on 1st,
>>   1st arguments)
>>   foo_equation is defined
>>   foo_ind is defined
>>   foo_rec is defined
>>   foo_rect is defined
>>   bar_equation is defined
>>   bar_ind is defined
>>   bar_rec is defined
>>   bar_rect is defined
>>   R_foo_correct is defined
>>   R_bar_correct is defined
>>   R_foo_complete is defined
>>   R_bar_complete is defined *)
>> 
>> (** Note the induction hypothesis for Ctor:
>> 
>>    (forall f : a -> Higher, (forall a : a, P (f a)) -> P (Ctor f)) *)
>> 
>> Print Higher_ind.
>> 
>> (** It is missing for foo_ind:
>> 
>>    (forall (h : Higher) (f : a -> Higher),
>>      h = Ctor f -> P (Ctor f) (Ctor (foo ∘ f))) *)
>> 
>> Print foo_ind.
>> 
>> Functional Scheme foo_ind2 := Induction for foo Sort Prop
>>  with bar_ind2 := Induction for bar Sort Prop.
>> 
>> (** And also for foo_ind2:
>> 
>>    (forall (h : Higher) (f : a -> Higher),
>>        h = Ctor f -> P (Ctor f) (Ctor (foo ∘ f)))
>>    (forall (h : Higher) (f2 : a -> Higher),
>>        h = Ctor f2 -> P0 (Ctor f2) (Ctor (bar ∘ f2))) *)
>> 
>> Print foo_ind2.
>> 
>> Function foo' (h : Higher) : Higher :=
>>  match h with
>>  | Ctor f => Ctor (fun x => foo' (f x))
>>  | Neg x => Rec (bar' x)
>>  | Rec x => Rec (foo' x)
>>  end
>> with
>>  bar' (h : Higher) : Higher :=
>>  match h with
>>  | Ctor f => Ctor (fun x => bar' (f x))
>>  | Neg x => Rec (foo' x)
>>  | Rec x => Rec (bar' x)
>>  end.
>> 
>> (** Why does it now fail to build the graph?
>> 
>>    foo' is defined
>>    bar' is defined
>>    foo', bar' are recursively defined (decreasing respectively on 1st,
>>    1st arguments)
>>    Warning: Cannot define graph(s) for foo', bar'
>>    [funind-cannot-define-graph,funind]
>>    Warning: Cannot build inversion information
>>    [funind-cannot-build-inversion,funind] *)
>> 
>> End Foo.
>> 
>> --
>> John Wiegley                  GPG fingerprint = 4710 CF98 AF9B 327B B80F
> > http://newartisans.com                          60E1 46C4 BD1A 7AC1 4BA2