The Coq mailing list

[Chris Dams <chris.dams.nl AT gmail.com>]

Hello Jef,

2010/1/22 Jeff Terrell 
<jeff AT kc.com>:
> Many thanks for your comments. Unfortunately, this problem is a show stopper
> for my project. Does anyone know if there's a prototypical implementation of
> Coq that would allow f to pass the guardedness checker?

The development below more or less does this. It first makes a
coinductive type that is bigger than what you need, then restricts
that by introducing a predicate, creating a version of f that lives in
the bigger coinductive set and finally defines a new ff that is more
or less equivalent to your f, I don't know if this can be used in your
particular case but it might be a start. Note that my implementation
is horrendously code-duplicated. Generally one would want to turn the
types A and X into some abstract data type to avoid this.

Good luck,
Chris


CoInductive A: Set
:= | Build_A : A_list -> A
with A_list: Set
:= | cons_A: A -> A_list -> A_list
  | nil_A: A_list.

Inductive A_list_finite: A_list -> Prop
:= | nil_A_finite: A_list_finite nil_A
  | cons_A_finite:
       forall a: A,
       forall l: A_list,
       A_list_finite l ->
       A_list_finite (cons_A a l).

CoInductive A_lists_finite: A -> Prop
:= | Build_A_finite:
       forall l: A_list,
       A_list_and_children_finite l ->
       A_lists_finite (Build_A l)
with A_list_and_children_finite: A_list -> Prop
:= | Build_A_finite_nil:
       A_list_and_children_finite nil_A
  | Build_A_finite_cons:
       forall a: A,
       forall l: A_list,
       A_lists_finite a ->
       A_list_finite l ->
       A_list_and_children_finite l ->
       A_list_and_children_finite (cons_A a l).

Inductive AA: Set
:= mk_AA: forall a: A, A_lists_finite a -> AA.

CoInductive X : Set
:= | Build_X : X_list -> X
with X_list: Set
:= | cons_X: X -> X_list -> X_list
  | nil_X: X_list.

Theorem X_unfold:
  forall x: X,
  x = match x with
      | Build_X l => Build_X l
      end.
Proof.
intro x.
case x.
tauto.
Qed.

Theorem X_list_unfold:
  forall l: X_list,
  l = match l with
      | cons_X x l => cons_X x l
      | nil_X => nil_X
      end.
Proof.
intro l.
case l; tauto.
Qed.

Inductive X_list_finite: X_list -> Prop
:= | nil_X_finite: X_list_finite nil_X
  | cons_X_finite:
       forall a: X,
       forall l: X_list,
       X_list_finite l ->
       X_list_finite (cons_X a l).

CoInductive X_lists_finite: X -> Prop
:= | Build_X_finite:
       forall l: X_list,
       X_list_and_children_finite l ->
       X_lists_finite (Build_X l)
with X_list_and_children_finite: X_list -> Prop
:= | Build_X_finite_nil:
       X_list_and_children_finite nil_X
  | Build_X_finite_cons:
       forall a: X,
       forall l: X_list,
       X_lists_finite a ->
       X_list_finite l ->
       X_list_and_children_finite l ->
       X_list_and_children_finite (cons_X a l).

Inductive XX: Set
:= mk_XX: forall x: X, X_lists_finite x -> XX.

CoFixpoint f (a: A): X
:= match a with
  | Build_A l => Build_X (f_list l)
  end
with f_list (l: A_list): X_list
:= match l with
  | cons_A a l => cons_X (f a) (f_list l)
  | nil_A => nil_X
  end.

Theorem f_list_conserves_list_finite:
  forall l: A_list,
  A_list_finite l ->
  X_list_finite (f_list l).
Proof.
intros l H1.
induction H1 as [|a l H1 IH];
  rewrite X_list_unfold;
  simpl;
  [apply nil_X_finite; fail|].
apply cons_X_finite.
assumption.
Qed.

Theorem f_conserves_lists_finite:
  forall a: A,
  forall H1: A_lists_finite a,
  X_lists_finite (f a).
refine (
  cofix f_conserves_lists_finite (a: A) (H1: A_lists_finite a):
     X_lists_finite (f a)
  := match H1 with
     | Build_A_finite l H2 => _
     end
  with f_conserves_lists_finite_list (l: A_list)
        (H1: A_list_and_children_finite l):
     X_list_and_children_finite (f_list l)
  := match H1 with
     | Build_A_finite_nil => _
     | Build_A_finite_cons a l H2 H3 H4 => _
     end
  for f_conserves_lists_finite).
(* Build_A_finite *)
rewrite X_unfold.
simpl.
apply Build_X_finite.
apply f_conserves_lists_finite_list.
assumption.
(* Build_A_finite *)
rewrite X_list_unfold.
simpl.
apply Build_X_finite_nil.
(* Build_A_finite_cons *)
rewrite X_list_unfold.
simpl.
apply Build_X_finite_cons;
  [apply f_conserves_lists_finite
  |apply f_list_conserves_list_finite
  |apply f_conserves_lists_finite_list];
  assumption.
Qed.

Definition ff (a: AA): XX.
intros [a H1].
apply (mk_XX (f a)).
apply f_conserves_lists_finite.
assumption.
Defined.