The Coq mailing list

[Gyesik Lee <gslee AT ropas.snu.ac.kr>]

2010/3/20 Roman Beslik 
<beroal AT ukr.net>:
> First, Coq thinks that structural argument is "a". Because of "match x", I
> suppose that structural argument is "x", so write it explicitly: "fix to_T
> (a : Rep) (x : Interpret RT a) {struct x} : ...". Then you must call "to_T"
> with a subterm of "x". That subterm is of type "Interpret RT Rec". "to_T"
> may not receive an argument of such a type, so you can not call "to_T".
> Recursion is impossible.

Using {struct x} doesn't help.


> And it does not make sense to me. What do you suppose "to_T" to do?

It should reproduce the set T from its interpretation (Interpret RT RT).
(RT is a kind of a representative of T)

=======

Having seen that the problem setting seems to be not trivial to
handle, let me ask questions one by one.

First, I would like to know why the proof mode in [to_T] won't close
where I use "refine (fix ...)" style to use induction on the
well-founded relation based on the structurally-smaller-than-relation.
(I am aware of the danger of using "fix" and using Coq 8.2pl1)

Inductive Rep : Type :=
| Plus   : Rep -> Rep -> Rep
| Rec    : Rep
| Const  : Type -> Rep.

Inductive Interpret (r : Rep) : Rep -> Type :=
| inl   : forall a b, Interpret r a -> Interpret r (Plus a b)
| inr   : forall a b, Interpret r b -> Interpret r (Plus a b)
| rec   : Interpret r r -> Interpret r Rec
| const : forall a, a -> Interpret r (Const a).

Inductive T :=
| A : nat -> T
| B : T -> T.

Definition RT := Plus (Const nat) Rec.

Definition to_T (a : Rep) (x : Interpret RT a) : (a = RT) -> T.
refine (fix to_T (a : Rep) (x : Interpret RT a) {struct x}: (a = RT) -> T :=
  match x with
    | inl a b _ => _
    | inr a b _ => _
    | rec _ => _
    | const a _  => _
  end
); intros; try discriminate.

(* only the case [a = Plus l r] remains.*)

(* first case: [l = (Const nat)] *)
inversion H.
subst a0.
(* to get [i = const nat X] for some X *)
inversion i.
(* use the X *)
exact (A X).

(* second case: [r = Rec] *)

inversion H.
subst b.
(* to get [i = rec X  for some X of type (Interpret RT RT) *)
inversion i.
(* apply to_T to this X which is structrually smaller than x. *)
exact (to_T RT X (refl_equal RT)).
(* the proof is finished, but termination check failed although X is
obviously structurally smaller than x. *)
Defined.