The Coq mailing list

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

Dear Clare Jang,

As hinted in private before, you can use the Braga method to approach the study of your

complex *mutual and nested* recursive scheme. I did the exercise for you but having no

idea of what this algorithm computes, I cannot establish partial correctness results.

You would need to figure that out yourself.

However, below are all the tool you might need to prove those results in the form

of a proof-irrelevant Inductive-Recursive scheme, provided that you know what

property you want to establish for subst[Sub,Ty]. You can show partial correctness

results use the domain recursors DsS & DsT but you need to establish properties

simultaneously for subst[Sub,Ty] because of the mutual scheme.

Good luck,

Dominique

(**************************************************************)
(*   Copyright Dominique Larchey-Wendling [*]                 *)
(*                                                            *)
(*                             [*] Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

Require Import Arith.

(**

An implementation of the following mutual and nested
recursive schemes using the Braga method

Fixpoint substSub (s : Sub) (n : nat) (s' : Sub) : Sub :=
  match s' with
  | NullS => NullS
  | SnocS s'' t'' => SnocS (substSub s n s'') (substTy s n t'')
  end
with substTy (s : Sub) (n : nat) (t' : Ty) : Ty :=
  match t' with
  | TUnit => TUnit
  | TBox t'' => TBox (substTy s n t'')
  | TUnbox x'' d'' s'' =>
    if eq_nat_dec d'' n
    then
      match nth s x'' with
      | TBox t''' => substTy (substSub s n s'') d'' t'''
      | t''' => TUnit
      end
    else
      TUnbox x'' d'' (substSub s n s'')
  end
.

*)

Section nested_and_mutual.

  Inductive Sub : Set :=
    | NullS : Sub
    | SnocS : Sub -> Ty -> Sub
  with Ty : Set :=
    | TUnit : Ty
    | TBox : Ty -> Ty
    | TUnbox : nat -> nat -> Sub -> Ty
    .

  Fixpoint nth (s : Sub) (x : nat) : Ty :=
    match s with
      | NullS => TUnit
      | SnocS s' t' =>
      match x with
        | O => t'
        | S x' => nth s' x'
      end
    end.

  (* The graphs of subst[Sub,Ty] linking the inputs and outputs *)

  Inductive g_substSub : Sub -> nat -> Sub -> Sub -> Prop :=
    | in_gsS_N s n : g_substSub s n NullS NullS
    | in_gsS_S s n s' t' rs rt : g_substSub s n s' rs
                              -> g_substTy s n t' rt
                              -> g_substSub s n (SnocS s' t') (SnocS rs rt)
  with g_substTy : Sub -> nat -> Ty -> Ty -> Prop :=
    | in_gsT_u s n : g_substTy s n TUnit TUnit
    | in_gsT_B s n t' rt : g_substTy s n t' rt -> g_substTy s n (TBox t') (TBox rt)
    | in_gsT_U1 s n x d s' t' rs rt : d = n
                          -> nth s x = TBox t'
                          -> g_substSub s n s' rs
                          -> g_substTy rs d t' rt
                          -> g_substTy s n (TUnbox x d s') rt
    | in_gsT_U2 s n x d s' : d = n
                          -> (~ exists t', nth s x = TBox t')
                          -> g_substTy s n (TUnbox x d s') TUnit
    | in_gsT_U3 s n x d s' rs : d <> n
                          -> g_substSub s n s' rs
                          -> g_substTy s n (TUnbox x d s') (TUnbox x d rs)
    .

  (* The graphs are functional/deterministic *)

  Fixpoint g_substSub_fun s n s' o1 (H1 : g_substSub s n s' o1) : forall o2, g_substSub s n s' o2 -> o1 = o2
  with     g_substTy_fun s n t' o1 (H1 : g_substTy s n t' o1) : forall o2, g_substTy s n t' o2 -> o1 = o2.
  Proof.
    + destruct H1 as [s n | s n s' t' rs rt H1 H2 ].
      * inversion 1; trivial.
      * inversion 1; f_equal.
        - apply g_substSub_fun with (1 := H1); assumption.
        - apply g_substTy_fun with (1 := H2); assumption.
    + destruct H1 as [ s n | s n t' rt H1 | s n x d s' t' rs rt H1 H2 H3 H4 | s n x d s' H1 H2 | s n x d s' rs H1 H2 ].
      * inversion 1; trivial.
      * inversion 1; f_equal.
        apply g_substTy_fun with (1 := H1); assumption.
      * inversion 1.
        - generalize (g_substSub_fun _ _ _ _ H3 _ H12); intro; subst rs0.
          rewrite H2 in H10; inversion H10; subst t'0.
          apply (g_substTy_fun _ _ _ _ H4 _ H13).
        - destruct H11; exists t'; trivial.
        - destruct H10; trivial.
      * inversion 1.
        - destruct H2; exists t'; trivial.
        - trivial.
        - destruct H8; trivial.
      * inversion 1.
        - destruct H1; trivial.
        - destruct H1; trivial.
        - f_equal.
          apply g_substSub_fun with (1 := H2); assumption.
  Qed.

  (* Characterization of the domains using the subcall/call relation *)

  Let Call := ((Sub * nat * Sub) + (Sub * nat * Ty))%type.

  Reserved Notation "x '<sc' y" (at level 70).

  Inductive Ds_subcall : Call -> Call -> Prop :=
    | in_sc_0 s n s' t' : inl (s,n,s') <sc inl (s,n,SnocS s' t')
    | in_sc_1 s n s' t' : inr (s,n,t') <sc inl (s,n,SnocS s' t')
    | in_sc_2 s n t' : inr (s,n,t') <sc inr (s,n,TBox t')
    | in_sc_3 s n x d s' t' : d = n -> nth s x = TBox t' -> inl (s,n,s') <sc inr (s,n,TUnbox x d s')
    | in_sc_4 s n x d s' t' rs : d = n -> nth s x = TBox t' -> g_substSub s n s' rs -> inr (rs,d,t') <sc inr (s,n,TUnbox x d s')
    | in_sc_5 s n x d s' : d <> n -> inl (s,n,s') <sc inr (s,n,TUnbox x d s')
  where "x '<sc' y" := (Ds_subcall x y).

  Definition DsS s n s' := Acc Ds_subcall (inl (s,n,s')).
  Definition DsT s n t' := Acc Ds_subcall (inr (s,n,t')).

  (* The subst[Sub,Ty] packed with conformity certificate wrt the their graphs *)

  Let Fixpoint substSub_pwc s n s' (D : DsS s n s') { struct D } : sig (g_substSub s n s')
  with     substTy_pwc s n t' (D : DsT s n t') { struct D } : sig (g_substTy s n t').
  Proof.
    + revert D; refine (match s' with
        | NullS => fun _ => exist _ NullS _
        | SnocS s' t' => fun D => let (s1,S1) := substSub_pwc s n s' _ in
                                  let (t1,T1) := substTy_pwc s n t' _
                                  in  exist _ (SnocS s1 t1) _
      end).
      * constructor.
      * apply Acc_inv with (1 := D); constructor.
      * apply Acc_inv with (1 := D); constructor.
      * constructor; assumption.
    + revert D; refine (match t' with
        | TUnit => fun _ => exist _ TUnit _
        | TBox t' => fun D => let (t1,T1) := substTy_pwc s n t' _
                              in  exist _ (TBox t1) _
        | TUnbox x d s' => fun D =>
          match eq_nat_dec d n with
            | left H => match nth s x as u return nth s x = u -> _ with
              | TBox t' => fun E => let (s1,S1) := substSub_pwc s n s' _ in
                                    let (t1,T1) := substTy_pwc s1 d t' _
                                    in exist _ t1 _
              | _       => fun _ => exist _ TUnit _
            end eq_refl
            | right H => let (s1,S1) := substSub_pwc s n s' _
                         in exist _ (TUnbox x d s1) _
          end
      end).
      * constructor.
      * apply Acc_inv with (1 := D); constructor.
      * constructor; trivial.
      * constructor; trivial.
        intros (t1 & E); now rewrite E in *.
      * apply Acc_inv with (1 := D); constructor 4 with t'; trivial.
      * apply Acc_inv with (1 := D); constructor 5; trivial.
      * constructor 3 with t' s1; trivial.
      * constructor 4; trivial.
        intros (t1 & E); now rewrite E in *.
      * apply Acc_inv with (1 := D); constructor; trivial.
      * constructor; trivial.
  Qed.

  (* Now the partial functions, by projection *)

  Definition substSub s n s' D := proj1_sig (substSub_pwc s n s' D).
  Definition substTy s n t' D := proj1_sig (substTy_pwc s n t' D).

  (* And their specs, conformity with their graphs *)

  Fact substSub_spec s n s' D : g_substSub s n s' (substSub s n s' D).
  Proof. apply (proj2_sig _). Qed.

  Fact substTy_spec s n t' D : g_substTy s n t' (substTy s n t' D).
  Proof. apply (proj2_sig _). Qed.

  (** Proof irrelevance *)

  Fact substSub_pirr s n s' D1 D2 : substSub s n s' D1 = substSub s n s' D2.
  Proof. apply g_substSub_fun with s n s'; apply substSub_spec. Qed.

  Fact substTy_pirr s n t' D1 D2 : substTy s n t' D1 = substTy s n t' D2.
  Proof. apply g_substTy_fun with s n t'; apply substTy_spec. Qed.

  (** Domain constructors Induction-Recursion style *)

  Fact DsS_0 s n : DsS s n NullS.
  Proof. constructor; inversion 1. Qed.

  Fact DsS_1 s n s' t' : DsS s n s' -> DsT s n t' -> DsS s n (SnocS s' t').
  Proof. intros H1 H2; constructor; inversion 1; auto. Qed.

  Fact DsT_0 s n : DsT s n TUnit.
  Proof. constructor; inversion 1. Qed.

  Fact DsT_1 s n t' : DsT s n t' -> DsT s n (TBox t').
  Proof. intros H; constructor; inversion 1; auto. Qed.

  Fact DsT_2 s n x d s' t' : d = n -> nth s x = TBox t' -> forall D : DsS s n s', DsT (substSub s n s' D) d t' -> DsT s n (TUnbox x d s').
  Proof.
    intros H1 H2 D HD.
    constructor; inversion 1; subst.
    + apply D.
    + rewrite (g_substSub_fun _ _ _ _ H10 _ (substSub_spec _ _ _ D)).
      rewrite H2 in H9; inversion H9; subst; trivial.
    + destruct H4; trivial.
  Qed.

  Fact DsT_3 s n x d s' : d = n -> (~ exists t', nth s x = TBox t') -> DsT s n (TUnbox x d s').
  Proof.
    intros H1 H2.
    constructor; inversion 1; subst.
    + destruct H2; exists t'; trivial.
    + destruct H2; exists t'; trivial.
    + destruct H4; trivial.
  Qed.

  Fact DsT_4 s n x d s' : d <> n -> DsS s n s' -> DsT s n (TUnbox x d s').
  Proof.
    intros H1 H2.
    constructor; inversion 1; subst; now auto.
  Qed.

  (** Fixpoint equations *)

  Hint Resolve substSub_spec substTy_spec : core.
  Hint Constructors g_substSub g_substTy : core.

  Fact substSub_fix_0 s n : substSub s n NullS (DsS_0 s n) = NullS.
  Proof. apply g_substSub_fun with s n NullS; auto. Qed.

  Fact substSub_fix_1 s n s' t' D1 D2 :
            substSub s n (SnocS s' t') (DsS_1 s n s' t' D1 D2)
          = SnocS (substSub s n s' D1) (substTy s n t' D2).
  Proof. apply g_substSub_fun with s n (SnocS s' t'); auto. Qed.

  Fact substTy_fix_0 s n : substTy s n TUnit (DsT_0 s n) = TUnit.
  Proof. apply g_substTy_fun with s n TUnit; auto. Qed.

  Fact substTy_fix_1 s n t' D :
            substTy s n (TBox t') (DsT_1 s n t' D)
          = TBox (substTy s n t' D).
  Proof. apply g_substTy_fun with s n (TBox t'); auto. Qed.

  Fact substTy_fix_2 s n x d s' t' E H D1 D2 :
            substTy s n (TUnbox x d s') (DsT_2 s n x d s' t' E H D1 D2)
          = substTy (substSub s n s' D1) d t' D2.
  Proof.
    apply g_substTy_fun with s n (TUnbox x d s'); auto.
    constructor 3 with t' (substSub s n s' D1); auto.
  Qed.

  Fact substTy_fix_3 s n x d s' E H :
            substTy s n (TUnbox x d s') (DsT_3 s n x d s' E H)
          = TUnit.
  Proof. apply g_substTy_fun with s n (TUnbox x d s'); auto. Qed.

  Fact substTy_fix_4 s n x d s' E D :
            substTy s n (TUnbox x d s') (DsT_4 s n x d s' E D)
          = TUnbox x d (substSub s n s' D).
  Proof. apply g_substTy_fun with s n (TUnbox x d s'); auto. Qed.

  Section mutual_recursors.

    Variable (P : forall s n s', DsS s n s' -> Type) (Q : forall s n t', DsT s n t' -> Type)
             (HPi : forall s n s' D1 D2, P s n s' D1 -> P s n s' D2)
             (HP0 : forall s n, P _ _ _ (DsS_0 s n))
             (HP1 : forall s n s' t' D1 (_ : P _ _ _ D1) D2 (_ : Q _ _ _ D2), P _ _ _ (DsS_1 s n s' t' D1 D2))
             (HQi : forall s n t' D1 D2, Q s n t' D1 -> Q s n t' D2)
             (HQ0 : forall s n, Q _ _ _ (DsT_0 s n))
             (HQ1 : forall s n t' D (_ : Q _ _ _ D), Q _ _ _ (DsT_1 s n t' D))
             (HQ2 : forall s n x d s' t' E H D1 (_ : P _ _ _ D1) D2 (_ : Q _ _ _ D2), Q _ _ _ (DsT_2 s n x d s' t' E H D1 D2))
             (HQ3 : forall s n x d s' E H, Q _ _ _ (DsT_3 s n x d s' E H))
             (HQ4 : forall s n x d s' E D (_ : P _ _ _ D), Q _ _ _ (DsT_4 s n x d s' E D)).

    Fixpoint DsS_rect s n s' D : P s n s' D
    with     DsT_rect s n t' D : Q s n t' D.
    Proof.
      + destruct s' as [ | s' t' ].
        * refine (HPi _ _ _ _ _ (HP0 _ _)).
        * refine (HPi _ _ _ _ _ (HP1 _ _ _ _ _ (DsS_rect s n s' _) _ (DsT_rect s n t' _)));
            apply Acc_inv with (1 := D); constructor.
      + destruct t' as [ | t' | x d s' ].
        * refine (HQi _ _ _ _ _ (HQ0 _ _)).
        * refine (HQi _ _ _ _ _ (HQ1 _ _ _ _ (DsT_rect s n t' _)));
            apply Acc_inv with (1 := D); constructor.
        * destruct (eq_nat_dec d n) as [ E | E ]; [ case_eq (nth s x) | ].
          - intros H.
            refine (HQi _ _ _ _ _ (HQ3 _ _ _ _ _ _ _)); auto.
            intros (? & H1); now rewrite H1 in H.
          - intros t' H.
            assert (D1 : DsS s n s').
            { apply Acc_inv with (1 := D); constructor 4 with t'; auto. }
            refine (HQi _ _ _ _ _ (HQ2 _ _ _ _ _ _ E H _ (DsS_rect s n s' D1) _ (DsT_rect _ _ _ _))); auto.
            apply Acc_inv with (1 := D); constructor; auto.
          - intros x' d' s'' H'.
            refine (HQi _ _ _ _ _ (HQ3 _ _ _ _ _ _ _)); auto.
            intros (? & H1); now rewrite H1 in H'.
          - refine (HQi _ _ _ _ _ (HQ4 _ _ _ _ _ _ _ (DsS_rect _ _ _ _))); auto.
            apply Acc_inv with (1 := D); constructor; auto.
    Qed.

  End mutual_recursors.

  (** Notice that until now, we build the inductive-recursive scheme
      w/o using knowledge about what subst[Sub,Ty] actually compute.

      You can use DsS_rect & DsT_rect to characterise what subst[Sub,Ty]
      compute on there respective domains, ie *partial correctness results*.

      Then you can try to show

      (a) forall s n s', DsS s n s' and (b) forall s n t', DsT s n t'

      But you might need partial correctness results because of the nesting
      of recursive calls
   *)

End nested_and_mutual.