Ssreflect Users Discussion List

[Vladimir Komendantsky <>]

Dear Ssreflect club,

Recently I tried to implement "monadic"
substitution for a language of recursive types with nameless variables.
I referred to Conor McBride's "Type-preserving renaming and
substitution" and Danielsson's "Subtyping, declaratively", replacing
the inductive family of finite number with type ordinal and dependent
vectors with tuples. It works rather well compared to other popular
"types for programming language metatheory" methods. I'm attaching the
definitions.

There seems to be a problem with representing recursive types as
(infinitely) unfolded structures. As you can see, I use CoInductive to
define the type of finite and infinite tree, which has a side-effect on
proofs about trees: one has to force Coq evaluation in a way that looks
to me as a hack: tree_forced. Is there a way to avoid a step "rewrite
(tree_forced ...) /=" ?

It's unclear to me whether Coq can be used to prove that a mixed
inductive-coinductive relation Tyle below is in fact equivalent to
subtyping (Tle) modulo tree representation (tree_of). It seems that my
last hope is somehow to restrict proofs to finitary cases. Does
Ssreflect provide a method to define possibly an approximation of
le_arr below without using the CoInductive INF?

(* suspension functor INF with a delay constructor *)
CoInductive INF T : Type :=
  delay : forall x : T, INF T.

(* the force operation remomving one delay constructor *)
Definition force T (x' : INF T) : T :=
  match x' with delay x => x end.

(* subtyping without trees, by syntactic one-step unfolding *)
Inductive Tyle n : Ty n -> Ty n -> Type :=
  | le_bot :   forall E,       Tyle bot E
  | le_top :   forall E,       Tyle E top
  | le_arr :   forall E F G H, INF (Tyle E F) -> INF (Tyle G H)


                            -> Tyle (arr F G) (arr E H)
  | le_unfold: forall E F,     Tyle (mu E F) (unfld E F)
  | le_fold :  forall E F,     Tyle (unfld E F) (mu E F)
  | le_refl :  forall E,       Tyle E E


  | le_tran :  forall E F G,   Tyle E F -> Tyle F G -> Tyle E G.


The desired equivalence would consist of a pair of functions (as it does in Agda):

Theorem sound : forall n (E F : Ty n), Tyle E F -> Tle (tree_of E) (tree_of F).


Theorem complete : forall n (E F : Ty n), Tle (tree_of E) (tree_of F) -> Tyle E F.

proving
which seems impossible when Tyle is not CoInductive. Meanwhile, if we
define Tyle by CoInductive, the resulting relation is trivial (thanks
to transitivity). So, this variant is not considered.

Best wishes,
Vladimir

Attachment: Tle.v
Description: Binary data