The Coq mailing list

[Roman Beslik <beroal AT ukr.net>]

On 22.03.10 16:35, Gyesik Lee wrote:
> Many thanks Roman.
> You gave me the right answer what I wanted to know.
> Doing "pattern matching" again was the key point, I think, to overcome
> Coq's restriction, wasn't it?
>    
"inversion x0" does "pattern matching". I think that it fails because 
"subst b" stands before "inversion x0" (see another proof below). 
"inversion H. subst b." changes "x0" to something different. There are 
different variables "x0 : Interpret RT b" and "x1 : Interpret RT Rec" in 
the proof term.
> Now when I look at the proof term created by Coq, it is really huge
> because of pattern matching caused by "discriminate" tactic.
> I am wondering if there is a way to simplify it.
>    
You can move that pattern matching to separate theorems.
====
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.

inversion H. subst a0. inversion i. exact (A X).

(* second case: [r = Rec] *)
inversion x0.
subst b; try discriminate.
subst b; try discriminate.
refine (to_T _ X (refl_equal _)).
subst b; try discriminate.
Defined.

--
Best regards,
  Roman Beslik.