Library CoLoR.Term.Lambda.LCompInt

CoLoR, a Coq library on rewriting and termination.
See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2013-07-30

Interpretation of positive inductive data type systems

as computability predicates so that the accessible arguments (that must satisfy some positivity condition) of a computable constructor term are computable.

Set Implicit Arguments.


Accessible supterm relation.


Module Export Def.

  Section supterm_acc.

    Variables F X : Type.
    Notation Fun := (@Fun F X).
    Notation Te := (@Te F X).

    Variable So : Type.
    Notation Ty := (@Ty So).

    Variable typ : F -> Ty.
    Notation TypArgs := (@TypArgs F X So typ).

    Variables (Acc : F -> set nat)
      (Acc_arity : forall f i, Acc f i -> i < arity (typ f)).

    Inductive supterm_acc : relation Te :=
    | stacc_intro : forall f (ts : TypArgs f) i (hi : Acc f i),
      supterm_acc (apps (Fun f) ts) (Vnth ts (Acc_arity hi)).

    Lemma stacc_intro' f (ts : TypArgs f) i (hi : Acc f i) t u :
      t = apps (Fun f) ts -> u = Vnth ts (Acc_arity hi) -> supterm_acc t u.

  End supterm_acc.

End Def.

Structure on base types for defining their interpretation as computability predicates.


Module Type BI_Struct.

We assume given an ST structure.

  Declare Module Export ST : ST_Struct.

We assume given a decidable total ordering structure on base types.

  Declare Module Export BOrd : OrderedType
  with Definition t := So
  with Definition eq := @Logic.eq So.

  Infix "<B" := lt (at level 70).
  Notation gtB := (transp lt) (only parsing).
  Infix ">B" := gtB (at level 70).

We assume that ltB is well-founded (in Coq sense).

  Parameter ltB_wf : well_founded lt.

For each symbol f : T_0 ~~> .. ~~> T_{n-1} -> A, we assume given a set Acc f of accessible argument positions i between 0 and n-1 such that, for every base type B occurring in T_i, either B is smaller than A, or B is equivalent to A and occurs only positively in T_i.

  Parameter Acc : F -> set nat.
  Parameter Acc_arity : forall f i, Acc f i -> i < arity (typ f).
  Parameter Acc_ok : forall f i (hi : Acc f i) a,
    occurs a (Vnth (inputs (typ f)) (Acc_arity hi)) ->
    a <B output_base (typ f)
    \/ (a = output_base (typ f)
      /\ pos a (Vnth (inputs (typ f)) (Acc_arity hi))).


Notations.

  Notation aeq := (@aeq F X FOrd.eq_dec XOrd.eq_dec ens_X var_notin).
  Notation vaeq := (Vforall2 aeq).
  Notation supterm_acc := (@supterm_acc F X So typ Acc Acc_arity).

End BI_Struct.

Definition of the interpretation of base types

given an ST structure for terms, a CP structure for the rewrite relation, and a BI structure.

Module Make (Export ST : ST_Struct)
  (Export CP : CP_Struct with Module L := ST.L)
  (Export BI : BI_Struct with Module ST := ST).

  Module Import P := OrderedTypeFacts BOrd.
  Module Export CS := LCompSimple.Make ST CP.

  Infix "=>R" := (clos_aeq (clos_mon Rh)).
  Infix "=>R*" := (R_aeq*).

Properties of supterm_acc.


  Lemma supterm_acc_supterm : supterm_acc << supterm!.

  Lemma supterm_acc_wf : WF supterm_acc.

  Instance size_subpterm_acc : Proper (supterm_acc --> Peano.lt) size.


  Lemma supterm_acc_size : supterm_acc << transp (ltof size).

  Lemma aeq_supterm_acc_commut : aeq @ supterm_acc << supterm_acc @ aeq.

  Lemma aeq_tc_supterm_acc_commut :
    aeq @ (supterm_acc!) << (supterm_acc!) @ aeq.

  Lemma supterm_acc_subs : forall s t u,
    supterm_acc t u -> supterm_acc (subs s t) (subs s u).

  Lemma tc_supterm_acc_subs : forall s t u,
    supterm_acc! t u -> supterm_acc! (subs s t) (subs s u).

  Section tc_supterm_acc_R_mon_wf.

    Variables (R : relation Te) (R_mon : Monotone R).

    Lemma supterm_acc_R_mon_commut : supterm_acc @ R << R @ supterm_acc.

    Lemma tc_supterm_acc_R_mon_commut : supterm_acc! @ R << R @ supterm_acc!.

    Lemma tc_supterm_acc_R_mon_wf : WF R -> WF (supterm_acc! U R).

    Import RelUtil.

    Section restrict.

      Variables (P : set Te) (P_R : Proper (R ==> impl) P).

      Lemma restrict_tc_supterm_acc_R_mon_wf :
        WF (restrict P R) -> WF (restrict P (supterm_acc! U R)).

    End restrict.

    Lemma restrict_SN_tc_supterm_acc_R_mon_wf :
      WF (restrict (SN R) (supterm_acc! U R)).

  End tc_supterm_acc_R_mon_wf.

Properties of clos_aeq supterm_acc.


  Lemma clos_aeq_supterm_acc_wf : WF (clos_aeq supterm_acc).

  Instance clos_aeq_tc_supterm_cc_trans : Transitive (clos_aeq (supterm_acc!)).


  Lemma clos_aeq_tc_supterm_acc_eq :
    clos_aeq (supterm_acc!) == (clos_aeq supterm_acc)!.

  Lemma clos_aeq_tc_supterm_acc_wf : WF (clos_aeq (supterm_acc!)).

  Lemma clos_aeq_tc_supterm_acc_subs : forall s t u,
    clos_aeq (supterm_acc!) t u ->
    clos_aeq (supterm_acc!) (subs s t) (subs s u).

  Section clos_aeq_tc_supterm_acc_R_mon_wf.

    Variables (R : relation Te) (R_mon : Monotone R)
      (R_aeq : Proper (aeq ==> aeq ==> impl) R).

    Lemma clos_aeq_supterm_acc_R_mon_commut :
      clos_aeq supterm_acc @ R << R @ clos_aeq supterm_acc.

    Lemma clos_aeq_tc_supterm_acc_R_mon_commut :
      clos_aeq (supterm_acc!) @ R << R @ clos_aeq (supterm_acc!).

    Lemma clos_aeq_tc_supterm_acc_R_mon_wf :
      WF R -> WF (clos_aeq (supterm_acc!) U R).

    Import SetUtil RelUtil.

    Section restrict.

      Variables (P : set Te) (P_R : Proper (R ==> impl) P).

      Lemma restrict_clos_aeq_tc_supterm_acc_R_mon_wf :
        WF (restrict P R) -> WF (restrict P (clos_aeq (supterm_acc!) U R)).

    End restrict.

    Lemma restrict_SN_clos_aeq_tc_supterm_acc_R_mon_wf :
      WF (restrict (SN R) (clos_aeq (supterm_acc!) U R)).

  End clos_aeq_tc_supterm_acc_R_mon_wf.

Interpretation of types

The interpretation I will be defined by well-founded induction on ltB using Coq's corresponding combinator Wf.Fix, which requires a function F computing the interpretation of a base type a from the interpretation I_lt_a for each base type strictly smaller than a. The interpretation of a itself is defined as the least fixpoint of some variant of the following monotone function G.

  Import SetUtil AccUtil.

  Section fixpoint.

    Variable a : So.

    Definition G I : set Te := fun t =>
      SN R_aeq t /\ forall f, output_base (typ f) = a ->
        forall ts : Tes (arity (typ f)), R_aeq* t (apps (Fun f) ts) ->
          forall i (hi : Acc f i),
            int I (Vnth (inputs (typ f)) (Acc_arity hi))
                  (Vnth ts (Acc_arity hi)).

    Variable I_lt_a : forall b, b <B a -> set Te.

    Definition update (X : set Te) b :=
      match BOrd.compare b a with
        | LT h => I_lt_a h
        | EQ _ => X
        | GT _ => SN R_aeq
      end.

    Definition G' X := G (update X).

    Definition F := lfp subset set_glb G'.

  End fixpoint.

  Definition I : So -> set Te := Fix ltB_wf F.

We now check that G is monotone.

  Section G'_props.

    Variables (a : So) (I_lt_a : forall b, b <B a -> set Te).

    Global Instance G'_mon : Proper (subset ==> subset) (G' I_lt_a).


    Global Instance G'_equiv : Proper (equiv ==> equiv) (G' I_lt_a).


  End G'_props.

We also check that G and F are compatible with equiv.

  Section G_ext.

    Variables (a : So) (I J : So -> set Te)
      (e : forall b, ~b >B a -> I b [=] J b).

    Lemma G_ext : G a I [=] G a J.

  End G_ext.

  Section F_ext.

    Variables (a : So) (I_lt_a J_lt_a : forall b, b <B a -> set Te)
      (e : forall b (h : b <B a), I_lt_a h [=] J_lt_a h).

    Lemma G'_ext : forall X Y, X [=] Y -> G' I_lt_a X [=] G' J_lt_a Y.

    Lemma F_ext : F I_lt_a [=] F J_lt_a.

  End F_ext.

Fixpoint equation satisfied by I.

  Definition I' a b (_ : b <B a) := I b.


  Lemma I_eq_F : forall a, I a [=] F (I' a).

  Lemma I_eq_G' : forall a, I a [=] G' (I' a) (I a).

  Lemma I_eq : forall a, I a [=] G a I.

We now check that base types are interpreted by computability predicates.

  Section cp.

    Variables (a : So) (I_lt_a : forall b, b <B a -> set Te)
      (I_lt_a_cp_aeq : forall b (h : b<B a), cp_aeq (I_lt_a h))
      (I_lt_a_cp_sn : forall b (h : b<B a), cp_sn (I_lt_a h))
      (I_lt_a_cp_red : forall b (h : b<B a), cp_red (I_lt_a h))
      (I_lt_a_cp_neutral : forall b (h : b<B a), cp_neutral (I_lt_a h))
      (X : set Te) (X_cp_aeq : cp_aeq X) (X_cp_sn : cp_sn X)
      (X_cp_red : cp_red X) (X_cp_neutral : cp_neutral X).

    Lemma G'_cp_aeq : cp_aeq (G' I_lt_a X).

    Lemma G'_cp_sn : cp_sn (G' I_lt_a X).

    Lemma G'_cp_red : cp_red (G' I_lt_a X).

    Lemma G'_cp_neutral :
      (forall f n (ts : Tes n), ~neutral (apps (Fun f) ts)) ->
      cp_neutral (G' I_lt_a X).

  End cp.

  Lemma I_cp : (forall f n (ts : Tes n), ~neutral (apps (Fun f) ts)) ->
    forall a, cp (I a).

Computability of accessible arguments.

  Lemma comp_acc : forall f (ts : Tes (arity (typ f))),
    I (output_base (typ f)) (apps (Fun f) ts) -> forall i (hi : Acc f i),
      int I (Vnth (inputs (typ f)) (Acc_arity hi)) (Vnth ts (Acc_arity hi)).

Computability of function symbols.

  Lemma comp_fun : (forall f n (ts : Tes n), ~neutral (apps (Fun f) ts)) ->
    forall f (ts : Tes (arity (typ f))), vint I (inputs (typ f)) ts ->
      (forall u, apps (Fun f) ts =>R u -> I (output_base (typ f)) u) ->
      I (output_base (typ f)) (apps (Fun f) ts).

End Make.