The Coq mailing list

[Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>]

Hello.

Could I interactively construct witnesses of sig types?

I have been a happy Coq programmer for a while, 
but almost for the first time I use sig types.

Here is a simpler variation on my program:

  Variable eq: nat -> nat -> Prop.
  Variable eq_refl: forall n, eq n n.
  Variable eq_sym: forall n1 n2, eq n1 n2 -> eq n2 n1.
  Variable eq_trans: forall n1 n2 n3, eq n1 n2 -> eq n2 n3 -> eq n1 n3.

  Record spec: Type := {index:Set; gen: index -> nat}.

  Inductive satisfy: spec -> nat -> Prop :=
  | satisfy_intro: forall p x n, 
    eq (gen p x) n -> satisfy p n.

  Definition spec_and (p1 p2: spec): spec :=
  Build_spec 
  ({x: prod (index p1) (index p2) | 
    eq (gen p1 (fst x)) (gen p2 (snd x))})
  (fun x => match x with exist (n, _) _ => gen p1 n end).
  
  Lemma and_intro: forall p1 p2 n,
  satisfy p1 n -> satisfy p2 n -> satisfy (spec_and p1 p2) n.
  Proof.
  intros p1 p2 n h1 h2.  
  inversion h1; subst. inversion h2; subst.

At this point the proof context contains:

  x: index p1
  x0: index p2

and I want to use (x, x0) as a witness by interactively proving 
that (x, x0) inhabits the sig type. 

I am aware that I can complete the rest of the proof with: 

  apply (satisfy_intro 
  (Build_spec  
  ({x: prod (index p1) (index p2) | 
    eq (gen p1 (fst x))  (gen p2 (snd x))})
  (fun x => match x with exist (n, _) _ => gen p1 n end))
  (@exist (prod (index p1) (index p2))  
                (fun x => eq (gen p1 (fst x)) (gen p2 (snd x)))
                (x, x0) (eq_trans _ _ _ H (eq_sym _ _ H0))) n).
  simpl. apply H. 


However my situation is a little bit more complex than this example, and 
I have spent more than 30 min to construct the above "apply" term....

Kind regards,
Keiko