The Coq mailing list

[Roman Beslik <beroal AT ukr.net>]

Yes, you are right, there is a structurally smaller value. See the proof 
below. The answer to why your proof does not check lays in your proof 
term ("Show Proof."). It is huge so its analysis is a separate task.
I also assigned my names to variables because I am always lost in names 
auto-generated by Coq. :)

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 x0 => _
    | rec _ => _
    | const _ _  => _
  end
); intros; try discriminate.
(* first case: [l = (Const nat)] *) inversion H. subst a0. inversion i. 
exact (A X).
(* second case: [r = Rec] *)
refine (match x0 in (Interpret _ r) return (Plus a0 r = RT -> T) with
    | inl a b _ => _
    | inr a b _ => _
    | rec x1 => _
    | const _ _  => _
  end
H); intros; try discriminate.
refine (to_T _ x1 (refl_equal _)).
Defined.

On 22.03.10 10:01, Gyesik Lee wrote:
> Having seen that the problem setting seems to be not trivial to
> handle, let me ask questions one by one.
> ...
> (* the proof is finished, but termination check failed although X is
> obviously structurally smaller than x. *)

--
Best regards,
  Roman Beslik.